Nuprl Definition : functor-cat

functor-cat(C1;C2) ==
  <Functor(C1;C2), λF,G. nat-trans(C1;C2;F;G), λF.identity-trans(C1;C2;F), λF,G,H,t1,t2. trans-comp(C1;C2;F;G;H;t1;t2)>



Definitions occuring in Statement :  trans-comp: trans-comp(C;D;F;G;H;t1;t2) identity-trans: identity-trans(C;D;F) nat-trans: nat-trans(C;D;F;G) cat-functor: Functor(C1;C2) lambda: λx.A[x] pair: <a, b>
Definitions occuring in definition :  cat-functor: Functor(C1;C2) nat-trans: nat-trans(C;D;F;G) pair: <a, b> identity-trans: identity-trans(C;D;F) lambda: λx.A[x] trans-comp: trans-comp(C;D;F;G;H;t1;t2)
FDL editor aliases :  functor-cat

Latex:
functor-cat(C1;C2)  ==
    <Functor(C1;C2)
    ,  \mlambda{}F,G.  nat-trans(C1;C2;F;G)
    ,  \mlambda{}F.identity-trans(C1;C2;F)
    ,  \mlambda{}F,G,H,t1,t2.  trans-comp(C1;C2;F;G;H;t1;t2)>



Date html generated: 2016_05_18-AM-11_53_08
Last ObjectModification: 2015_09_23-AM-09_29_11

Theory : small!categories


Home Index