---

Step * of Lemma cubical-fiber-at

∀[X,T,A,w,a,I,rho:Top].  (Fiber(w;a)(rho) ~ u:T(rho) × (Path_(A)p (a)p app((w)p; q))((rho;u)))
BY
{ ((Auto THEN RepUR ``cubical-type-at cubical-fiber cubical-sigma `` 0) THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[X,T,A,w,a,I,rho:Top].    (Fiber(w;a)(rho)  \msim{}  u:T(rho)  \mtimes{}  (Path\_(A)p  (a)p  app((w)p;  q))((rho;u)))


By

---

Latex:
((Auto  THEN  RepUR  ``cubical-type-at  cubical-fiber  cubical-sigma  ``  0)  THEN  Auto)

---

Home Index