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 :
mk-adjunction: mk-adjunction(b.eps[b];a.eta[a]),
apply: f a,
cat-id: cat-id(C),
monad-fun: M(x),
monad-unit: monad-unit(M;x)
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:
2020_05_20-AM-08_00_00
Last ObjectModification:
2017_01_17-PM-02_43_27
Theory : small!categories
Home
Index