---

Step * of Lemma face-type-ap-morph-ps

∀[I,J,f,rho,u:Top].  ((u rho f) ~ (u)<f>)
BY
{ (Auto
   THEN RepUR ``presheaf-type-ap-morph face-type constant-cubical-type`` 0
   THEN RepUR ``cube-set-restriction face-presheaf`` 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[I,J,f,rho,u:Top].    ((u  rho  f)  \msim{}  (u)<f>)


By

---

Latex:
(Auto
  THEN  RepUR  ``presheaf-type-ap-morph  face-type  constant-cubical-type``  0
  THEN  RepUR  ``cube-set-restriction  face-presheaf``  0
  THEN  Auto)

---

Home Index