---

Step * of Lemma interval-type-ap-morph

∀[I,J,f,rho,u:Top].  ((u rho f) ~ dM-lift(J;I;f) u)
BY
{ (Auto
   THEN RepUR ``cubical-type-ap-morph interval-type constant-cubical-type`` 0
   THEN RWO "interval-presheaf-restriction" 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[I,J,f,rho,u:Top].    ((u  rho  f)  \msim{}  dM-lift(J;I;f)  u)


By

---

Latex:
(Auto
  THEN  RepUR  ``cubical-type-ap-morph  interval-type  constant-cubical-type``  0
  THEN  RWO  "interval-presheaf-restriction"  0
  THEN  Auto)

---

Home Index