指数の計算：2項（共変, 反変）関手性

今さら、こんなこと書いて、つう感じもするが、、、

Xはとりあえず集合部分圏だとしておく（X→Setって忘却埋め込みがある）、CはXの適当な部分圏（Xでもよい）の逆圏。k:A→B in Cは、k:A←B in Xとなる。対象U∈|X|, A∈|C|に対して、U^A = U^Aとする。U^AはXのなかの関数空間（ベキ、指数）対象だから、|X|のなかで（upto-isoで）確定する。

以下では、記号を次のように使う。

• f:U→V in X
• g:V→W in X
• k:A→B in C i.e. k:B→A in X
• j:B→C in C i.e. j:C→B in X

f:U→Vと、k:A→Bに対して、f^k: U^A→V^B を次のように定義する：

a∈U^A、つまりa:A→U in Xに対して、b = (f^k)(a) = k;a;f : B→V in X 。

  A ←k- B

 a|      |b

  |      |

  v      v

  U -f→ V

f^kは、U^A → V^B in Xとなる。^が2変項関手になることを示す。つまり、次を示す。

1. ^(id_U, id_A) = id_{^(U, A)}
2. ^( (f, k);(g, j) ) = ^(f, k);^(g, j)

中値記法を使えば：

1. id_U^id_A = id_U^A
2. (f;g)^(k;j) = (f^k);(g^j)

一番目は、次の図を見ながら、id_U^id_A(a) = id_A;a;id_U = a、id_U^A(a) = a なのでOK。

  A ←== A

 a|      |a

  |      |

  v      v

  U ==→ U

二番目は、次の図を見ながら、

  A ←k- B ←j- C

 a|      |      |

  |      |      |

  v      v      v

  U -f=→V -g→ W

• ( (f;g)^(k;j) )(a) = (j;k);a;(f;g) （右辺は in X）
• ( (f^k);(g^j) )(a) = (g^j)( (f^k)(a) ) = (g^j)(k;a;f) = j;(k;a;f);g

結合律で括弧を付け替えれば同じ。

以上で、C⊆X⊆Setの状況で、^:X×C^op→X が2変項関手だとわかった。抽象的にベキ対象が存在する圏（例CCC）でやるなら、elementは使えないからelementless図式計算、メンド。