PS

Naturality for bifunctors

定義 Functor Natural transformation

Bifunctor

Domainがproduct categoryになっているfunctorのこと。

Partial application

bifunctor $F : \mathcal{C} \times \mathcal{D} \rightarrow \mathcal{E}$
$\mathcal{C}$ -object $X$

について、functor:

$F(X, \unicode{x2013}) : \mathcal{D} \rightarrow \mathcal{E}$
$F(X, \unicode{x2013}) _ 0(Y) = F(X, Y)$
$F(X, \unicode{x2013}) _ 1(g\ : Y \rightarrow Y') = F(1 _ X, g) : F(X, Y) \rightarrow F(X, Y')$

を定義できる。同様にして、functor:

$F(\unicode{x2013}, Y) : \mathcal{C} \rightarrow \mathcal{E}$
$F(\unicode{x2013}, Y) _ 0(X) = F(X, Y)$
$F(\unicode{x2013}, Y) _ 1(f : X \rightarrow X') = F(f, 1 _ Y) : F(X, Y) \rightarrow F(X', Y)$

を定義できる。

命題

$\big( F(1 _ X, g) \big) _ X : \text{natural}$
$\big( F(f, 1 _ Y) \big) _ Y : \text{natural}$

Natural in both X and Y

Morphism族 $(\eta _ {X, Y}) _ {X, Y}$ がnaturalということ。

命題

bifunctor $F, G : \mathcal{C} \times \mathcal{D} \rightarrow \mathcal{E}$
morphism族 $\big( \eta _ {X, Y} : F(X, Y) \rightarrow G(X, Y) \big) _ {X, Y}$

について

*1
- ${} ^ \forall Y, (\eta _ {X, Y}) _ {X} : \text{natural}$
- and ${} ^ \forall X, (\eta _ {X, Y}) _ {Y} : \text{natural}$ *2

参考文献

Product of Categories (Pt. II) « Abstract Nonsense

*1: (co)domainはbifunctor

*2: (co)domainはpartial application