Step
*
1
1
1
of Lemma
sigma-box-fst_wf
1. X : CubicalSet
2. A : {X ⊢ _(Kan)}
3. B : {X.Kan-type(A) ⊢ _(Kan)}
4. I : Cname List
5. alpha : X(I)
6. J : nameset(I) List
7. x : nameset(I)
8. i : ℕ2
9. bx : A-face(X;Σ Kan-type(A) Kan-type(B);I;alpha) List
10. ∀i:ℕ||bx||. ∀j:ℕi. A-face-compatible(X;Σ Kan-type(A) Kan-type(B);I;alpha;bx[j];bx[i])
11. ¬(x ∈ J)
12. l_subset(Cname;J;I)
13. ∀y:nameset(J). ∀c:ℕ2. (∃f∈bx. A-face-name(f) = <y, c> ∈ (nameset(I) × ℕ2))
14. (∃f∈bx. A-face-name(f) = <x, i> ∈ (nameset(I) × ℕ2))
15. (∀f∈bx.¬(A-face-name(f) = <x, 1 - i> ∈ (nameset(I) × ℕ2)))
16. (∀f∈bx.(fst(f) ∈ [x / J]))
17. (∀f1,f2∈bx. ¬(A-face-name(f1) = A-face-name(f2) ∈ (nameset(I) × ℕ2)))
18. i1 : ℕ||bx||
19. ∀j:ℕi1. A-face-compatible(X;Σ Kan-type(A) Kan-type(B);I;alpha;bx[j];bx[i1])
20. j : ℕi1
21. x2 : nameset(I)
22. i3 : ℕ2
23. u1 : Kan-type(A)((x2:=i3)(alpha))
24. v7 : Kan-type(B)(((x2:=i3)(alpha);u1))
25. x1 : nameset(I)
26. i2 : ℕ2
27. u : Kan-type(A)((x1:=i2)(alpha))
28. v4 : Kan-type(B)(((x1:=i2)(alpha);u))
29. ¬(x2 = x1 ∈ Cname)
30. (<u1, v7> (x2:=i3)(alpha) (x1:=i2))
= (<u, v4> (x1:=i2)(alpha) (x2:=i3))
∈ Σ Kan-type(A) Kan-type(B)(((x1:=i2) o (x2:=i3))(alpha))
⊢ (u1 (x2:=i3)(alpha) (x1:=i2)) = (u (x1:=i2)(alpha) (x2:=i3)) ∈ Kan-type(A)(((x1:=i2) o (x2:=i3))(alpha))
BY
{ (RWO "cubical-sigma-at" (-1) THENA Auto) }
1
1. X : CubicalSet
2. A : {X ⊢ _(Kan)}
3. B : {X.Kan-type(A) ⊢ _(Kan)}
4. I : Cname List
5. alpha : X(I)
6. J : nameset(I) List
7. x : nameset(I)
8. i : ℕ2
9. bx : A-face(X;Σ Kan-type(A) Kan-type(B);I;alpha) List
10. ∀i:ℕ||bx||. ∀j:ℕi. A-face-compatible(X;Σ Kan-type(A) Kan-type(B);I;alpha;bx[j];bx[i])
11. ¬(x ∈ J)
12. l_subset(Cname;J;I)
13. ∀y:nameset(J). ∀c:ℕ2. (∃f∈bx. A-face-name(f) = <y, c> ∈ (nameset(I) × ℕ2))
14. (∃f∈bx. A-face-name(f) = <x, i> ∈ (nameset(I) × ℕ2))
15. (∀f∈bx.¬(A-face-name(f) = <x, 1 - i> ∈ (nameset(I) × ℕ2)))
16. (∀f∈bx.(fst(f) ∈ [x / J]))
17. (∀f1,f2∈bx. ¬(A-face-name(f1) = A-face-name(f2) ∈ (nameset(I) × ℕ2)))
18. i1 : ℕ||bx||
19. ∀j:ℕi1. A-face-compatible(X;Σ Kan-type(A) Kan-type(B);I;alpha;bx[j];bx[i1])
20. j : ℕi1
21. x2 : nameset(I)
22. i3 : ℕ2
23. u1 : Kan-type(A)((x2:=i3)(alpha))
24. v7 : Kan-type(B)(((x2:=i3)(alpha);u1))
25. x1 : nameset(I)
26. i2 : ℕ2
27. u : Kan-type(A)((x1:=i2)(alpha))
28. v4 : Kan-type(B)(((x1:=i2)(alpha);u))
29. ¬(x2 = x1 ∈ Cname)
30. (<u1, v7> (x2:=i3)(alpha) (x1:=i2))
= (<u, v4> (x1:=i2)(alpha) (x2:=i3))
∈ (u:Kan-type(A)(((x1:=i2) o (x2:=i3))(alpha)) × Kan-type(B)((((x1:=i2) o (x2:=i3))(alpha);u)))
⊢ (u1 (x2:=i3)(alpha) (x1:=i2)) = (u (x1:=i2)(alpha) (x2:=i3)) ∈ Kan-type(A)(((x1:=i2) o (x2:=i3))(alpha))
Latex:
Latex:
1. X : CubicalSet
2. A : \{X \mvdash{} \_(Kan)\}
3. B : \{X.Kan-type(A) \mvdash{} \_(Kan)\}
4. I : Cname List
5. alpha : X(I)
6. J : nameset(I) List
7. x : nameset(I)
8. i : \mBbbN{}2
9. bx : A-face(X;\mSigma{} Kan-type(A) Kan-type(B);I;alpha) List
10. \mforall{}i:\mBbbN{}||bx||. \mforall{}j:\mBbbN{}i. A-face-compatible(X;\mSigma{} Kan-type(A) Kan-type(B);I;alpha;bx[j];bx[i])
11. \mneg{}(x \mmember{} J)
12. l\_subset(Cname;J;I)
13. \mforall{}y:nameset(J). \mforall{}c:\mBbbN{}2. (\mexists{}f\mmember{}bx. A-face-name(f) = <y, c>)
14. (\mexists{}f\mmember{}bx. A-face-name(f) = <x, i>)
15. (\mforall{}f\mmember{}bx.\mneg{}(A-face-name(f) = <x, 1 - i>))
16. (\mforall{}f\mmember{}bx.(fst(f) \mmember{} [x / J]))
17. (\mforall{}f1,f2\mmember{}bx. \mneg{}(A-face-name(f1) = A-face-name(f2)))
18. i1 : \mBbbN{}||bx||
19. \mforall{}j:\mBbbN{}i1. A-face-compatible(X;\mSigma{} Kan-type(A) Kan-type(B);I;alpha;bx[j];bx[i1])
20. j : \mBbbN{}i1
21. x2 : nameset(I)
22. i3 : \mBbbN{}2
23. u1 : Kan-type(A)((x2:=i3)(alpha))
24. v7 : Kan-type(B)(((x2:=i3)(alpha);u1))
25. x1 : nameset(I)
26. i2 : \mBbbN{}2
27. u : Kan-type(A)((x1:=i2)(alpha))
28. v4 : Kan-type(B)(((x1:=i2)(alpha);u))
29. \mneg{}(x2 = x1)
30. (<u1, v7> (x2:=i3)(alpha) (x1:=i2)) = (<u, v4> (x1:=i2)(alpha) (x2:=i3))
\mvdash{} (u1 (x2:=i3)(alpha) (x1:=i2)) = (u (x1:=i2)(alpha) (x2:=i3))
By
Latex:
(RWO "cubical-sigma-at" (-1) THENA Auto)
Home
Index