Nuprl Definition : bag-cat-monad
bag-cat-monad() == mk-monad(functor(ob(x) = bag(x);arrow(x,y,f) = λz.bag-map(f;z));x |→ λz.{z};x |→ λz.bag-union(z))
Definitions occuring in Statement :
mk-monad: mk-monad,
mk-nat-trans: x |→ T[x],
mk-functor: mk-functor,
lambda: λx.A[x],
bag-union: bag-union(bbs),
bag-map: bag-map(f;bs),
single-bag: {x},
bag: bag(T)
Definitions occuring in definition :
mk-monad: mk-monad,
mk-functor: mk-functor,
bag: bag(T),
bag-map: bag-map(f;bs),
single-bag: {x},
mk-nat-trans: x |→ T[x],
lambda: λx.A[x],
bag-union: bag-union(bbs)
FDL editor aliases :
bag-cat-monad
Latex:
bag-cat-monad() ==
mk-monad(functor(ob(x) = bag(x);
arrow(x,y,f) = \mlambda{}z.bag-map(f;z));
x |\mrightarrow{} \mlambda{}z.\{z\};
x |\mrightarrow{} \mlambda{}z.bag-union(z))
Date html generated:
2018_05_22-PM-09_57_58
Last ObjectModification:
2018_01_31-PM-03_17_20
Theory : small!categories
Home
Index