Nuprl Lemma : glue-term_wf2
∀[Gamma:j⊢]. ∀[A:{Gamma ⊢ _}]. ∀[phi:{Gamma ⊢ _:𝔽}]. ∀[T:{Gamma, phi ⊢ _}]. ∀[w:{Gamma, phi ⊢ _:(T ⟶ A)}].
∀[t:{Gamma, phi ⊢ _:T}]. ∀[a:{Gamma ⊢ _:A[phi |⟶ app(w; t)]}].
(glue [phi ⊢→ t] a ∈ {Gamma ⊢ _:Glue [phi ⊢→ (T;w)] A[phi |⟶ t]})
Proof
Definitions occuring in Statement :
glue-term: glue [phi ⊢→ t] a,
glue-type: Glue [phi ⊢→ (T;w)] A,
constrained-cubical-term: {Gamma ⊢ _:A[phi |⟶ t]},
context-subset: Gamma, phi,
face-type: 𝔽,
cubical-app: app(w; u),
cubical-fun: (A ⟶ B),
cubical-term: {X ⊢ _:A},
cubical-type: {X ⊢ _},
cubical_set: CubicalSet,
uall: ∀[x:A]. B[x],
member: t ∈ T
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
constrained-cubical-term: {Gamma ⊢ _:A[phi |⟶ t]},
same-cubical-type: Gamma ⊢ A = B,
subtype_rel: A ⊆r B,
same-cubical-term: X ⊢ u=v:A,
uimplies: b supposing a
Lemmas referenced :
glue-term_wf,
glue-type-constraint,
constrained-cubical-term_wf,
cubical-type-cumulativity2,
cubical_set_cumulativity-i-j,
cubical-app_wf_fun,
context-subset_wf,
thin-context-subset,
istype-cubical-term,
cubical-fun_wf,
cubical-type_wf,
face-type_wf,
cubical_set_wf,
glue-term-constraint,
cubical-term-eqcd,
context-subset-term-subtype,
glue-type_wf
Rules used in proof :
cut,
introduction,
extract_by_obid,
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation_alt,
hypothesis,
sqequalHypSubstitution,
isectElimination,
thin,
hypothesisEquality,
dependent_set_memberEquality_alt,
equalityTransitivity,
equalitySymmetry,
because_Cache,
universeIsType,
instantiate,
applyEquality,
sqequalRule,
Error :memTop,
independent_isectElimination,
lambdaEquality_alt,
cumulativity,
universeEquality,
hyp_replacement,
equalityIstype
Latex:
\mforall{}[Gamma:j\mvdash{}]. \mforall{}[A:\{Gamma \mvdash{} \_\}]. \mforall{}[phi:\{Gamma \mvdash{} \_:\mBbbF{}\}]. \mforall{}[T:\{Gamma, phi \mvdash{} \_\}].
\mforall{}[w:\{Gamma, phi \mvdash{} \_:(T {}\mrightarrow{} A)\}]. \mforall{}[t:\{Gamma, phi \mvdash{} \_:T\}]. \mforall{}[a:\{Gamma \mvdash{} \_:A[phi |{}\mrightarrow{} app(w; t)]\}].
(glue [phi \mvdash{}\mrightarrow{} t] a \mmember{} \{Gamma \mvdash{} \_:Glue [phi \mvdash{}\mrightarrow{} (T;w)] A[phi |{}\mrightarrow{} t]\})
Date html generated:
2020_05_20-PM-05_44_49
Last ObjectModification:
2020_04_21-PM-07_03_55
Theory : cubical!type!theory
Home
Index