両クライスリ圏構成の準備

とりあえず使う予定の等式を列挙。ここでは反図式順は一切使わずDOTN。（http://www.chimaira.org/docs/DOTN.htm）

μ::GG⇒G の自然性

• f.G.G ; y.μ = x.μ ; f.G

η::I⇒G の自然性

• f ; y.η = x.η ; f.G

δ::F⇒FF の自然性

• f.F ; y.δ = x.δ ; f.F.F

ε::F⇒I の自然性

• f.F ; y.ε = x.ε ; f

τ::GF⇒FG の自然性

• f.G.F ; y.τ = x.τ ; f.F.G

Fがコモナドであること

1. δ|εF = F^
2. δ|Fε = F^
3. δ|Fδ = δ|δF

1. x.δ ; x.ε.F = (x.F)^
2. x.δ ; x.F.ε = (x.F)^
3. x.δ ; x.F.δ = x.δ ; x.δ.F

Gがモナドであること

1. ηG|μ = G^
2. Gη|μ = G^
3. Gμ|μ = μG|μ

1. x.η.G ; x.μ = (x.G)^
2. x.G.η ; x.μ = (x.G)^
3. x.G.μ ; x.μ = x.μ.G ; x.μ

ベックの法則

1. τ|εG = Gε
2. ηF|τ = Fη
3. Gδ|τF|Fτ = τ|δG
4. Gτ|τG|Fμ = μF|τ

1. x.τ ; x.ε.G = x.G.ε
2. x.η.F ; x.τ = x.F.η
3. x.G.δ ; x.τ.F ; x.F.τ = x.τ ; x.δ.G
4. x.G.τ ; x.τ.G ; x.F.μ = x.μ.F ; x.τ