豊饒圏から圏を作る -- ピノキオと人間

Vが対称モノイド閉圏だとして、□がモノイド積、[-, -]はベキ（指数）とする。そのとき、対象A, B, Cに対して、V内で結合を与える射c_A,B,C:[A, B]□[B, C]→[A, C] を定義したい。

まず、次の自然演繹証明図を考える。

        A⊃B   A

       ----------[MP]

  B⊃C   B

 ----------[MP]

     C

これから、[B, C]□[A, B]□A → C が得られる。[B, C]と[A, B]に対称（置換、入れ替え）σ_[B,C],[A,B]を適用すれば、[A, B]□[B, C]□A → C、これをカリー化すれば、[A, B]□[B, C] →[A, C]。□の優先順位が強いとして、具体的に書き下すと：

• Λ_[A,B],[B,C]^A(σ_[B,C],[A,B]□id_A ; id_[B,C]□ev_A,B ; ev_B,C)

次にV-豊饒化している状況を考える。CがV-圏のとき、f:A→B, g:B→C in C は、f:I→C(A, B), g:I→C(B, C) in V のことだと解釈。Δ:I→I□I は単位律を使って定義可能だから、ペアリング<f, g>を、Δ;(f□g) で定義できる。c_A,B,C:C(A, B)□C(B, C)→C(A, C) があるから、fとgの結合f;g は <f, g>;c_A,B,C:I→C(A, C) として定義できる。

以上の方法を使うと、V-圏Cに対して、普通の圏Dを D(A, B) = V(I, C(A, B)) で定義できる。こうすれば、f:A→B in C は、f∈D(A, B)のことだとも解釈できる。記号の乱用をして、f:A→B in C ⇔ f:A→B in D （ちょっと混乱しそうだが）。ホントのことを言えば、Cには対象はあるが、射と呼べるモノなんてまったく存在しない、射の集まりに相当するモノがあっただけなのだ。しかし、Dには確かに射が存在し、普通にここで圏論できる。

V-圏Cの概念には、D(A, B) = V(I, C(A, B)) を使った普通の圏が常に付きまとっている。バエズの例えで言うなら、CはピノキオだがDは人間だ。

Cとして、Vの標準自己豊饒圏を取ると、Cから作ったDによりVが再現する。この再現機構は詳しく見ておいたほうがいいだろう。