Nuprl Definition : type-cat
TypeCat == <Type, λI,J. (I ⟶ J), λI,x. x, λI,J,K,f,g. (g o f)>
Definitions occuring in Statement :
compose: f o 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: f o 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:
2020_05_20-AM-07_52_22
Last ObjectModification:
2015_09_23-AM-09_29_14
Theory : small!categories
Home
Index