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