---

Step * 1 of Lemma decode-universe-term


1. G : CubicalSet{j}
2. decode(encode(c𝕌;univ-comp{i:l}())) = c𝕌 ∈ {G ⊢' _}
⊢ 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.  decode(encode(c\mBbbU{};univ-comp\{i:l\}()))  =  c\mBbbU{}
\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