---

Step * of Lemma contractible-type-subset

∀[X,A,phi:Top].  (X, phi ⊢ Contractible(A) ~ X ⊢ Contractible(A))
BY
{ ((UnivCD THENA Auto)
   THEN RepUR ``contractible-type cubical-sigma cubical-pi`` 0
   THEN ((RepUR ``cubical-pi-family path-type cubical-subset pathtype`` 0
          THEN RepUR ``cubical-fun cubical-fun-family`` 0
          )
         THEN RepUR ``context-subset cube-context-adjoin`` 0
         )
   THEN EqCD) }

---

Latex:

---

Latex:
\mforall{}[X,A,phi:Top].    (X,  phi  \mvdash{}  Contractible(A)  \msim{}  X  \mvdash{}  Contractible(A))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  RepUR  ``contractible-type  cubical-sigma  cubical-pi``  0
  THEN  ((RepUR  ``cubical-pi-family  path-type  cubical-subset  pathtype``  0
                THEN  RepUR  ``cubical-fun  cubical-fun-family``  0
                )
              THEN  RepUR  ``context-subset  cube-context-adjoin``  0
              )
  THEN  EqCD)

---

Home Index