---

Step * of Lemma contractible-type-at

∀[X,A,I,rho:Top].  (Contractible(A)(rho) ~ u:A(rho) × cubical-pi-family(X.A;(A)p;(Path_((A)p)p (q)p q);I;(rho;u)))
BY
{ (Auto THEN RepUR ``contractible-type cubical-sigma cubical-pi`` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[X,A,I,rho:Top].
    (Contractible(A)(rho)  \msim{}  u:A(rho)  \mtimes{}  cubical-pi-family(X.A;(A)p;(Path\_((A)p)p  (q)p  q);I;(rho;u)))


By

---

Latex:
(Auto  THEN  RepUR  ``contractible-type  cubical-sigma  cubical-pi``  0  THEN  Auto)

---

Home Index