---

Step * of Lemma paths-equal-eta

No Annotations
∀[X:j⊢]. ∀[A:{X ⊢ _}]. ∀[a,b:{X ⊢ _:A}]. ∀[p:{X ⊢ _:(Path_A a b)}]. ∀[q:{X ⊢ _:Path(A)}].
  p = q ∈ {X ⊢ _:(Path_A a b)} supposing path-eta(p) = path-eta(q) ∈ {X.𝕀 ⊢ _:(A)p}
BY
{ (InstLemma `paths-equal` [] THEN RepeatFor 7 (ParallelLast') THEN BLemma `equal-paths-eta` THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[X:j\mvdash{}].  \mforall{}[A:\{X  \mvdash{}  \_\}].  \mforall{}[a,b:\{X  \mvdash{}  \_:A\}].  \mforall{}[p:\{X  \mvdash{}  \_:(Path\_A  a  b)\}].  \mforall{}[q:\{X  \mvdash{}  \_:Path(A)\}].
    p  =  q  supposing  path-eta(p)  =  path-eta(q)


By

---

Latex:
(InstLemma  `paths-equal`  []
  THEN  RepeatFor  7  (ParallelLast')
  THEN  BLemma  `equal-paths-eta`
  THEN  Auto)

---

Home Index