---

Step * of Lemma csm-univ-comp

No Annotations
∀[s:Top]. ((univ-comp{i:l}())s ~ univ-comp{i:l}())
BY
{ (RepUR ``univ-comp comp-fun-to-comp-op comp-fun-to-comp-op1`` 0
   THEN RepUR ``canonical-section context-map csm-ap-type csm-composition`` 0
   THEN RepUR ``compU cubical-universe`` 0
   THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[s:Top].  ((univ-comp\{i:l\}())s  \msim{}  univ-comp\{i:l\}())


By

---

Latex:
(RepUR  ``univ-comp  comp-fun-to-comp-op  comp-fun-to-comp-op1``  0
  THEN  RepUR  ``canonical-section  context-map  csm-ap-type  csm-composition``  0
  THEN  RepUR  ``compU  cubical-universe``  0
  THEN  Auto)

---

Home Index