Nuprl Definition : cat-cat
Cat == <SmallCategory, λC1,C2. Functor(C1;C2), λC.1, λC1,C2,C3,F,G. functor-comp(F;G)>
Definitions occuring in Statement :
id_functor: 1,
functor-comp: functor-comp(F;G),
cat-functor: Functor(C1;C2),
small-category: SmallCategory,
lambda: λx.A[x],
pair: <a, b>
Definitions occuring in definition :
small-category: SmallCategory,
cat-functor: Functor(C1;C2),
pair: <a, b>,
id_functor: 1,
lambda: λx.A[x],
functor-comp: functor-comp(F;G)
FDL editor aliases :
cat-cat
Latex:
Cat == <SmallCategory, \mlambda{}C1,C2. Functor(C1;C2), \mlambda{}C.1, \mlambda{}C1,C2,C3,F,G. functor-comp(F;G)>
Date html generated:
2020_05_20-AM-07_53_43
Last ObjectModification:
2017_01_09-AM-10_55_31
Theory : small!categories
Home
Index