Nuprl Definition : functor-cat
FUN(C1;C2) == <Functor(C1;C2), λF,G. nat-trans(C1;C2;F;G), λF.identity-trans(C1;C2;F), λF,G,H,t1,t2. t1 o t2>
Definitions occuring in Statement :
trans-comp: t1 o 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: t1 o t2
FDL editor aliases :
functor-cat
Latex:
FUN(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. t1 o t2>
Date html generated:
2020_05_20-AM-07_51_52
Last ObjectModification:
2015_09_23-AM-09_29_11
Theory : small!categories
Home
Index