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

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

まず、ベックの法則（全部で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.μ