Nuprl Definition : monad-from
monad-from(Mnd) ==
mk-monad(functor(ob(T) = M-map(Mnd) T;
arrow(X,Y,f) = λz.(M-bind(Mnd) z (λx.(M-return(Mnd) (f x)))));λx.M-return(Mnd);λx,z. (M-bind(Mnd) z
(λx.x)))
Definitions occuring in Statement :
mk-monad: mk-monad(T;u;m),
mk-functor: mk-functor,
apply: f a,
lambda: λx.A[x],
M-bind: M-bind(Mnd),
M-return: M-return(Mnd),
M-map: M-map(mnd)
Definitions occuring in definition :
lambda: λx.A[x],
M-bind: M-bind(Mnd),
apply: f a,
M-return: M-return(Mnd),
M-map: M-map(mnd),
mk-functor: mk-functor,
mk-monad: mk-monad(T;u;m)
FDL editor aliases :
monad-from
Latex:
monad-from(Mnd) ==
mk-monad(functor(ob(T) = M-map(Mnd) T;
arrow(X,Y,f) = \mlambda{}z.(M-bind(Mnd) z (\mlambda{}x.(M-return(Mnd) (f x)))));\mlambda{}x.M-return(Mnd);
\mlambda{}x,z. (M-bind(Mnd) z (\mlambda{}x.x)))
Date html generated:
2017_01_19-PM-02_59_52
Last ObjectModification:
2017_01_18-AM-00_17_33
Theory : small!categories
Home
Index