---

Step * 1 2 1 1 2 1 1 1 1 1 1 1 1 2 of Lemma universe-encode-decode


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. universe-type(t;I;a) = universe-type(encode(decode(t);compOp(t));I;a) ∈ {formal-cube(I) ⊢ _}
11. snd(t(a)) ∈ formal-cube(I) ⊢ CompOp(universe-type(t;I;a))
12. (compOp(t))<a> ∈ formal-cube(I) ⊢ CompOp(universe-type(t;I;a))
13. J : fset(ℕ)
14. i : {i:ℕ| ¬i ∈ J} 
15. f : J+i ⟶ I
16. phi : 𝔽(J)
17. u : {J+i,s(phi) ⊢ _:(universe-type(t;I;a))<f> o iota}
18. a0 : cubical-path-0(formal-cube(I);universe-type(t;I;a);J;i;f;phi;u)
19. (t(a) a f) = t(f(a)) ∈ (A:{formal-cube(J+i) ⊢ _} × formal-cube(J+i) ⊢ CompOp(A))
20. (t(a) a f)
= t(f(a))
∈ {z:A:{formal-cube(J+i) ⊢ _} × formal-cube(J+i) ⊢ CompOp(A)| 
   (z = (t(a) a f) ∈ (A:{formal-cube(J+i) ⊢ _} × formal-cube(J+i) ⊢ CompOp(A)))
   ∧ (z = t(f(a)) ∈ (A:{formal-cube(J+i) ⊢ _} × formal-cube(J+i) ⊢ CompOp(A)))} 
21. (snd((t(a) a f))) = (snd(t(f(a)))) ∈ formal-cube(J+i) ⊢ CompOp(universe-type(t;J+i;f(a)))
⊢ ((snd(t(a))) J i f phi u a0) = ((snd(t(f(a)))) J i 1 phi u a0) ∈ universe-type(t;I;a)((i1)(f))
BY
{ (MoveToConcl (-1) THEN (RWO "cubical-universe-at" 5 THENA Auto) THEN (GenConclTerm ⌜t(a)⌝⋅ THENA Auto)) }

1
1. X : CubicalSet{j}
2. t : {X ⊢ _:c𝕌}
3. I : fset(ℕ)
4. a : X(I)
5. t(a) ∈ A:{formal-cube(I) ⊢ _} × formal-cube(I) ⊢ CompOp(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. universe-type(t;I;a) = universe-type(encode(decode(t);compOp(t));I;a) ∈ {formal-cube(I) ⊢ _}
11. snd(t(a)) ∈ formal-cube(I) ⊢ CompOp(universe-type(t;I;a))
12. (compOp(t))<a> ∈ formal-cube(I) ⊢ CompOp(universe-type(t;I;a))
13. J : fset(ℕ)
14. i : {i:ℕ| ¬i ∈ J} 
15. f : J+i ⟶ I
16. phi : 𝔽(J)
17. u : {J+i,s(phi) ⊢ _:(universe-type(t;I;a))<f> o iota}
18. a0 : cubical-path-0(formal-cube(I);universe-type(t;I;a);J;i;f;phi;u)
19. (t(a) a f) = t(f(a)) ∈ (A:{formal-cube(J+i) ⊢ _} × formal-cube(J+i) ⊢ CompOp(A))
20. (t(a) a f)
= t(f(a))
∈ {z:A:{formal-cube(J+i) ⊢ _} × formal-cube(J+i) ⊢ CompOp(A)| 
   (z = (t(a) a f) ∈ (A:{formal-cube(J+i) ⊢ _} × formal-cube(J+i) ⊢ CompOp(A)))
   ∧ (z = t(f(a)) ∈ (A:{formal-cube(J+i) ⊢ _} × formal-cube(J+i) ⊢ CompOp(A)))} 
21. v : A:{formal-cube(I) ⊢ _} × formal-cube(I) ⊢ CompOp(A)
22. t(a) = v ∈ (A:{formal-cube(I) ⊢ _} × formal-cube(I) ⊢ CompOp(A))
⊢ ((snd((v a f))) = (snd(t(f(a)))) ∈ formal-cube(J+i) ⊢ CompOp(universe-type(t;J+i;f(a))))
⇒ (((snd(v)) J i f phi u a0) = ((snd(t(f(a)))) J i 1 phi u a0) ∈ universe-type(t;I;a)((i1)(f)))

---

Latex:

---

Latex:

1.  X  :  CubicalSet\{j\}
2.  t  :  \{X  \mvdash{}  \_:c\mBbbU{}\}
3.  I  :  fset(\mBbbN{})
4.  a  :  X(I)
5.  t(a)  \mmember{}  c\mBbbU{}(a)
6.  X  \mvdash{}  decode(t)
7.  compOp(t)  \mmember{}  X  \mvdash{}  CompOp(decode(t))
8.  encode(decode(t);compOp(t))  \mmember{}  \{X  \mvdash{}  \_:c\mBbbU{}\}
9.  encode(decode(t);compOp(t))(a)  \mmember{}  c\mBbbU{}(a)
10.  universe-type(t;I;a)  =  universe-type(encode(decode(t);compOp(t));I;a)
11.  snd(t(a))  \mmember{}  formal-cube(I)  \mvdash{}  CompOp(universe-type(t;I;a))
12.  (compOp(t))<a>  \mmember{}  formal-cube(I)  \mvdash{}  CompOp(universe-type(t;I;a))
13.  J  :  fset(\mBbbN{})
14.  i  :  \{i:\mBbbN{}|  \mneg{}i  \mmember{}  J\} 
15.  f  :  J+i  {}\mrightarrow{}  I
16.  phi  :  \mBbbF{}(J)
17.  u  :  \{J+i,s(phi)  \mvdash{}  \_:(universe-type(t;I;a))<f>  o  iota\}
18.  a0  :  cubical-path-0(formal-cube(I);universe-type(t;I;a);J;i;f;phi;u)
19.  (t(a)  a  f)  =  t(f(a))
20.  (t(a)  a  f)  =  t(f(a))
21.  (snd((t(a)  a  f)))  =  (snd(t(f(a))))
\mvdash{}  ((snd(t(a)))  J  i  f  phi  u  a0)  =  ((snd(t(f(a))))  J  i  1  phi  u  a0)


By

---

Latex:
(MoveToConcl  (-1)
  THEN  (RWO  "cubical-universe-at"  5  THENA  Auto)
  THEN  (GenConclTerm  \mkleeneopen{}t(a)\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index