---

Step * of Lemma glue-type-term-subtype2

No Annotations
∀[Gamma:j⊢]. ∀[psi:{Gamma ⊢ _:𝔽}]. ∀[A:{Gamma, psi ⊢ _}]. ∀[phi:{Gamma, psi ⊢ _:𝔽}]. ∀[T:{Gamma, psi, phi ⊢ _}].
∀[w:{Gamma, psi, phi ⊢ _:(T ⟶ A)}].
  ({Gamma, psi ⊢ _:Glue [phi ⊢→ (T;w)] A} ⊆r {Gamma, psi, phi ⊢ _:T})
BY
{ (Intros THEN (InstLemma `glue-type-term-subtype` [⌜Gamma, psi⌝;⌜A⌝;⌜phi⌝;⌜T⌝;⌜w⌝]⋅ THENA Auto)) }

1
1. [Gamma] : CubicalSet{j}
2. [psi] : {Gamma ⊢ _:𝔽}
3. [A] : {Gamma, psi ⊢ _}
4. [phi] : {Gamma, psi ⊢ _:𝔽}
5. [T] : {Gamma, psi, phi ⊢ _}
6. [w] : {Gamma, psi, phi ⊢ _:(T ⟶ A)}
7. {Gamma, psi ⊢ _:Glue [phi ⊢→ (T;w)] A} ⊆r {Gamma, psi, phi ⊢ _:T}
⊢ {Gamma, psi ⊢ _:Glue [phi ⊢→ (T;w)] A} ⊆r {Gamma, psi, phi ⊢ _:T}

---

Latex:

---

Latex:
No  Annotations
\mforall{}[Gamma:j\mvdash{}].  \mforall{}[psi:\{Gamma  \mvdash{}  \_:\mBbbF{}\}].  \mforall{}[A:\{Gamma,  psi  \mvdash{}  \_\}].  \mforall{}[phi:\{Gamma,  psi  \mvdash{}  \_:\mBbbF{}\}].
\mforall{}[T:\{Gamma,  psi,  phi  \mvdash{}  \_\}].  \mforall{}[w:\{Gamma,  psi,  phi  \mvdash{}  \_:(T  {}\mrightarrow{}  A)\}].
    (\{Gamma,  psi  \mvdash{}  \_:Glue  [phi  \mvdash{}\mrightarrow{}  (T;w)]  A\}  \msubseteq{}r  \{Gamma,  psi,  phi  \mvdash{}  \_:T\})


By

---

Latex:
(Intros  THEN  (InstLemma  `glue-type-term-subtype`  [\mkleeneopen{}Gamma,  psi\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}phi\mkleeneclose{};\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}w\mkleeneclose{}]\mcdot{}  THENA  Auto))

---

Home Index