Nuprl Lemma : glue-comp-agrees2
The type (not displayed) of the equality in this lemma
is composition-structure{i:l}(G, psi; T)
This means that in "extent" psi, when ⌜G ⊢ Glue [psi ⊢→ (T;f)] A = T ∈ {G, psi ⊢ _}⌝, the
composition for ⌜Glue [psi ⊢→ (T;f)] A⌝ is the same as the composition for T.
This property of the compostion for Glue is used in construction of the
composition for c𝕌 (the cubiucal universe type).⋅
∀[G:j⊢]. ∀[A:{G ⊢ _}]. ∀[cA:G +⊢ Compositon(A)]. ∀[psi:{G ⊢ _:𝔽}]. ∀[T:{G, psi ⊢ _}]. ∀[cT:G, psi +⊢ Compositon(T)].
∀[f:{G, psi ⊢ _:Equiv(T;A)}].
comp(Glue [psi ⊢→ (T, f)] A) = cT ∈ G ⊢ Compositon(T) supposing G ⊢ (1(𝔽) ⇒ psi)
Proof
Definitions occuring in Statement :
glue-comp: comp(Glue [phi ⊢→ (T, f)] A) ,
composition-structure: Gamma ⊢ Compositon(A),
cubical-equiv: Equiv(T;A),
face-term-implies: Gamma ⊢ (phi ⇒ psi),
context-subset: Gamma, phi,
face-1: 1(𝔽),
face-type: 𝔽,
cubical-term: {X ⊢ _:A},
cubical-type: {X ⊢ _},
cubical_set: CubicalSet,
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
equal: s = t ∈ T
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
uimplies: b supposing a,
subtype_rel: A ⊆r B,
prop: ℙ
Lemmas referenced :
glue-comp-agrees,
composition-structure-subset,
context-subset_wf,
face-1-implies-subset,
face-term-implies_wf,
face-1_wf,
istype-cubical-term,
cubical-equiv_wf,
thin-context-subset,
composition-structure_wf,
cubical-type_wf,
face-type_wf,
cubical_set_cumulativity-i-j,
cubical_set_wf
Rules used in proof :
cut,
introduction,
extract_by_obid,
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation_alt,
hypothesis,
sqequalHypSubstitution,
isectElimination,
thin,
hypothesisEquality,
applyEquality,
independent_isectElimination,
because_Cache,
sqequalRule,
universeIsType,
instantiate
Latex:
\mforall{}[G:j\mvdash{}]. \mforall{}[A:\{G \mvdash{} \_\}]. \mforall{}[cA:G +\mvdash{} Compositon(A)]. \mforall{}[psi:\{G \mvdash{} \_:\mBbbF{}\}]. \mforall{}[T:\{G, psi \mvdash{} \_\}].
\mforall{}[cT:G, psi +\mvdash{} Compositon(T)]. \mforall{}[f:\{G, psi \mvdash{} \_:Equiv(T;A)\}].
comp(Glue [psi \mvdash{}\mrightarrow{} (T, f)] A) = cT supposing G \mvdash{} (1(\mBbbF{}) {}\mRightarrow{} psi)
Date html generated:
2020_05_20-PM-07_04_00
Last ObjectModification:
2020_04_21-PM-11_52_26
Theory : cubical!type!theory
Home
Index