Nuprl Lemma : glue-comp_wf3
∀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) ∈ G ⊢ Compositon(gluetype(G;A;psi;T;f)))
Proof
Definitions occuring in Statement :
gluetype: gluetype(Gamma;A;phi;T;f),
glue-comp: comp(Glue [phi ⊢→ (T, f)] A) ,
composition-structure: Gamma ⊢ Compositon(A),
cubical-equiv: Equiv(T;A),
context-subset: Gamma, phi,
face-type: 𝔽,
cubical-term: {X ⊢ _:A},
cubical-type: {X ⊢ _},
cubical_set: CubicalSet,
all: ∀x:A. B[x],
member: t ∈ T
Definitions unfolded in proof :
gluetype: gluetype(Gamma;A;phi;T;f)
Lemmas referenced :
glue-comp_wf2
Rules used in proof :
cut,
introduction,
extract_by_obid,
sqequalHypSubstitution,
sqequalSubstitution,
sqequalRule,
sqequalReflexivity,
sqequalTransitivity,
computationStep,
hypothesis
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) \mmember{} G \mvdash{} Compositon(gluetype(G;A;psi;T;f)))
Date html generated:
2020_05_20-PM-07_05_15
Last ObjectModification:
2020_04_25-AM-11_22_11
Theory : cubical!type!theory
Home
Index