---

Step * 1 of Lemma universe-encode-decode


1. X : CubicalSet{j}
2. t : {X ⊢ _:c𝕌}
3. I : fset(ℕ)
4. a : X(I)
⊢ t(a) = encode(decode(t);compOp(t))(a) ∈ c𝕌(a)
BY
{ ((Assert t(a) ∈ c𝕌(a) BY
          Auto)
   THEN (InstLemma `universe-decode_wf` [⌜X⌝;⌜t⌝]⋅ THENA Auto)
   THEN (InstLemma `universe-comp-op_wf` [⌜X⌝;⌜t⌝]⋅ THENA Auto)
   THEN (InstLemma `universe-encode_wf` [⌜X⌝;⌜decode(t)⌝;⌜compOp(t)⌝]⋅ THENA Auto)
   THEN (Assert encode(decode(t);compOp(t))(a) ∈ c𝕌(a) BY
               (MemCD THEN Auto))
   THEN BLemma `cubical-universe-at-equal`
   THEN Auto) }

1
1. X : CubicalSet{j}
2. t : {X ⊢ _:c𝕌}
3. I : fset(ℕ)
4. a : X(I)
5. t(a) ∈ c𝕌(a)
6. X ⊢ decode(t)
7. compOp(t) ∈ X ⊢ CompOp(decode(t))
8. encode(decode(t);compOp(t)) ∈ {X ⊢ _:c𝕌}
9. encode(decode(t);compOp(t))(a) ∈ c𝕌(a)
⊢ (fst(t(a))) = (fst(encode(decode(t);compOp(t))(a))) ∈ {formal-cube(I) ⊢ _}

2
1. X : CubicalSet{j}
2. t : {X ⊢ _:c𝕌}
3. I : fset(ℕ)
4. a : X(I)
5. t(a) ∈ c𝕌(a)
6. X ⊢ decode(t)
7. compOp(t) ∈ X ⊢ CompOp(decode(t))
8. encode(decode(t);compOp(t)) ∈ {X ⊢ _:c𝕌}
9. encode(decode(t);compOp(t))(a) ∈ c𝕌(a)
10. (fst(t(a))) = (fst(encode(decode(t);compOp(t))(a))) ∈ {formal-cube(I) ⊢ _}
⊢ (snd(t(a))) = (snd(encode(decode(t);compOp(t))(a))) ∈ formal-cube(I) ⊢ CompOp(fst(t(a)))

---

Latex:

---

Latex:

1.  X  :  CubicalSet\{j\}
2.  t  :  \{X  \mvdash{}  \_:c\mBbbU{}\}
3.  I  :  fset(\mBbbN{})
4.  a  :  X(I)
\mvdash{}  t(a)  =  encode(decode(t);compOp(t))(a)


By

---

Latex:
((Assert  t(a)  \mmember{}  c\mBbbU{}(a)  BY
                Auto)
  THEN  (InstLemma  `universe-decode\_wf`  [\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}t\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `universe-comp-op\_wf`  [\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}t\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `universe-encode\_wf`  [\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}decode(t)\mkleeneclose{};\mkleeneopen{}compOp(t)\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (Assert  encode(decode(t);compOp(t))(a)  \mmember{}  c\mBbbU{}(a)  BY
                          (MemCD  THEN  Auto))
  THEN  BLemma  `cubical-universe-at-equal`
  THEN  Auto)

---

Home Index