Nuprl Definition : adjunction-monad
adjMonad(adj) ==
mk-monad(functor-comp(F;G);snd(adj);x |→ arrow(G) (ob(F) (ob(G) (ob(F) x))) (ob(F) x) ((fst(adj)) (ob(F) x)))
Definitions occuring in Statement :
mk-monad: mk-monad(T;u;m),
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 :
functor-ob: ob(F),
apply: f a,
pi1: fst(t),
functor-arrow: arrow(F),
mk-nat-trans: x |→ T[x],
pi2: snd(t),
functor-comp: functor-comp(F;G),
mk-monad: mk-monad(T;u;m)
FDL editor aliases :
adjunction-monad
Latex:
adjMonad(adj) ==
mk-monad(functor-comp(F;G);snd(adj);x |\mrightarrow{} arrow(G) (ob(F) (ob(G) (ob(F) x))) (ob(F) x)
((fst(adj)) (ob(F) x)))
Date html generated:
2017_01_19-PM-02_59_01
Last ObjectModification:
2017_01_17-AM-00_18_57
Theory : small!categories
Home
Index