Nuprl Definition : irr-face-morph
irr-face-morph(I;as;bs) == λi.if i ∈b as then 0 if i ∈b bs then 1 else <i> fi
Definitions occuring in Statement :
dM1: 1,
dM0: 0,
dM_inc: <x>,
names-deq: NamesDeq,
deq-fset-member: a ∈b s,
ifthenelse: if b then t else f fi ,
lambda: λx.A[x]
Definitions occuring in definition :
lambda: λx.A[x],
dM0: 0,
ifthenelse: if b then t else f fi ,
deq-fset-member: a ∈b s,
names-deq: NamesDeq,
dM1: 1,
dM_inc: <x>
FDL editor aliases :
irr-face-morph
Latex:
irr-face-morph(I;as;bs) == \mlambda{}i.if i \mmember{}\msubb{} as then 0 if i \mmember{}\msubb{} bs then 1 else <i> fi
Date html generated:
2017_02_21-AM-10_34_07
Last ObjectModification:
2017_02_03-PM-00_14_55
Theory : cubical!type!theory
Home
Index