Nuprl Definition : adjunction-monad
adjMonad(adj) == mk-monad(functor-comp(F;G);snd(adj);x |→ G (F (G (F x))) (F x) ((fst(adj)) (F x)))
Definitions occuring in Statement :
mk-monad: mk-monad,
functor-comp: functor-comp(F;G),
mk-nat-trans: x |→ T[x],
functor-arrow: arrow(F),
functor-ob: ob(F),
pi1: fst(t),
pi2: snd(t),
apply: f a
Definitions occuring in definition :
mk-monad: mk-monad,
functor-comp: functor-comp(F;G),
pi2: snd(t),
mk-nat-trans: x |→ T[x],
functor-arrow: arrow(F),
pi1: fst(t),
apply: f a,
functor-ob: ob(F)
FDL editor aliases :
adjunction-monad
Latex:
adjMonad(adj) == mk-monad(functor-comp(F;G);snd(adj);x |\mrightarrow{} G (F (G (F x))) (F x) ((fst(adj)) (F x)))
Date html generated:
2020_05_20-AM-07_59_26
Last ObjectModification:
2017_01_17-AM-00_18_57
Theory : small!categories
Home
Index