Nuprl Definition : dM-to-FL
dM-to-FL(I;z) ==
lattice-extend(face_lattice(I);union-deq(names(I);names(I);NamesDeq;NamesDeq);face_lattice-deq();λx.case x
of inl(a) =>
(a=1)
| inr(a) =>
(a=0);z)
Definitions occuring in Statement :
fl1: (x=1),
fl0: (x=0),
face_lattice-deq: face_lattice-deq(),
face_lattice: face_lattice(I),
names-deq: NamesDeq,
names: names(I),
lattice-extend: lattice-extend(L;eq;eqL;f;ac),
union-deq: union-deq(A;B;a;b),
lambda: λx.A[x],
decide: case b of inl(x) => s[x] | inr(y) => t[y]
Definitions occuring in definition :
lattice-extend: lattice-extend(L;eq;eqL;f;ac),
face_lattice: face_lattice(I),
union-deq: union-deq(A;B;a;b),
names: names(I),
names-deq: NamesDeq,
face_lattice-deq: face_lattice-deq(),
lambda: λx.A[x],
decide: case b of inl(x) => s[x] | inr(y) => t[y],
fl1: (x=1),
fl0: (x=0)
FDL editor aliases :
dM-to-FL
Latex:
dM-to-FL(I;z) ==
lattice-extend(face\_lattice(I);union-deq(names(I);names(I);NamesDeq;NamesDeq);face\_lattice-deq();
\mlambda{}x.case x of inl(a) => (a=1) | inr(a) => (a=0);z)
Date html generated:
2016_05_18-PM-00_11_46
Last ObjectModification:
2015_10_15-AM-10_25_07
Theory : cubical!type!theory
Home
Index