---

Step * of Lemma comp-universe-term

No Annotations
∀[G:j⊢]. (compOp(t𝕌) = univ-comp{i:l}() ∈ G ⊢ CompOp(c𝕌))
BY
{ (Intro
   THEN Unfolds ``universe-term`` 0
   THEN (InstLemma `universe-comp-op-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. 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}())

---

Latex:

---

Latex:
No  Annotations
\mforall{}[G:j\mvdash{}].  (compOp(t\mBbbU{})  =  univ-comp\{i:l\}())


By

---

Latex:
(Intro
  THEN  Unfolds  ``universe-term``  0
  THEN  (InstLemma  `universe-comp-op-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