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 : 
functor-comp: functor-comp(F;G)
, 
lambda: λx.A[x]
, 
id_functor: 1
, 
pair: <a, b>
, 
cat-functor: Functor(C1;C2)
, 
small-category: SmallCategory
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:
2017_01_10-AM-08_41_14
Last ObjectModification:
2017_01_09-AM-10_55_31
Theory : small!categories
Home
Index