Nuprl Definition : fl-all-hom
fl-all-hom(I;i) ==
fl-lift(names(I+i);NamesDeq;face_lattice(I);face_lattice-deq();λx.if (x =z i) then 0 else (x=0) fi ;λx.if (x =z i)
then 0
else (x=1)
fi )
Definitions occuring in Statement :
fl1: (x=1),
fl0: (x=0),
face_lattice-deq: face_lattice-deq(),
face_lattice: face_lattice(I),
add-name: I+i,
names-deq: NamesDeq,
names: names(I),
fl-lift: fl-lift(T;eq;L;eqL;f0;f1),
lattice-0: 0,
ifthenelse: if b then t else f fi ,
eq_int: (i =z j),
lambda: λx.A[x]
Definitions occuring in definition :
fl-lift: fl-lift(T;eq;L;eqL;f0;f1),
names: names(I),
add-name: I+i,
names-deq: NamesDeq,
face_lattice-deq: face_lattice-deq(),
fl0: (x=0),
lambda: λx.A[x],
ifthenelse: if b then t else f fi ,
eq_int: (i =z j),
lattice-0: 0,
face_lattice: face_lattice(I),
fl1: (x=1)
FDL editor aliases :
fl-all-hom
Latex:
fl-all-hom(I;i) ==
fl-lift(names(I+i);NamesDeq;face\_lattice(I);face\_lattice-deq();
\mlambda{}x.if (x =\msubz{} i) then 0 else (x=0) fi ;\mlambda{}x.if (x =\msubz{} i) then 0 else (x=1) fi )
Date html generated:
2016_05_18-PM-00_17_11
Last ObjectModification:
2016_03_25-AM-10_17_20
Theory : cubical!type!theory
Home
Index