---

Step * of Lemma glue-type-1

No Annotations
∀[Gamma:j⊢]. ∀[A:{Gamma ⊢ _}]. ∀[T:{Gamma, 1(𝔽) ⊢ _}]. ∀[w:{Gamma, 1(𝔽) ⊢ _:(T ⟶ A)}].
  (Gamma ⊢ Glue [1(𝔽) ⊢→ (T;w)] A = T ∈ {Gamma ⊢ _})
BY
{ (InstLemma `glue-type-constraint` []
   THEN RepeatFor 2 (ParallelLast')
   THEN (D -1 With ⌜1(𝔽)⌝  THENA Auto)
   THEN RepeatFor 2 (ParallelLast')
   THEN Unfold `same-cubical-type` -1
   THEN SubsumeC ⌜{Gamma, 1(𝔽) ⊢ _}⌝⋅
   THEN Auto) }

---

Latex:

---

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


By

---

Latex:
(InstLemma  `glue-type-constraint`  []
  THEN  RepeatFor  2  (ParallelLast')
  THEN  (D  -1  With  \mkleeneopen{}1(\mBbbF{})\mkleeneclose{}    THENA  Auto)
  THEN  RepeatFor  2  (ParallelLast')
  THEN  Unfold  `same-cubical-type`  -1
  THEN  SubsumeC  \mkleeneopen{}\{Gamma,  1(\mBbbF{})  \mvdash{}  \_\}\mkleeneclose{}\mcdot{}
  THEN  Auto)

---

Home Index