---

Step * of Lemma glue-term-constraint

No Annotations
∀[Gamma:j⊢]. ∀[phi:{Gamma ⊢ _:𝔽}]. ∀[T:{Gamma, phi ⊢ _}]. ∀[t:{Gamma, phi ⊢ _:T}]. ∀[A,a:Top].
  Gamma, phi ⊢ glue [phi ⊢→ t] a=t:T
BY
{ (Intros THEN Unfold `same-cubical-term` 0 THEN Symmetry THEN (CubicalTermEqual THENA Auto)) }

1
1. Gamma : CubicalSet{j}
2. phi : {Gamma ⊢ _:𝔽}
3. T : {Gamma, phi ⊢ _}
4. t : {Gamma, phi ⊢ _:T}
5. A : Top
6. a : Top
7. I : fset(ℕ)
8. a1 : Gamma, phi(I)
⊢ (t I a1) = (glue [phi ⊢→ t] a I a1) ∈ T(a1)

---

Latex:

---

Latex:
No  Annotations
\mforall{}[Gamma:j\mvdash{}].  \mforall{}[phi:\{Gamma  \mvdash{}  \_:\mBbbF{}\}].  \mforall{}[T:\{Gamma,  phi  \mvdash{}  \_\}].  \mforall{}[t:\{Gamma,  phi  \mvdash{}  \_:T\}].  \mforall{}[A,a:Top].
    Gamma,  phi  \mvdash{}  glue  [phi  \mvdash{}\mrightarrow{}  t]  a=t:T


By

---

Latex:
(Intros  THEN  Unfold  `same-cubical-term`  0  THEN  Symmetry  THEN  (CubicalTermEqual  THENA  Auto))

---

Home Index