Nuprl Definition : fl-morph
<f> == fl-lift(names(J);NamesDeq;face_lattice(I);face_lattice-deq();λj.dM-to-FL(I;¬(f j));λj.dM-to-FL(I;f j))
Definitions occuring in Statement :
dM-to-FL: dM-to-FL(I;z),
face_lattice-deq: face_lattice-deq(),
face_lattice: face_lattice(I),
names-deq: NamesDeq,
names: names(I),
dm-neg: ¬(x),
fl-lift: fl-lift(T;eq;L;eqL;f0;f1),
apply: f a,
lambda: λx.A[x]
Definitions occuring in definition :
fl-lift: fl-lift(T;eq;L;eqL;f0;f1),
face_lattice: face_lattice(I),
face_lattice-deq: face_lattice-deq(),
dm-neg: ¬(x),
names: names(I),
names-deq: NamesDeq,
lambda: λx.A[x],
dM-to-FL: dM-to-FL(I;z),
apply: f a
FDL editor aliases :
fl-morph
Latex:
<f> ==
fl-lift(names(J);NamesDeq;face\_lattice(I);face\_lattice-deq();\mlambda{}j.dM-to-FL(I;\mneg{}(f j));
\mlambda{}j.dM-to-FL(I;f j))
Date html generated:
2016_05_18-PM-00_14_09
Last ObjectModification:
2015_10_15-PM-06_07_17
Theory : cubical!type!theory
Home
Index