---

Step * of Lemma path-eta-0

∀[G,pth:Top].  ((path-eta(pth))[0(𝕀)] ~ pth @ 0(𝕀))
BY
{ (RWO  "path-eta-id-adjoin" 0 THEN Auto) }

---

Latex:

---

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


By

---

Latex:
(RWO    "path-eta-id-adjoin"  0  THEN  Auto)

---

Home Index