---

Step * of Lemma cu-cube-family-Kan-type-at

∀[alpha,L,f:Top].  (cu-cube-family(alpha;L;f) ~ Kan-type(alpha)(f))
BY
{ (RepUR ``Kan-type cubical-type-at cu-cube-family`` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[alpha,L,f:Top].    (cu-cube-family(alpha;L;f)  \msim{}  Kan-type(alpha)(f))


By

---

Latex:
(RepUR  ``Kan-type  cubical-type-at  cu-cube-family``  0  THEN  Auto)

---

Home Index