---

Step * of Lemma path-eta-1

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

---

Latex:

---

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


By

---

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

---

Home Index