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 :
bag-union: bag-union(bbs),
bag-map: bag-map(f;bs),
single-bag: {x},
bag: bag(T),
mk-monad: mk-monad,
mk-nat-trans: x |→ T[x],
mk-functor: mk-functor,
lambda: λx.A[x]
Definitions occuring in definition :
bag: bag(T),
bag-map: bag-map(f;bs),
single-bag: {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:
2020_05_20-AM-08_04_23
Last ObjectModification:
2020_01_16-PM-05_25_35
Theory : bags
Home
Index