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