---

Step * of Lemma decode-universe-term

No Annotations
∀[G:j⊢]. (decode(t𝕌) = c𝕌 ∈ {G ⊢' _})
BY
{ (Intro
   THEN Unfolds ``universe-term`` 0
   THEN (InstLemma `universe-decode-encode` [⌜parm{j}⌝;⌜parm{i'}⌝;⌜G⌝;⌜c𝕌⌝;⌜univ-comp{i:l}()⌝]⋅ THENA Auto)
   THEN NthHypSq (-1)
   THEN RepeatFor 2 (EqCD)) }

1
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}())

---

Latex:

---

Latex:
No  Annotations
\mforall{}[G:j\mvdash{}].  (decode(t\mBbbU{})  =  c\mBbbU{})


By

---

Latex:
(Intro
  THEN  Unfolds  ``universe-term``  0
  THEN  (InstLemma  `universe-decode-encode`  [\mkleeneopen{}parm\{j\}\mkleeneclose{};\mkleeneopen{}parm\{i'\}\mkleeneclose{};\mkleeneopen{}G\mkleeneclose{};\mkleeneopen{}c\mBbbU{}\mkleeneclose{};\mkleeneopen{}univ-comp\{i:l\}()\mkleeneclose{}]\mcdot{}
              THENA  Auto
              )
  THEN  NthHypSq  (-1)
  THEN  RepeatFor  2  (EqCD))

---

Home Index