Nuprl Definition : interval-presheaf
This is the cubical set that assigns to a finite set of names I the
points of the free DeMorgan algebra generated by I.
Since, a morphism f : I->J maps J -> dM(I), it lifts to a
homomorphism dM(J)->dM(I).⋅
𝕀 == <λI.Point(dM(I)), λJ,I,f. dM-lift(I;J;f)>
Definitions occuring in Statement :
dM-lift: dM-lift(I;J;f),
dM: dM(I),
lattice-point: Point(l),
lambda: λx.A[x],
pair: <a, b>
Definitions occuring in definition :
pair: <a, b>,
lattice-point: Point(l),
dM: dM(I),
lambda: λx.A[x],
dM-lift: dM-lift(I;J;f)
FDL editor aliases :
interval-presheaf
Latex:
\mBbbI{} == <\mlambda{}I.Point(dM(I)), \mlambda{}J,I,f. dM-lift(I;J;f)>
Date html generated:
2016_07_08-PM-06_30_54
Last ObjectModification:
2016_06_30-PM-02_26_45
Theory : cubical!type!theory
Home
Index