Nuprl Definition : extend-face-term
This construction extends a partial term u ∈ {I,phi ⊢ _:𝔽} to a
total formula in 𝔽(I).
For each face, fc = (irr_face(I;as;bs)),
in the components of phi, there is a "free-est" morphism,
g=(irr-face-morph(I;as;bs)), that makes (fc)g = 1.
This makes (fc ∧ u(g)) a well-defined formula in 𝔽(I).
The join of all of these formulas is the extension.
It satisfies these additional properties:
Error :extend-face-term-property
Error :extend-face-term-le
Error :extend-face-term-unique
Error :extend-face-term-morph
We use it to define the composition operation for ⌜𝔽⌝
face_comp.
face_comp_wf⋅
extend-face-term(I;phi;u) ==
\/(λpr.let as,bs = pr
in irr_face(I;as;bs) ∧ u(irr-face-morph(I;as;bs))"(face_lattice_components(I;phi)))
Definitions occuring in Statement :
cubical-term-at: u(a),
irr-face-morph: irr-face-morph(I;as;bs),
face_lattice_components: face_lattice_components(I;x),
irr_face: irr_face(I;as;bs),
face_lattice-deq: face_lattice-deq(),
face_lattice: face_lattice(I),
names-deq: NamesDeq,
names: names(I),
lattice-fset-join: \/(s),
lattice-meet: a ∧ b,
fset-image: f"(s),
deq-fset: deq-fset(eq),
fset: fset(T),
product-deq: product-deq(A;B;a;b),
lambda: λx.A[x],
spread: spread def
Definitions occuring in definition :
face_lattice_components: face_lattice_components(I;x),
irr-face-morph: irr-face-morph(I;as;bs),
cubical-term-at: u(a),
irr_face: irr_face(I;as;bs),
face_lattice: face_lattice(I),
lattice-meet: a ∧ b,
spread: spread def,
lambda: λx.A[x],
face_lattice-deq: face_lattice-deq(),
names-deq: NamesDeq,
deq-fset: deq-fset(eq),
names: names(I),
fset: fset(T),
product-deq: product-deq(A;B;a;b),
fset-image: f"(s),
lattice-fset-join: \/(s)
FDL editor aliases :
extend-face-term
Latex:
extend-face-term(I;phi;u) ==
\mbackslash{}/(\mlambda{}pr.let as,bs = pr
in irr\_face(I;as;bs) \mwedge{} u(irr-face-morph(I;as;bs))"(face\_lattice\_components(I;phi)))
Date html generated:
2017_02_21-AM-10_59_58
Last ObjectModification:
2017_02_07-PM-05_44_13
Theory : cubical!type!theory
Home
Index