Nuprl Definition : type-cat

TypeCat ==  <Type, λI,J. (I ⟶ J), λI,x. x, λI,J,K,f,g. (g f)>



Definitions occuring in Statement :  compose: g lambda: λx.A[x] function: x:A ⟶ B[x] pair: <a, b> universe: Type
Definitions occuring in definition :  universe: Type function: x:A ⟶ B[x] pair: <a, b> lambda: λx.A[x] compose: g
FDL editor aliases :  type-cat

Latex:
TypeCat  ==    <Type,  \mlambda{}I,J.  (I  {}\mrightarrow{}  J),  \mlambda{}I,x.  x,  \mlambda{}I,J,K,f,g.  (g  o  f)>



Date html generated: 2016_05_18-AM-11_53_20
Last ObjectModification: 2015_09_23-AM-09_29_14

Theory : small!categories


Home Index