---

Step * of Lemma path-eta-id-adjoin

∀[G,u,pth:Top].  ((path-eta(pth))[u] ~ pth @ u)
BY
{ (Intros
   THEN RepUR ``path-eta`` 0
   THEN (RWO "csm-cubicalpath-app" 0 THENA Auto)
   THEN RepUR ``cubicalpath-app cubical-app`` 0
   THEN CsmUnfolding
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[G,u,pth:Top].    ((path-eta(pth))[u]  \msim{}  pth  @  u)


By

---

Latex:
(Intros
  THEN  RepUR  ``path-eta``  0
  THEN  (RWO  "csm-cubicalpath-app"  0  THENA  Auto)
  THEN  RepUR  ``cubicalpath-app  cubical-app``  0
  THEN  CsmUnfolding
  THEN  Auto)

---

Home Index