Nuprl Definition : Kleisli-cat
Kl(C;M) ==
  Cat(ob = cat-ob(C);
      arrow(x,y) = cat-arrow(C) x M(y);
      id(x) = monad-unit(M;x);
      comp(x,y,z,f,g) = cat-comp(C) x M(y) M(z) f monad-extend(C;M;y;z;g))
Definitions occuring in Statement : 
monad-extend: monad-extend(C;M;x;y;f)
, 
monad-unit: monad-unit(M;x)
, 
monad-fun: M(x)
, 
mk-cat: mk-cat, 
cat-comp: cat-comp(C)
, 
cat-arrow: cat-arrow(C)
, 
cat-ob: cat-ob(C)
, 
apply: f a
Definitions occuring in definition : 
monad-extend: monad-extend(C;M;x;y;f)
, 
monad-fun: M(x)
, 
cat-comp: cat-comp(C)
, 
apply: f a
, 
monad-unit: monad-unit(M;x)
, 
cat-arrow: cat-arrow(C)
, 
cat-ob: cat-ob(C)
, 
mk-cat: mk-cat
FDL editor aliases : 
Kleisli-cat
Latex:
Kl(C;M)  ==
    Cat(ob  =  cat-ob(C);
            arrow(x,y)  =  cat-arrow(C)  x  M(y);
            id(x)  =  monad-unit(M;x);
            comp(x,y,z,f,g)  =  cat-comp(C)  x  M(y)  M(z)  f  monad-extend(C;M;y;z;g))
Date html generated:
2017_01_19-PM-02_59_16
Last ObjectModification:
2017_01_17-AM-11_47_14
Theory : small!categories
Home
Index