---

Step * of Lemma equiv-fun-cubical-id-equiv

∀[G,A:Top].  (equiv-fun(IdEquiv(G;A)) ~ cubical-id-fun(G))
BY
{ (Intros
   THEN RepUR ``equiv-fun cubical-id-equiv cubical-id-fun cubical-lam`` 0
   THEN RepUR ``cubical-id-is-equiv equiv-witness cubical-lambda cubical-pair cubical-fst`` 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[G,A:Top].    (equiv-fun(IdEquiv(G;A))  \msim{}  cubical-id-fun(G))


By

---

Latex:
(Intros
  THEN  RepUR  ``equiv-fun  cubical-id-equiv  cubical-id-fun  cubical-lam``  0
  THEN  RepUR  ``cubical-id-is-equiv  equiv-witness  cubical-lambda  cubical-pair  cubical-fst``  0
  THEN  Auto)

---

Home Index