Nuprl Definition : Kleisli-adjunction
Kl(C;M) == mk-adjunction(y.cat-id(C) M(y);x.monad-unit(M;x))
Definitions occuring in Statement :
monad-unit: monad-unit(M;x),
monad-fun: M(x),
mk-adjunction: mk-adjunction(b.eps[b];a.eta[a]),
cat-id: cat-id(C),
apply: f a
Definitions occuring in definition :
monad-unit: monad-unit(M;x),
monad-fun: M(x),
cat-id: cat-id(C),
apply: f a,
mk-adjunction: mk-adjunction(b.eps[b];a.eta[a])
FDL editor aliases :
Kleisli-adjunction
Latex:
Kl(C;M) == mk-adjunction(y.cat-id(C) M(y);x.monad-unit(M;x))
Date html generated:
2017_01_19-PM-02_59_37
Last ObjectModification:
2017_01_17-PM-02_43_27
Theory : small!categories
Home
Index