Step
*
1
2
1
1
2
1
1
1
1
1
1
1
1
2
1
1
1
1
1
1
2
1
2
1
2
1
1
1
of Lemma
universe-encode-decode
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. A : {formal-cube(I) ⊢ _}
22. v1 : formal-cube(I) ⊢ CompOp(A)
23. t(a) = <A, v1> ∈ (A:{formal-cube(I) ⊢ _} × formal-cube(I) ⊢ CompOp(A))
24. (v1)<f> = (snd(t(f(a)))) ∈ formal-cube(J+i) ⊢ CompOp(universe-type(t;J+i;f(a)))
25. Z : formal-cube(J+i) ⊢ CompOp(universe-type(t;J+i;f(a)))
26. a1 : universe-type(t;I;a)((i0)(f))
27. J@0 : fset(ℕ)
28. f@0 : J,phi(J@0)
29. (universe-type(t;I;a))<f> = universe-type(t;J+i;f(a)) ∈ {formal-cube(J+i) ⊢ _}
30. (universe-type(t;I;a))<f>
= universe-type(t;J+i;f(a))
∈ {z:{formal-cube(J+i) ⊢ _}|
(z = (universe-type(t;I;a))<f> ∈ {formal-cube(J+i) ⊢ _}) ∧ (z = universe-type(t;J+i;f(a)) ∈ {formal-cube(J+i) ⊢ _})}
31. W : {z:{formal-cube(J+i) ⊢ _}|
(z = (universe-type(t;I;a))<f> ∈ {formal-cube(J+i) ⊢ _})
∧ (z = universe-type(t;J+i;f(a)) ∈ {formal-cube(J+i) ⊢ _})}
⊢ (a1 (i0)(1) f@0) ∈ universe-type(t;I;a)(f@0((i0)(f)))
BY
{ InferEqualTypeGen }
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. A : {formal-cube(I) ⊢ _}
22. v1 : formal-cube(I) ⊢ CompOp(A)
23. t(a) = <A, v1> ∈ (A:{formal-cube(I) ⊢ _} × formal-cube(I) ⊢ CompOp(A))
24. (v1)<f> = (snd(t(f(a)))) ∈ formal-cube(J+i) ⊢ CompOp(universe-type(t;J+i;f(a)))
25. Z : formal-cube(J+i) ⊢ CompOp(universe-type(t;J+i;f(a)))
26. a1 : universe-type(t;I;a)((i0)(f))
27. J@0 : fset(ℕ)
28. f@0 : J,phi(J@0)
29. (universe-type(t;I;a))<f> = universe-type(t;J+i;f(a)) ∈ {formal-cube(J+i) ⊢ _}
30. (universe-type(t;I;a))<f>
= universe-type(t;J+i;f(a))
∈ {z:{formal-cube(J+i) ⊢ _}|
(z = (universe-type(t;I;a))<f> ∈ {formal-cube(J+i) ⊢ _}) ∧ (z = universe-type(t;J+i;f(a)) ∈ {formal-cube(J+i) ⊢ _})}
31. W : {z:{formal-cube(J+i) ⊢ _}|
(z = (universe-type(t;I;a))<f> ∈ {formal-cube(J+i) ⊢ _})
∧ (z = universe-type(t;J+i;f(a)) ∈ {formal-cube(J+i) ⊢ _})}
⊢ W(f@0((i0)(1))) = universe-type(t;I;a)(f@0((i0)(f))) ∈ Type
2
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. A : {formal-cube(I) ⊢ _}
22. v1 : formal-cube(I) ⊢ CompOp(A)
23. t(a) = <A, v1> ∈ (A:{formal-cube(I) ⊢ _} × formal-cube(I) ⊢ CompOp(A))
24. (v1)<f> = (snd(t(f(a)))) ∈ formal-cube(J+i) ⊢ CompOp(universe-type(t;J+i;f(a)))
25. Z : formal-cube(J+i) ⊢ CompOp(universe-type(t;J+i;f(a)))
26. a1 : universe-type(t;I;a)((i0)(f))
27. J@0 : fset(ℕ)
28. f@0 : J,phi(J@0)
29. (universe-type(t;I;a))<f> = universe-type(t;J+i;f(a)) ∈ {formal-cube(J+i) ⊢ _}
30. (universe-type(t;I;a))<f>
= universe-type(t;J+i;f(a))
∈ {z:{formal-cube(J+i) ⊢ _}|
(z = (universe-type(t;I;a))<f> ∈ {formal-cube(J+i) ⊢ _}) ∧ (z = universe-type(t;J+i;f(a)) ∈ {formal-cube(J+i) ⊢ _})}
31. W : {z:{formal-cube(J+i) ⊢ _}|
(z = (universe-type(t;I;a))<f> ∈ {formal-cube(J+i) ⊢ _})
∧ (z = universe-type(t;J+i;f(a)) ∈ {formal-cube(J+i) ⊢ _})}
32. W(f@0((i0)(1))) = universe-type(t;I;a)(f@0((i0)(f))) ∈ Type
⊢ (a1 (i0)(1) f@0) ∈ W(f@0((i0)(1)))
Latex:
Latex:
1. X : CubicalSet\{j\}
2. t : \{X \mvdash{} \_:c\mBbbU{}\}
3. I : fset(\mBbbN{})
4. a : X(I)
5. t(a) \mmember{} A:\{formal-cube(I) \mvdash{} \_\} \mtimes{} formal-cube(I) \mvdash{} CompOp(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. A : \{formal-cube(I) \mvdash{} \_\}
22. v1 : formal-cube(I) \mvdash{} CompOp(A)
23. t(a) = <A, v1>
24. (v1)<f> = (snd(t(f(a))))
25. Z : formal-cube(J+i) \mvdash{} CompOp(universe-type(t;J+i;f(a)))
26. a1 : universe-type(t;I;a)((i0)(f))
27. J@0 : fset(\mBbbN{})
28. f@0 : J,phi(J@0)
29. (universe-type(t;I;a))<f> = universe-type(t;J+i;f(a))
30. (universe-type(t;I;a))<f> = universe-type(t;J+i;f(a))
31. W : \{z:\{formal-cube(J+i) \mvdash{} \_\}|
(z = (universe-type(t;I;a))<f>) \mwedge{} (z = universe-type(t;J+i;f(a)))\}
\mvdash{} (a1 (i0)(1) f@0) \mmember{} universe-type(t;I;a)(f@0((i0)(f)))
By
Latex:
InferEqualTypeGen
Home
Index