Circ-Kleisli構成

懸案のCirc-Kleisli構成をやっと確認できた。対称モノイド圏Cの上の強モノイドTに対して、Circ-Kleisli圏C_+Tを確実に構成できます。

Circ-Kleisli射のU-stamping

C=(C; +, 0, σ)を対称モノイド圏、T=(T, μ, η, τ)をC上の強モナドとする。τはTの強度(tensorial strength)である。ただし、τは T(A)+B → T(A+B) の形を採用する（通常の定義とは左右が逆）。強度の公理もすべて左右が逆になる。

f:A+X→T(B+X)の形をしたCの射をCirc-Kleisli射と呼ぶ。

U∈|C|に対して、fのU-stampingを次のように定義する。

• f_U = (f+U);τ_(B+X, U);T(B+σ_(X, U))

この定義から、f_U:A+X+U → T(B+U+X) となる（UとXの順序に注意）。

Circ-Kleisli結合

以下、Circ-KleisliをCKと略記。

f:A+X → T(B+X)、g:B+Y → T(C+Y) が2つのCK射とするとき、CK結合##を次のように定義する。

• f##g = f_Y # g_X

ここで、#は普通のKleisli結合； u#v = u;T(v);μ。

AのCK単位 A+0 → T(A+0)は、Tの単位ηとする。正確にいえば、(η+0);τ_(A, 0)である。

仮定する等式群

CK射の全体は、CK結合とCK単位に関して圏になる。これを示すためには次の等式群が使われる。単位律は簡単だから、結合律の証明に関して述べる。

まず、通常のKleisli圏の結合律に相当する次の等式。f:A→T(B)として：

 TT(A) -[μ_A]→ T(A) -[T(f)]→ TT(B) -[μ_B]→ T(B)

 ===================================================

 TT(A) -[TT(f)]→ TTT(B) -[T(μ_B)]→ TT(B) 

   -[μ_B]→ T(B)

次の2つは強度の公理：

 T(A)+B+C -[τ_(A, B)]→ T(A+B)+C 

    -[τ_(A+B, C)]→ T(A+B+C)

 ==================================

 T(A)+B+C -[τ_(A, B+C)]→ T(A+B+C)
 

 TT(A)+B -[μ_A +B]→ T(A)+B  

    -[τ_(A, B)]→ T(A+B)

 ===============================================

 TT(A)+B  -[τ_(T(A), B)]→ T(T(A)+B) 

    -[T(τ_(A, B))] → T(T(A+B))  

    -[μ_(A+B)]→ T(A+B)

そして、（忘れないでね）τが自然変換であること。K(A, B)=T(A)+B、L(A, B)=T(A+B)とすると、τ::K⇒L となっている。これを、f:A→B、u:X→Yに関して書き下すと：

 T(A)+X -[T(f)+u]→ T(B)+Y -[τ_(B, X)]→ T(B+Y)

 ===============================================

 T(A)+X -[τ_(A, X)]→ T(A+X) -[T(f+u)]→ T(B+Y)

計算法

このままだと、計算はけっこう大変である（brute force calc.）。全部pictureに翻訳して、絵算（pictorial calc.）を行う。仮定する等式群を、絵算のグラフ書き換え規則にして、そのパターンを参照しながら、グラフ書き換えを行う。T(-)を「四角の箱で囲む」、τを「合流して箱に入る」、μを「入れ子の箱から中身の箱を引っ張り出す」ような印を使うと直観的に絵算を遂行できる。射の方向を上から下にしたほうがレイアウトが楽なようである。