Nuprl Definition : cubical-interval
cubical-interval() == <λI.(name-morph(I;[]) ⟶ ℕ2), λJ,K,f,L,g. (L (f o g))>
Definitions occuring in Statement :
name-comp: (f o g),
name-morph: name-morph(I;J),
nil: [],
int_seg: {i..j-},
apply: f a,
lambda: λx.A[x],
function: x:A ⟶ B[x],
pair: <a, b>,
natural_number: $n
Definitions occuring in definition :
pair: <a, b>,
function: x:A ⟶ B[x],
name-morph: name-morph(I;J),
nil: [],
int_seg: {i..j-},
natural_number: $n,
lambda: λx.A[x],
apply: f a,
name-comp: (f o g)
FDL editor aliases :
cubical-interval
Latex:
cubical-interval() == <\mlambda{}I.(name-morph(I;[]) {}\mrightarrow{} \mBbbN{}2), \mlambda{}J,K,f,L,g. (L (f o g))>
Date html generated:
2016_06_16-PM-05_38_27
Last ObjectModification:
2015_09_23-AM-09_30_08
Theory : cubical!sets
Home
Index