Nuprl Definition : face-presheaf
𝔽 == <λI.Point(face_lattice(I)), λJ,I,f. <f>>
Definitions occuring in Statement :
fl-morph: <f>,
face_lattice: face_lattice(I),
lattice-point: Point(l),
lambda: λx.A[x],
pair: <a, b>
Definitions occuring in definition :
pair: <a, b>,
lattice-point: Point(l),
face_lattice: face_lattice(I),
lambda: λx.A[x],
fl-morph: <f>
FDL editor aliases :
face-presheaf
Latex:
\mBbbF{} == <\mlambda{}I.Point(face\_lattice(I)), \mlambda{}J,I,f. <f>>
Date html generated:
2016_05_18-PM-00_16_10
Last ObjectModification:
2015_10_15-PM-03_23_20
Theory : cubical!type!theory
Home
Index