---

Step * 1 of Lemma comp-universe-term


1. G : CubicalSet{j}
2. compOp(encode(c𝕌;univ-comp{i:l}())) = univ-comp{i:l}() ∈ G ⊢ CompOp(c𝕌)
⊢ encode(c𝕌;univ-comp{i:l}()) ~ encode(c𝕌;univ-comp{i:l}())
BY
{ (RepUR ``universe-encode`` 0 THEN RWO "csm-univ-comp csm-cubical-universe" 0 THEN Auto) }

---

Latex:

---

Latex:

1.  G  :  CubicalSet\{j\}
2.  compOp(encode(c\mBbbU{};univ-comp\{i:l\}()))  =  univ-comp\{i:l\}()
\mvdash{}  encode(c\mBbbU{};univ-comp\{i:l\}())  \msim{}  encode(c\mBbbU{};univ-comp\{i:l\}())


By

---

Latex:
(RepUR  ``universe-encode``  0  THEN  RWO  "csm-univ-comp  csm-cubical-universe"  0  THEN  Auto)

---

Home Index