両クライスリ圏、ひょとすると、、

ムフフフ、今回の山勘は当たりかもなー。

両クライスリ圏の単位律は証明できた。

まず、両クライスリ圏の恒等 x.ι（恒等もDOTNで書く）を次のように定義する。

• x.ι := x.(ε|η) = x.ε ; x.η

図式順両クライスリ結合を f # g として、x.ι # f = f を示せばいい。

x.ι # f

// 両クライスリ結合の定義

= x.δ ; (x.ι).F ; x.τ ; f.G ; x.μ

// x.ιの定義

= x.δ ; (x.ε ; x.η).F ; x.τ ; f.G ; x.μ

// Fの関手性

= x.δ ; (x.ε).F ; (x.η).F ; x.τ ; f.G ; x.μ

// Fのコモナド余単位律； x.δ ; (x.ε).F

= (x.F)^  ; (x.η).F ; x.τ ; f.G ; x.μ

// 恒等だから

= x.η.F ; x.τ ; f.G ; x.μ

// ベックの法則・単位律； x.η.F ; x.τ

= x.F.η ; f.G ; x.μ

// ηの自然性； x.F.η ; f.G

= f; x.G.η ; x.μ

// Gのモナド単位律

= f ; (x.G)^

// 恒等だから

= f

この計算で、「Fのコモナド余単位律」「ベックの法則・単位律」「Gのモナド単位律」が、この順で適用されている点に非常に強い必然性を感じる。

まだ安心はできないが、両クライスリ圏が存在する状況証拠は揃ったな。