---

Step * 1 of Lemma universe-term_wf

.....equality..... 
1. G : CubicalSet{j}
⊢ 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:
.....equality..... 
1.  G  :  CubicalSet\{j\}
\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