とりあえず使う予定の等式を列挙。ここでは反図式順は一切使わず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がC上のコモナド、Gがモナドのとき、F(X)→G(Y) というCの射を X→Y という射だと思って、両クライスリ圏を構成したい。どうしたらいいか？ という話。F = (F, δ, ε), G = (G, μ, η) だとする。ほかに、τ::FG⇒GF があるとする。τはスワッパーと呼ぶ。f:F(X)→G…

MをC上のモナドとして、K = Kl(C, M)をクライスリ圏とする。対応(-)--:C→K と (-)∨:K→C を次のように定義する。 X-- = X (f:X→Y)-- = f;εY:X→M(Y) (X→Y in K) X∨ = M(X) (k:X→M(Y))∨ = M(k);μY:M(X)→M(Y) (-)--と(-)∨が実際に関手であることを計算してみる。…