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

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

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

まず、両クライスリ圏の恒等 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のモナド単位律」が、この順で適用されている点に非常に強い必然性を感じる。

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

両クライスリ圏、出来た！

ビンゴッ！！ やったーっ、ひさびさの大当たり。

ベックの法則と簡単な補題を3つ使って結合律を証明できた。分かってしまえば、単純計算。いやー、DOTNは強力だ。絵算とDOTNがなければ、とても計算できかったろう、僕には。

念のためもう一度確認してから書く。両モナド（コモナド＋モナド＋ベックの法則）とその両クライスリ圏の存在は間違いない。コモナドF, モナドGに対して、その両クライスリ圏を DiKl(F, G; C)と書こう。Cが分かっていれば DiKl(F, G)。標準的な関手 C→DiKl(F, G; C) と DiKl(F, G; C) → C を構成しないとね。

両モナドと両クライスリ圏

計算手順をざっと書いておこう。

まず、ベックの法則（全部で4つ）のうちの2つ

1. Gδ|τF|Fτ = τ|δG （ベックの法則・余乗法スワップ）
2. Gτ|τG|Fμ = μF|τ （ベックの法則・乗法スワップ）

成分表示なら：

1. x.G.δ ; x.τ.F ; x.F.τ = x.τ ; x.δ.G （ベックの法則・余乗法スワップ）
2. x.G.τ ; x.τ.G ; x.F.μ = x.μ.F ; x.τ （ベックの法則・乗法スワップ）

仮定する3つの両クライスリ射：

1. f:x.F→y.G
2. g:y.F→z.G
3. h:z.F→w.G

変換の自然性の図式に、さらに関手を適用して示せる補題を3つ。

1. f.F ; y.G.δ = x.δ.F ; f.F.F
2. g.G.F ; z.G.τ = y.F.τ ; g.F.G
3. z.F.μ ; h.G = h.G.G ; w.μ.G

定義とベックの法則を使って平坦にしておく。

  (f#g) # h 

= x.δ ; (f#g).F ; z.τ ; h.G ; w.μ

// f#g の定義

= x.δ ; (x.δ ; f.F ; y.τ ; g.G ; z.μ).F ; z.τ ; h.G ; w.μ

// Fの関手性

= x.δ ; x.δ.F ; f.F.F ; y.τ.F ; g.G.F ; z.μ.F ; z.τ ; h.G ; w.μ

= x.δ ; x.δ.F ; f.F.F ; y.τ.F ; g.G.F ; (z.μ.F ; z.τ) ; h.G ; w.μ

// 括弧内をベックの法則・乗法スワップで展開

= x.δ ; x.δ.F ; f.F.F ; y.τ.F ; g.G.F ; (z.G.τ ; z.τ.G ; z.F.μ) ; h.G ; w.μ

  f # (g#h)

= x.δ ; f.F ; y.τ ; (g#h).G ; w.μ

// g#h の定義

= x.δ ; f.F ; y.τ ; (y.δ ; g.F ; z.τ ; h.G ; w.μ).G ; w.μ

// Gの関手性

= x.δ ; f.F ; y.τ ; y.δ.G ; g.F.G ; z.τ.G ; h.G.G ; w.μ.G ; w.μ

= x.δ ; f.F ; (y.τ ; y.δ.G) ; g.F.G ; z.τ.G ; h.G.G ; w.μ.G ; w.μ

// 括弧内をベックの法則・余乗法スワップで展開

= x.δ ; f.F ; (y.G.τ ; y.τ.F ; y.F.τ) ; g.F.G ; z.τ.G ; h.G.G ; w.μ.G ; w.μ

f # (g#h) の展開形を、(f#g) # h の展開形まで変形することにして：

  x.δ ; f.F ; y.G.τ ; y.τ.F ; y.F.τ ; g.F.G ; z.τ.G ; h.G.G ; w.μ.G ; w.μ

= x.δ ; (f.F ; y.G.τ) ; y.τ.F ; y.F.τ ; g.F.G ; z.τ.G ; h.G.G ; w.μ.G ; w.μ

// 括弧内に補題(1)

= x.δ ; (x.δ.F ; f.F.F) ; y.τ.F ; y.F.τ ; g.F.G ; z.τ.G ; h.G.G ; w.μ.G ; w.μ

= x.δ ; x.δ.F ; f.F.F ; y.τ.F ; (y.F.τ ; g.F.G) ; z.τ.G ; h.G.G ; w.μ.G ; w.μ

// 括弧内に補題(2)

= x.δ ; x.δ.F ; f.F.F ; y.τ.F ; (g.G.F ; z.G.τ) ; z.τ.G ; h.G.G ; w.μ.G ; w.μ

= x.δ ; x.δ.F ; f.F.F ; y.τ.F ; g.G.F ; z.G.τ ; z.τ.G ; (h.G.G ; w.μ.G) ; w.μ

// 括弧内に補題(3)

= x.δ ; x.δ.F ; f.F.F ; y.τ.F ; g.G.F ; z.G.τ ; z.τ.G ; (z.F.μ ; h.G) ; w.μ

= x.δ ; x.δ.F ; f.F.F ; y.τ.F ; g.G.F ; z.G.τ ; z.τ.G ; z.F.μ ; h.G ; w.μ