---

Step * of Lemma cubical-equiv-subset

∀[X,T,A,phi:Top].  (Equiv(T;A) ~ Equiv(T;A))
BY
{ (RepUR ``cubical-equiv is-cubical-equiv`` 0
   THEN (RWW "cubical-sigma-subset cubical-fun-subset cubical-pi-subset" 0 THENA Auto)
   THEN (UnivCD THENA Auto)
   THEN RepeatFor 2 ((EqCD THEN Try (Trivial)))
   THEN (RWO  "contractible-type-subset2" 0 THENA Auto)
   THEN EqCD
   THEN Try (Trivial)) }

1
1. X : Top
2. T : Top
3. A : Top
4. phi : Top
⊢ X, phi.(T ⟶ A).(A)p ⊢ Fiber((q)p;q) ~ X.(T ⟶ A).(A)p ⊢ Fiber((q)p;q)

---

Latex:

---

Latex:
\mforall{}[X,T,A,phi:Top].    (Equiv(T;A)  \msim{}  Equiv(T;A))


By

---

Latex:
(RepUR  ``cubical-equiv  is-cubical-equiv``  0
  THEN  (RWW  "cubical-sigma-subset  cubical-fun-subset  cubical-pi-subset"  0  THENA  Auto)
  THEN  (UnivCD  THENA  Auto)
  THEN  RepeatFor  2  ((EqCD  THEN  Try  (Trivial)))
  THEN  (RWO    "contractible-type-subset2"  0  THENA  Auto)
  THEN  EqCD
  THEN  Try  (Trivial))

---

Home Index