---

Step * 1 of Lemma cubical-equiv-subset


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)
BY
{ ((RWO  "cubical-fiber-subset-adjoin2" 0 THENA Auto) THEN EqCD THEN Try (Trivial)) }

---

Latex:

---

Latex:

1.  X  :  Top
2.  T  :  Top
3.  A  :  Top
4.  phi  :  Top
\mvdash{}  X,  phi.(T  {}\mrightarrow{}  A).(A)p  \mvdash{}  Fiber((q)p;q)  \msim{}  X.(T  {}\mrightarrow{}  A).(A)p  \mvdash{}  Fiber((q)p;q)


By

---

Latex:
((RWO    "cubical-fiber-subset-adjoin2"  0  THENA  Auto)  THEN  EqCD  THEN  Try  (Trivial))

---

Home Index