PS

Bifunctor lemma

Bifunctor lemma

Functor の族:

  •  (L ^ b  : \mathcal{C} \rightarrow \mathcal{D}) _ {b \in \mathcal{B} }
  •  (L _ {c} : \mathcal{B} \rightarrow \mathcal{C}) _ {c \in \mathcal{C} }

  •  {} ^ {\forall}b, {} ^ {\forall}c, L ^ b (c) = L _ {c}(b)

を満たすとき

  •  {} ^ {\forall}f : b \rightarrow b', {} ^ {\forall}g : c \rightarrow c', L ^ {b'}(g) \circ L _ {c}(f) = L _ {c'}(f) \circ L ^ b(g)
  •  \iff
  •  {} ^ {\exists} !L : \mathcal{B} \times \mathcal{C} \rightarrow \mathcal{D},
    •  {} ^ {\forall}c, L(\unicode{x2013}, c) = L _ {c} and  {} ^ {\forall}b, L(b, \unicode{x2013}) = L ^ {b}  *1

具体的には

  •  L(b, c) = L ^ b (c) = L _ {c}(b)
  •  L(f : b \rightarrow b', g : c \rightarrow c') = L ^ {b'}(g) \circ L _ c(f) = L _ {c'}(f) \circ L ^ {b}(g)

とすればよい。

f:id:mbps:20141208050821p:plain

Bifunctor:

  •  F,G : \mathcal{B} \times \mathcal{C} \to \mathcal{D}

について

  •  {} ^ \forall b \in \mathcal{B} _ 0, F(b, \unicode{x2013}) = G(b, \unicode{x2013})
  •  {} ^ \forall c \in \mathcal{C} _ 0, F(\unicode{x2013},c) = G(\unicode{x2013},c)

ならば

  •  F = G

参考文献

*1:functor の partial application