Circ-Kleisli構成、それから

あんれー、実際に定義を書き下したり計算してみたら、どうも予想と違うぞ。

まず、Moggiが触れていたTの強度τ:A+T(B)→T(A+B)を使ったペアリング T(A)+T(B)→T(A+B)は、τの左右を逆にした余強度τ':T(A)+B →T(A+B)を使って書くと自然なことがわかった。ペアリングの定義は強度と余強度（costrength）を使う順序により2種類定義できる。この2つのペアリングが一致することが可換モナド（commutative monad）の定義になる。

τ':: T(A)+B -[σ]→ B+T(A) -[τ]→ T(B+A) -[T(σ)]→ T(A+B)
ペアリング:: T(A)+T(B) -[τ']→ T(A+T(B)) -[T(τ)]→ T(T(A+B))

              -[μ]→T(A+B)
ペアリング':: T(A)+T(B) -[τ]→ T(TA+B) -[T(τ')]→ T(T(A+B))

              -[μ]→T(A+B)

さて、Moggiのペアリングを使うとf:A→T(B)、g:C→T(D)のモノイド積f+g:A+C → T(B+D)は簡単に定義できる。ペアリング＝Kleisli圏のモノイド積を使ってU-stamping f_U を定義すると、けっこう複雑になる。僕の定義とはどうも違うようだ。

 A+B -[f+g]→ T(B)+T(D) -[ペアリング]→ T(B+D)

もうひとつ、hom-catをうまく定義できるかどうかがポイントとなる -- hom-cat = 余代数圏 となってほしい。どんな定義がいいのかは、やっぱり例を調べるしかないようだ。とにかく例を作らないと。