Nuprl Lemma : csm-glue-comp-agrees
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).⋅
∀[H,G:j⊢]. ∀[tau:H j⟶ G]. ∀[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) )tau = (cT)tau ∈ H ⊢ Compositon((T)tau) supposing H ⊢ (1(𝔽) ⇒ (psi)tau)
Proof
Definitions occuring in Statement :
glue-comp: comp(Glue [phi ⊢→ (T, f)] A) ,
csm-comp-structure: (cA)tau,
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: 𝔽,
csm-ap-term: (t)s,
cubical-term: {X ⊢ _:A},
csm-ap-type: (AF)s,
cubical-type: {X ⊢ _},
cube_set_map: A ⟶ B,
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],
uimplies: b supposing a,
member: t ∈ T,
subtype_rel: A ⊆r B,
csm-comp-structure: (cA)tau,
cubical-type: {X ⊢ _},
csm-ap-term: (t)s,
interval-type: 𝕀,
csm-comp: G o F,
csm-ap-type: (AF)s,
compose: f o g,
csm-ap: (s)x,
prop: ℙ
Lemmas referenced :
csm-glue-comp,
csm-comp-structure_wf,
context-subset_wf,
csm-ap-term_wf,
face-type_wf,
csm-face-type,
context-subset-map,
cubical_set_cumulativity-i-j,
cube_set_map_cumulativity-i-j,
glue-comp-agrees2,
csm-ap-type_wf,
face-term-implies_wf,
face-1_wf,
istype-cubical-term,
cubical-equiv_wf,
thin-context-subset,
composition-structure_wf,
cubical-type_wf,
cube_set_map_wf,
cubical_set_wf,
cubical-term-eqcd,
csm-cubical-equiv
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation_alt,
sqequalRule,
cut,
introduction,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
because_Cache,
Error :memTop,
hypothesisEquality,
hypothesis,
instantiate,
applyEquality,
equalityTransitivity,
equalitySymmetry,
setElimination,
rename,
productElimination,
independent_isectElimination,
universeIsType,
inhabitedIsType,
lambdaEquality_alt,
hyp_replacement
Latex:
\mforall{}[H,G:j\mvdash{}]. \mforall{}[tau:H j{}\mrightarrow{} G]. \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) )tau = (cT)tau supposing H \mvdash{} (1(\mBbbF{}) {}\mRightarrow{} (psi)tau)
Date html generated:
2020_05_20-PM-07_04_31
Last ObjectModification:
2020_04_21-PM-11_55_31
Theory : cubical!type!theory
Home
Index