---

Step * of Lemma path-type-q-csm-adjoin

No Annotations
∀[X,H:j⊢]. ∀[s:H j⟶ X]. ∀[A:{X ⊢ _}]. ∀[a:{X ⊢ _:A}]. ∀[u:{H ⊢ _:(A)s}].
  (((Path_(A)p (a)p q))(s;u) = (H ⊢ Path_(A)s (a)s u) ∈ {H ⊢ _})
BY
{ Auto }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[X,H:j\mvdash{}].  \mforall{}[s:H  j{}\mrightarrow{}  X].  \mforall{}[A:\{X  \mvdash{}  \_\}].  \mforall{}[a:\{X  \mvdash{}  \_:A\}].  \mforall{}[u:\{H  \mvdash{}  \_:(A)s\}].
    (((Path\_(A)p  (a)p  q))(s;u)  =  (H  \mvdash{}  Path\_(A)s  (a)s  u))


By

---

Latex:
Auto

---

Home Index