Step
*
1
1
of Lemma
lift-id-faces-wf
1. X : CubicalSet
2. A : {X ⊢ _}
3. a : {X ⊢ _:A}
4. b : {X ⊢ _:A}
5. I : Cname List
6. J : nameset(I) List
7. x : nameset(I)
8. i : ℕ2
9. alpha : X(I)
10. box : A-face(X;(Id_A a b);I;alpha) List
11. ∀i:ℕ||box||. ∀j:ℕi. A-face-compatible(X;(Id_A a b);I;alpha;box[j];box[i])
12. ¬(x ∈ J)
13. l_subset(Cname;J;I)
14. ∀y:nameset(J). ∀c:ℕ2. (∃f∈box. A-face-name(f) = <y, c> ∈ (nameset(I) × ℕ2))
15. (∃f∈box. A-face-name(f) = <x, i> ∈ (nameset(I) × ℕ2))
16. (∀f∈box.¬(A-face-name(f) = <x, 1 - i> ∈ (nameset(I) × ℕ2)))
17. (∀f∈box.(fst(f) ∈ [x / J]))
18. (∀f1,f2∈box. ¬(A-face-name(f1) = A-face-name(f2) ∈ (nameset(I) × ℕ2)))
19. i1 : ℕ||box||
20. ∀j:ℕi1. A-face-compatible(X;(Id_A a b);I;alpha;box[j];box[i1])
21. j : ℕi1
22. x1 : nameset(I)
23. i2 : ℕ2
24. v3 : (Id_A a b)((x1:=i2)(alpha))
25. box[j] = <x1, i2, v3> ∈ A-face(X;(Id_A a b);I;alpha)
26. x2 : nameset(I)
27. i3 : ℕ2
28. v5 : (Id_A a b)((x2:=i3)(alpha))
29. box[i1] = <x2, i3, v5> ∈ A-face(X;(Id_A a b);I;alpha)
30. ¬(x1 = x2 ∈ Cname)
31. (v3 (x1:=i2)(alpha) (x2:=i3)) = (v5 (x2:=i3)(alpha) (x1:=i2)) ∈ (Id_A a b)(((x2:=i3) o (x1:=i2))(alpha))
⊢ (snd(set-path-name(X;A;I-[x1];(x1:=i2)(alpha);fresh-cname(I);v3)) (x1:=i2)(iota'(I)(alpha)) (x2:=i3))
= (snd(set-path-name(X;A;I-[x2];(x2:=i3)(alpha);fresh-cname(I);v5)) (x2:=i3)(iota'(I)(alpha)) (x1:=i2))
∈ A(((x2:=i3) o (x1:=i2))(iota'(I)(alpha)))
BY
{ Assert ⌜∀i:ℕ2. ∀x:nameset(I). (I-path(X;A;a;b;I-[x];(x:=i)(alpha)) ⊆r (Id_A a b)((x:=i)(alpha)))⌝⋅ }
1
.....assertion.....
1. X : CubicalSet
2. A : {X ⊢ _}
3. a : {X ⊢ _:A}
4. b : {X ⊢ _:A}
5. I : Cname List
6. J : nameset(I) List
7. x : nameset(I)
8. i : ℕ2
9. alpha : X(I)
10. box : A-face(X;(Id_A a b);I;alpha) List
11. ∀i:ℕ||box||. ∀j:ℕi. A-face-compatible(X;(Id_A a b);I;alpha;box[j];box[i])
12. ¬(x ∈ J)
13. l_subset(Cname;J;I)
14. ∀y:nameset(J). ∀c:ℕ2. (∃f∈box. A-face-name(f) = <y, c> ∈ (nameset(I) × ℕ2))
15. (∃f∈box. A-face-name(f) = <x, i> ∈ (nameset(I) × ℕ2))
16. (∀f∈box.¬(A-face-name(f) = <x, 1 - i> ∈ (nameset(I) × ℕ2)))
17. (∀f∈box.(fst(f) ∈ [x / J]))
18. (∀f1,f2∈box. ¬(A-face-name(f1) = A-face-name(f2) ∈ (nameset(I) × ℕ2)))
19. i1 : ℕ||box||
20. ∀j:ℕi1. A-face-compatible(X;(Id_A a b);I;alpha;box[j];box[i1])
21. j : ℕi1
22. x1 : nameset(I)
23. i2 : ℕ2
24. v3 : (Id_A a b)((x1:=i2)(alpha))
25. box[j] = <x1, i2, v3> ∈ A-face(X;(Id_A a b);I;alpha)
26. x2 : nameset(I)
27. i3 : ℕ2
28. v5 : (Id_A a b)((x2:=i3)(alpha))
29. box[i1] = <x2, i3, v5> ∈ A-face(X;(Id_A a b);I;alpha)
30. ¬(x1 = x2 ∈ Cname)
31. (v3 (x1:=i2)(alpha) (x2:=i3)) = (v5 (x2:=i3)(alpha) (x1:=i2)) ∈ (Id_A a b)(((x2:=i3) o (x1:=i2))(alpha))
⊢ ∀i:ℕ2. ∀x:nameset(I). (I-path(X;A;a;b;I-[x];(x:=i)(alpha)) ⊆r (Id_A a b)((x:=i)(alpha)))
2
1. X : CubicalSet
2. A : {X ⊢ _}
3. a : {X ⊢ _:A}
4. b : {X ⊢ _:A}
5. I : Cname List
6. J : nameset(I) List
7. x : nameset(I)
8. i : ℕ2
9. alpha : X(I)
10. box : A-face(X;(Id_A a b);I;alpha) List
11. ∀i:ℕ||box||. ∀j:ℕi. A-face-compatible(X;(Id_A a b);I;alpha;box[j];box[i])
12. ¬(x ∈ J)
13. l_subset(Cname;J;I)
14. ∀y:nameset(J). ∀c:ℕ2. (∃f∈box. A-face-name(f) = <y, c> ∈ (nameset(I) × ℕ2))
15. (∃f∈box. A-face-name(f) = <x, i> ∈ (nameset(I) × ℕ2))
16. (∀f∈box.¬(A-face-name(f) = <x, 1 - i> ∈ (nameset(I) × ℕ2)))
17. (∀f∈box.(fst(f) ∈ [x / J]))
18. (∀f1,f2∈box. ¬(A-face-name(f1) = A-face-name(f2) ∈ (nameset(I) × ℕ2)))
19. i1 : ℕ||box||
20. ∀j:ℕi1. A-face-compatible(X;(Id_A a b);I;alpha;box[j];box[i1])
21. j : ℕi1
22. x1 : nameset(I)
23. i2 : ℕ2
24. v3 : (Id_A a b)((x1:=i2)(alpha))
25. box[j] = <x1, i2, v3> ∈ A-face(X;(Id_A a b);I;alpha)
26. x2 : nameset(I)
27. i3 : ℕ2
28. v5 : (Id_A a b)((x2:=i3)(alpha))
29. box[i1] = <x2, i3, v5> ∈ A-face(X;(Id_A a b);I;alpha)
30. ¬(x1 = x2 ∈ Cname)
31. (v3 (x1:=i2)(alpha) (x2:=i3)) = (v5 (x2:=i3)(alpha) (x1:=i2)) ∈ (Id_A a b)(((x2:=i3) o (x1:=i2))(alpha))
32. ∀i:ℕ2. ∀x:nameset(I). (I-path(X;A;a;b;I-[x];(x:=i)(alpha)) ⊆r (Id_A a b)((x:=i)(alpha)))
⊢ (snd(set-path-name(X;A;I-[x1];(x1:=i2)(alpha);fresh-cname(I);v3)) (x1:=i2)(iota'(I)(alpha)) (x2:=i3))
= (snd(set-path-name(X;A;I-[x2];(x2:=i3)(alpha);fresh-cname(I);v5)) (x2:=i3)(iota'(I)(alpha)) (x1:=i2))
∈ A(((x2:=i3) o (x1:=i2))(iota'(I)(alpha)))
Latex:
Latex:
1. X : CubicalSet
2. A : \{X \mvdash{} \_\}
3. a : \{X \mvdash{} \_:A\}
4. b : \{X \mvdash{} \_:A\}
5. I : Cname List
6. J : nameset(I) List
7. x : nameset(I)
8. i : \mBbbN{}2
9. alpha : X(I)
10. box : A-face(X;(Id\_A a b);I;alpha) List
11. \mforall{}i:\mBbbN{}||box||. \mforall{}j:\mBbbN{}i. A-face-compatible(X;(Id\_A a b);I;alpha;box[j];box[i])
12. \mneg{}(x \mmember{} J)
13. l\_subset(Cname;J;I)
14. \mforall{}y:nameset(J). \mforall{}c:\mBbbN{}2. (\mexists{}f\mmember{}box. A-face-name(f) = <y, c>)
15. (\mexists{}f\mmember{}box. A-face-name(f) = <x, i>)
16. (\mforall{}f\mmember{}box.\mneg{}(A-face-name(f) = <x, 1 - i>))
17. (\mforall{}f\mmember{}box.(fst(f) \mmember{} [x / J]))
18. (\mforall{}f1,f2\mmember{}box. \mneg{}(A-face-name(f1) = A-face-name(f2)))
19. i1 : \mBbbN{}||box||
20. \mforall{}j:\mBbbN{}i1. A-face-compatible(X;(Id\_A a b);I;alpha;box[j];box[i1])
21. j : \mBbbN{}i1
22. x1 : nameset(I)
23. i2 : \mBbbN{}2
24. v3 : (Id\_A a b)((x1:=i2)(alpha))
25. box[j] = <x1, i2, v3>
26. x2 : nameset(I)
27. i3 : \mBbbN{}2
28. v5 : (Id\_A a b)((x2:=i3)(alpha))
29. box[i1] = <x2, i3, v5>
30. \mneg{}(x1 = x2)
31. (v3 (x1:=i2)(alpha) (x2:=i3)) = (v5 (x2:=i3)(alpha) (x1:=i2))
\mvdash{} (snd(set-path-name(X;A;I-[x1];(x1:=i2)(alpha);fresh-cname(I);v3)) (x1:=i2)(iota'(I)(alpha)) ...)
= (snd(set-path-name(X;A;I-[x2];(x2:=i3)(alpha);fresh-cname(I);v5)) (x2:=i3)(iota'(I)(alpha)) ...)
By
Latex:
Assert \mkleeneopen{}\mforall{}i:\mBbbN{}2. \mforall{}x:nameset(I). (I-path(X;A;a;b;I-[x];(x:=i)(alpha)) \msubseteq{}r (Id\_A a b)((x:=i)(alpha)))\mkleeneclose{}\mcdot{}
Home
Index