PS

Bifunctoriality

圏論定義 Bifunctor

Product category

Product category - PS より、product category:

$\mathcal{A} \times \mathcal{B}$

とは

$1 _ { (A, B) } := (1 _ A, 1 _ B)$
$(a', b') \circ (a, b) := (a' \circ a, b' \circ b)$

･･･のような category であった。

Bifunctor

Domain が product category の functor:

$\phi : \mathcal{A} \times \mathcal{B} \to \mathcal{C}$

のこと。*1

記法

$\phi(a : A \to A', b : B \to B') := \phi( (a, b) : (A, A') \to (B, B') )$

Bifunctoriality

Bifunctor の functoriality は

$\phi( 1 _ A, 1 _ B ) = \phi( 1 _ {(A, B)} ) = 1 _ { \phi(A, B) }$
$\phi( a' \circ a, b' \circ b) = \phi ( (a', b') \circ (a, b) ) = \phi(a', b') \circ \phi(a, b)$

中置記法では

$1 _ A \operatorname{\phi} 1 _ B = 1 _ { A \operatorname{\phi} B }$
$(a' \circ a) \operatorname{\phi} (b' \circ b) = (a' \operatorname{\phi} b') \circ (a \operatorname{\phi} b)$

参考文献

*1:圏論の用語としては怪しいらしい