強モナドってか？ -- まだcirc-Kleisli構成

対称モノイド圏上のモナドFで、Fによるcirc-Kleisli構成のためにF(A)+F(B)→F(A+B)が必要だと書いたが、実際には、モナド単位B→F(B)と組み合わせて、F(A)+B→F(A)+F(B)→F(A+B)として使う。つまり、ほんとに必要なのはF(A)+B→F(A+B)だった。

F(A)+B→F(A+B)は、テンソル強度（tensorial strength）というらしい。テンソル強度を持つモナドは強モナド（strong monad）らしい。つまり、対称モノイド圏+強モナドがcirc-Kleisli構成のsettingになるようだ。

強度があれば、f:A→F(B) に対して、f'_X:A+X→F(B)+X→F(B+X)が定義できる、これは“F-resulticなf”のX拡張と呼べるだろう。F-resulticを保つモノイダルラベリングだ。circ-Klisli構成では、f:A+X→F(B+X)に対して、f':A+X+Y→F(B+Y+X)という射が必要。X+YがY+Xになっている所がミソで、対称でひねった“twisted Y拡張”だ。FがIdentityなら、f':A+X+Y→B+Y+Xとなる。g:B+Y→C+Yのとき、f'_Y:A+X+Y→F(B+Y+X)、g'_X:B+Y+X→F(B+X+Y)となり、うまいことKleisli composableである。

強モナドについては、Moggiの"Computational lambda-calculus and monads"（http://www.disi.unige.it/person/MoggiE/ftp/lics89.pdf）に書いてある。circ-Klisli構成とMoggiの議論、どうも状況は似たような感じだが、ハッキリとは関連を把握できない。

とりあえず、強モナドの定義を引き写しておく：

tensorial strength tA,B:A×TB→T(A×B)

×の単位性 rA:1×A→A

×の結合性 αA,B,C:(A×B)×C→A×(B×C)
(等式1)

1×TA-[t1,A]→T(1×A)-[T(rA]→TA

 ‖

1×TA-[rTA]→TA
(等式2)

(A×B)×TC-[tA×B,TC]→T( (A×B)×C)-[T(α)]→T(A×(B×C))

 ‖

(A×B)×TC-[α]→A×(B×TC)-[A×tB,C]→A×T(B×C)-[tA,B×C]→T(A×(B×C))
(等式3)

A×B-[A×ηB]→A×TB-[tA,TB]→T(A×B)

 ‖

A×B-[η]→T(A×B)
(等式4)

A×TTB -[A×μB]→A×TB-[tA,B]→T(A×B)

 ‖

A×TTB -[TA,TB]→T(A×TB)-[T(tA,B)]→TT(A×B) 

 -[μA×B]→T(A×B)

天下りだと辛いので、Moggiはラショネールを述べているが、モノイド閉圏の自己enrichmentが出てくる。そんなのが必要だとも思えないのだが、、、テンソル強度が要るのか？ほんとに。

テンソル強度t:A×TB→T(A×B)から、ペアリングT(A)×T(B)→T(A×B)を作れると、Moggiは言っている。σを対称、-^#をモナドの拡張として、σ_TA,TB;t_TB,A;(σ_TB,A;t_A,B)^#だそうだ。

TA×TB-[σ]→TB×TA-[t]→T(TB×A) -

[(TB×A -[σ]→A×TB-[t]→T(A×B))#]

ペアリング（と呼ぶらしい）の公理化はないのか？