---

Step * of Lemma contractible-type-subset2

∀[X,A,B,C,phi:Top].  (X, phi.B.C ⊢ Contractible(A) ~ X.B.C ⊢ Contractible(A))
BY
{ (((UnivCD THENA Auto) THEN Unfold `contractible-type` 0 THEN (RWO  "cubical-sigma-subset-adjoin2" 0 THENA Auto))
   THEN EqCD
   THEN Try (Trivial)
   THEN (RWO  "cubical-pi-subset-adjoin3" 0 THENA Auto)
   THEN EqCD
   THEN Try (Trivial)
   THEN (RWO  "path-type-subset-adjoin4" 0 THENA Auto)
   THEN EqCD
   THEN Try (Trivial)) }

---

Latex:

---

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


By

---

Latex:
(((UnivCD  THENA  Auto)
    THEN  Unfold  `contractible-type`  0
    THEN  (RWO    "cubical-sigma-subset-adjoin2"  0  THENA  Auto))
  THEN  EqCD
  THEN  Try  (Trivial)
  THEN  (RWO    "cubical-pi-subset-adjoin3"  0  THENA  Auto)
  THEN  EqCD
  THEN  Try  (Trivial)
  THEN  (RWO    "path-type-subset-adjoin4"  0  THENA  Auto)
  THEN  EqCD
  THEN  Try  (Trivial))

---

Home Index