---

Step * of Lemma glue-term-1'

No Annotations
∀[Gamma:j⊢]. ∀[phi:{Gamma ⊢ _:𝔽}]. ∀[T:{Gamma ⊢ _}]. ∀[t:{Gamma ⊢ _:T}]. ∀[A,a:Top].
  Gamma ⊢ glue [phi ⊢→ t] a = t ∈ {Gamma ⊢ _:T} supposing phi = 1(𝔽) ∈ {Gamma ⊢ _:𝔽}
BY
{ (InstLemma `glue-term-constraint` [] THEN RepeatFor 6 (ParallelLast') THEN Auto) }

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

---

Latex:

---

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


By

---

Latex:
(InstLemma  `glue-term-constraint`  []  THEN  RepeatFor  6  (ParallelLast')  THEN  Auto)

---

Home Index