---

Step * of Lemma univ-comp-sq

No Annotations
∀[G:Top]. (univ-comp{i:l}() ~ cfun-to-cop(G;c𝕌;compU()))
BY
{ (Intro
   THEN 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 closed-cubical-universe`` 0 THEN RepUR ``closed-type-to-type`` 0)
   THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[G:Top].  (univ-comp\{i:l\}()  \msim{}  cfun-to-cop(G;c\mBbbU{};compU()))


By

---

Latex:
(Intro
  THEN  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  closed-cubical-universe``  0
              THEN  RepUR  ``closed-type-to-type``  0
              )
  THEN  Auto)

---

Home Index