Step
*
1
1
2
1
2
1
2
4
1
1
1
1
1
2
2
2
1
2
10
1
2
2
3
1
1
1
1
2
1
2
1
2
1
1
1
1
1
of Lemma
lift-id-faces-wf
.....subterm..... T:t
2:n
1. I : Cname List
2. X : CubicalSet
3. A : {X ⊢ _}
4. a : {X ⊢ _:A}
5. b : {X ⊢ _:A}
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 : Cname
23. (x1 ∈ I)
24. i2 : ℕ2
25. v3 : (Id_A a b)((x1:=i2)(alpha))
26. box[j] = <x1, i2, v3> ∈ A-face(X;(Id_A a b);I;alpha)
27. x2 : Cname
28. (x2 ∈ I)
29. i3 : ℕ2
30. v5 : (Id_A a b)((x2:=i3)(alpha))
31. box[i1] = <x2, i3, v5> ∈ A-face(X;(Id_A a b);I;alpha)
32. ¬(x1 = x2 ∈ Cname)
33. (v3 (x1:=i2)(alpha) (x2:=i3)) = (v5 (x2:=i3)(alpha) (x1:=i2)) ∈ (Id_A a b)(((x2:=i3) o (x1:=i2))(alpha))
34. ∀i:ℕ2. ∀x:nameset(I). (I-path(X;A;a;b;I-[x];(x:=i)(alpha)) ⊆r (Id_A a b)((x:=i)(alpha)))
35. z : Cname
36. ¬(z ∈ I-[x1])
37. v7 : A(iota(fresh-cname(I))((x1:=i2)(alpha)))
38. name-path-endpoints(X;A;a;b;I-[x1];(x1:=i2)(alpha);fresh-cname(I);v7)
39. z = fresh-cname(I) ∈ Cname
40. <fresh-cname(I), v7> = v3 ∈ (Id_A a b)((x1:=i2)(alpha))
41. set-path-name(X;A;I-[x1];(x1:=i2)(alpha);fresh-cname(I);v3)
= <fresh-cname(I), v7>
∈ {q:I-path(X;A;a;b;I-[x1];(x1:=i2)(alpha))|
((fst(q)) = fresh-cname(I) ∈ Cname) ∧ (q = v3 ∈ (Id_A a b)((x1:=i2)(alpha)))}
42. z1 : Cname
43. ¬(z1 ∈ I-[x2])
44. v8 : A(iota(fresh-cname(I))((x2:=i3)(alpha)))
45. name-path-endpoints(X;A;a;b;I-[x2];(x2:=i3)(alpha);fresh-cname(I);v8)
46. z1 = fresh-cname(I) ∈ Cname
47. <fresh-cname(I), v8> = v5 ∈ (Id_A a b)((x2:=i3)(alpha))
48. set-path-name(X;A;I-[x2];(x2:=i3)(alpha);fresh-cname(I);v5)
= <fresh-cname(I), v8>
∈ {q:I-path(X;A;a;b;I-[x2];(x2:=i3)(alpha))|
((fst(q)) = fresh-cname(I) ∈ Cname) ∧ (q = v5 ∈ (Id_A a b)((x2:=i3)(alpha)))}
49. I-path-morph(X;A;I-[x1];I-[x1; x2];(x2:=i3);(x1:=i2)(alpha);<fresh-cname(I), v7>) = I-path-morph(X;A;I-[x2];I-[x1; x\000C2];(x1:=i2);(x2:=i3)(alpha);<fresh-cname(I), v8>) ∈ cubical-path(X;A;a;b;I-[x1; x2];((x2:=i3) o (x1:=i2))(alpha))
50. ((x2:=i3) o (x1:=i2)) ∈ name-morph(I;I-[x1; x2])
51. fresh-cname(I-[x1; x2]) = fresh-cname(I-[x1; x2]) ∈ {z:Cname| ¬(z ∈ I-[x1; x2])}
52. (v7 iota(fresh-cname(I))((x1:=i2)(alpha)) (x2:=i3)[fresh-cname(I):=fresh-cname(I-[x1; x2])])
= (v8 iota(fresh-cname(I))((x2:=i3)(alpha)) (x1:=i2)[fresh-cname(I):=fresh-cname(I-[x1; x2])])
∈ named-path(X;A;a;b;I-[x1; x2];((x2:=i3) o (x1:=i2))(alpha);fresh-cname(I-[x1; x2]))
53. (v7 iota'(I)((x1:=i2)(alpha)) (x2:=i3)[fresh-cname(I):=fresh-cname(I-[x1; x2])])
= (v8 iota'(I)((x2:=i3)(alpha)) (x1:=i2)[fresh-cname(I):=fresh-cname(I-[x1; x2])])
∈ A(iota'(I-[x1; x2])(((x2:=i3) o (x1:=i2))(alpha)))
54. ((x2:=i3) o (x1:=i2)) ∈ name-morph(I+;I+-[x1; x2])
55. I+-[x1; x2] = [fresh-cname(I) / I-[x1; x2]] ∈ (Cname List)
56. [fresh-cname(I) / I-[x1]] = I+-[x1] ∈ (Cname List)
57. iota(fresh-cname(I))((x1:=i2)(alpha)) = (x1:=i2)(iota'(I)(alpha)) ∈ X([fresh-cname(I) / I-[x1]])
58. [fresh-cname(I) / I-[x2]] = I+-[x2] ∈ (Cname List)
59. iota(fresh-cname(I))((x2:=i3)(alpha)) = (x2:=i3)(iota'(I)(alpha)) ∈ X([fresh-cname(I) / I-[x2]])
60. ((v7 (x1:=i2)(iota'(I)(alpha)) (x2:=i3)) (x2:=i3)((x1:=i2)(iota'(I)(alpha))) rename-one-name(fresh-cname(I);...))
= (v7 (x1:=i2)(iota'(I)(alpha)) ((x2:=i3) o rename-one-name(fresh-cname(I);fresh-cname(I-[x1; x2]))))
∈ A(((x2:=i3) o rename-one-name(fresh-cname(I);fresh-cname(I-[x1; x2])))((x1:=i2)(iota'(I)(alpha))))
61. v : Cname
62. ¬(v ∈ I)
63. fresh-cname(I) = v ∈ {x:Cname| ¬(x ∈ I)}
64. v9 : Cname
65. ¬(v9 ∈ I-[x1; x2])
66. fresh-cname(I-[x1; x2]) = v9 ∈ {x:Cname| ¬(x ∈ I-[x1; x2])}
67. [v / I-[x2]] = [v / I]-[x2] ∈ (Cname List)
68. [v / I-[x1; x2]] = [v / I-[x2]]-[x1] ∈ (Cname List)
69. iota(v) ∈ name-morph(I;[v / I])
70. (x2:=i3) ∈ name-morph([v / I];[v / I-[x2]])
71. (x1:=i2) ∈ name-morph([v / I-[x2]];[v / I-[x1; x2]])
72. rename-one-name(v;v9) ∈ name-morph([v / I-[x1; x2]];[v9 / I-[x1; x2]])
73. rename-one-name(v;v9)(((x2:=i3) o (x1:=i2))(iota(v)(alpha)))
= ((iota(v) o ((x2:=i3) o (x1:=i2))) o rename-one-name(v;v9))(alpha)
∈ X([v9 / I-[x1; x2]])
74. (x2:=i3)[v:=v9](iota(v)((x1:=i2)(alpha))) = (((x1:=i2) o iota(v)) o (x2:=i3)[v:=v9])(alpha) ∈ X([v9 / I-[x1; x2]])
⊢ ((x2:=i3) o (x1:=i2)) = ((x1:=i2) o (x2:=i3)) ∈ name-morph([v / I];[v / I-[x1; x2]])
BY
{ TACTIC:(InstLemma `face-maps-commute` [⌜[v / I]⌝;⌜x2⌝;⌜i3⌝;⌜x1⌝;⌜i2⌝]⋅ THENA Auto) }
1
1. I : Cname List
2. X : CubicalSet
3. A : {X ⊢ _}
4. a : {X ⊢ _:A}
5. b : {X ⊢ _:A}
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 : Cname
23. (x1 ∈ I)
24. i2 : ℕ2
25. v3 : (Id_A a b)((x1:=i2)(alpha))
26. box[j] = <x1, i2, v3> ∈ A-face(X;(Id_A a b);I;alpha)
27. x2 : Cname
28. (x2 ∈ I)
29. i3 : ℕ2
30. v5 : (Id_A a b)((x2:=i3)(alpha))
31. box[i1] = <x2, i3, v5> ∈ A-face(X;(Id_A a b);I;alpha)
32. ¬(x1 = x2 ∈ Cname)
33. (v3 (x1:=i2)(alpha) (x2:=i3)) = (v5 (x2:=i3)(alpha) (x1:=i2)) ∈ (Id_A a b)(((x2:=i3) o (x1:=i2))(alpha))
34. ∀i:ℕ2. ∀x:nameset(I). (I-path(X;A;a;b;I-[x];(x:=i)(alpha)) ⊆r (Id_A a b)((x:=i)(alpha)))
35. z : Cname
36. ¬(z ∈ I-[x1])
37. v7 : A(iota(fresh-cname(I))((x1:=i2)(alpha)))
38. name-path-endpoints(X;A;a;b;I-[x1];(x1:=i2)(alpha);fresh-cname(I);v7)
39. z = fresh-cname(I) ∈ Cname
40. <fresh-cname(I), v7> = v3 ∈ (Id_A a b)((x1:=i2)(alpha))
41. set-path-name(X;A;I-[x1];(x1:=i2)(alpha);fresh-cname(I);v3)
= <fresh-cname(I), v7>
∈ {q:I-path(X;A;a;b;I-[x1];(x1:=i2)(alpha))|
((fst(q)) = fresh-cname(I) ∈ Cname) ∧ (q = v3 ∈ (Id_A a b)((x1:=i2)(alpha)))}
42. z1 : Cname
43. ¬(z1 ∈ I-[x2])
44. v8 : A(iota(fresh-cname(I))((x2:=i3)(alpha)))
45. name-path-endpoints(X;A;a;b;I-[x2];(x2:=i3)(alpha);fresh-cname(I);v8)
46. z1 = fresh-cname(I) ∈ Cname
47. <fresh-cname(I), v8> = v5 ∈ (Id_A a b)((x2:=i3)(alpha))
48. set-path-name(X;A;I-[x2];(x2:=i3)(alpha);fresh-cname(I);v5)
= <fresh-cname(I), v8>
∈ {q:I-path(X;A;a;b;I-[x2];(x2:=i3)(alpha))|
((fst(q)) = fresh-cname(I) ∈ Cname) ∧ (q = v5 ∈ (Id_A a b)((x2:=i3)(alpha)))}
49. I-path-morph(X;A;I-[x1];I-[x1; x2];(x2:=i3);(x1:=i2)(alpha);<fresh-cname(I), v7>) = I-path-morph(X;A;I-[x2];I-[x1; x\000C2];(x1:=i2);(x2:=i3)(alpha);<fresh-cname(I), v8>) ∈ cubical-path(X;A;a;b;I-[x1; x2];((x2:=i3) o (x1:=i2))(alpha))
50. ((x2:=i3) o (x1:=i2)) ∈ name-morph(I;I-[x1; x2])
51. fresh-cname(I-[x1; x2]) = fresh-cname(I-[x1; x2]) ∈ {z:Cname| ¬(z ∈ I-[x1; x2])}
52. (v7 iota(fresh-cname(I))((x1:=i2)(alpha)) (x2:=i3)[fresh-cname(I):=fresh-cname(I-[x1; x2])])
= (v8 iota(fresh-cname(I))((x2:=i3)(alpha)) (x1:=i2)[fresh-cname(I):=fresh-cname(I-[x1; x2])])
∈ named-path(X;A;a;b;I-[x1; x2];((x2:=i3) o (x1:=i2))(alpha);fresh-cname(I-[x1; x2]))
53. (v7 iota'(I)((x1:=i2)(alpha)) (x2:=i3)[fresh-cname(I):=fresh-cname(I-[x1; x2])])
= (v8 iota'(I)((x2:=i3)(alpha)) (x1:=i2)[fresh-cname(I):=fresh-cname(I-[x1; x2])])
∈ A(iota'(I-[x1; x2])(((x2:=i3) o (x1:=i2))(alpha)))
54. ((x2:=i3) o (x1:=i2)) ∈ name-morph(I+;I+-[x1; x2])
55. I+-[x1; x2] = [fresh-cname(I) / I-[x1; x2]] ∈ (Cname List)
56. [fresh-cname(I) / I-[x1]] = I+-[x1] ∈ (Cname List)
57. iota(fresh-cname(I))((x1:=i2)(alpha)) = (x1:=i2)(iota'(I)(alpha)) ∈ X([fresh-cname(I) / I-[x1]])
58. [fresh-cname(I) / I-[x2]] = I+-[x2] ∈ (Cname List)
59. iota(fresh-cname(I))((x2:=i3)(alpha)) = (x2:=i3)(iota'(I)(alpha)) ∈ X([fresh-cname(I) / I-[x2]])
60. ((v7 (x1:=i2)(iota'(I)(alpha)) (x2:=i3)) (x2:=i3)((x1:=i2)(iota'(I)(alpha))) rename-one-name(fresh-cname(I);...))
= (v7 (x1:=i2)(iota'(I)(alpha)) ((x2:=i3) o rename-one-name(fresh-cname(I);fresh-cname(I-[x1; x2]))))
∈ A(((x2:=i3) o rename-one-name(fresh-cname(I);fresh-cname(I-[x1; x2])))((x1:=i2)(iota'(I)(alpha))))
61. v : Cname
62. ¬(v ∈ I)
63. fresh-cname(I) = v ∈ {x:Cname| ¬(x ∈ I)}
64. v9 : Cname
65. ¬(v9 ∈ I-[x1; x2])
66. fresh-cname(I-[x1; x2]) = v9 ∈ {x:Cname| ¬(x ∈ I-[x1; x2])}
67. [v / I-[x2]] = [v / I]-[x2] ∈ (Cname List)
68. [v / I-[x1; x2]] = [v / I-[x2]]-[x1] ∈ (Cname List)
69. iota(v) ∈ name-morph(I;[v / I])
70. (x2:=i3) ∈ name-morph([v / I];[v / I-[x2]])
71. (x1:=i2) ∈ name-morph([v / I-[x2]];[v / I-[x1; x2]])
72. rename-one-name(v;v9) ∈ name-morph([v / I-[x1; x2]];[v9 / I-[x1; x2]])
73. rename-one-name(v;v9)(((x2:=i3) o (x1:=i2))(iota(v)(alpha)))
= ((iota(v) o ((x2:=i3) o (x1:=i2))) o rename-one-name(v;v9))(alpha)
∈ X([v9 / I-[x1; x2]])
74. (x2:=i3)[v:=v9](iota(v)((x1:=i2)(alpha))) = (((x1:=i2) o iota(v)) o (x2:=i3)[v:=v9])(alpha) ∈ X([v9 / I-[x1; x2]])
75. ((x2:=i3) o (x1:=i2)) = ((x1:=i2) o (x2:=i3)) ∈ name-morph([v / I];[v / I]-[x2; x1])
⊢ ((x2:=i3) o (x1:=i2)) = ((x1:=i2) o (x2:=i3)) ∈ name-morph([v / I];[v / I-[x1; x2]])
Latex:
Latex:
.....subterm..... T:t
2:n
1. I : Cname List
2. X : CubicalSet
3. A : \{X \mvdash{} \_\}
4. a : \{X \mvdash{} \_:A\}
5. b : \{X \mvdash{} \_:A\}
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 : Cname
23. (x1 \mmember{} I)
24. i2 : \mBbbN{}2
25. v3 : (Id\_A a b)((x1:=i2)(alpha))
26. box[j] = <x1, i2, v3>
27. x2 : Cname
28. (x2 \mmember{} I)
29. i3 : \mBbbN{}2
30. v5 : (Id\_A a b)((x2:=i3)(alpha))
31. box[i1] = <x2, i3, v5>
32. \mneg{}(x1 = x2)
33. (v3 (x1:=i2)(alpha) (x2:=i3)) = (v5 (x2:=i3)(alpha) (x1:=i2))
34. \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)))
35. z : Cname
36. \mneg{}(z \mmember{} I-[x1])
37. v7 : A(iota(fresh-cname(I))((x1:=i2)(alpha)))
38. name-path-endpoints(X;A;a;b;I-[x1];(x1:=i2)(alpha);fresh-cname(I);v7)
39. z = fresh-cname(I)
40. <fresh-cname(I), v7> = v3
41. set-path-name(X;A;I-[x1];(x1:=i2)(alpha);fresh-cname(I);v3) = <fresh-cname(I), v7>
42. z1 : Cname
43. \mneg{}(z1 \mmember{} I-[x2])
44. v8 : A(iota(fresh-cname(I))((x2:=i3)(alpha)))
45. name-path-endpoints(X;A;a;b;I-[x2];(x2:=i3)(alpha);fresh-cname(I);v8)
46. z1 = fresh-cname(I)
47. <fresh-cname(I), v8> = v5
48. set-path-name(X;A;I-[x2];(x2:=i3)(alpha);fresh-cname(I);v5) = <fresh-cname(I), v8>
49. I-path-morph(X;A;I-[x1];I-[x1; x2];(x2:=i3);(x1:=i2)(alpha);<fresh-cname(I), v7>)
= I-path-morph(X;A;I-[x2];I-[x1; x2];(x1:=i2);(x2:=i3)(alpha);<fresh-cname(I), v8>)
50. ((x2:=i3) o (x1:=i2)) \mmember{} name-morph(I;I-[x1; x2])
51. fresh-cname(I-[x1; x2]) = fresh-cname(I-[x1; x2])
52. (v7 iota(fresh-cname(I))((x1:=i2)(alpha)) (x2:=i3)[fresh-cname(I):=fresh-cname(I-[x1; x2])])
= (v8 iota(fresh-cname(I))((x2:=i3)(alpha)) (x1:=i2)[fresh-cname(I):=fresh-cname(I-[x1; x2])])
53. (v7 iota'(I)((x1:=i2)(alpha)) (x2:=i3)[fresh-cname(I):=fresh-cname(I-[x1; x2])])
= (v8 iota'(I)((x2:=i3)(alpha)) (x1:=i2)[fresh-cname(I):=fresh-cname(I-[x1; x2])])
54. ((x2:=i3) o (x1:=i2)) \mmember{} name-morph(I+;I+-[x1; x2])
55. I+-[x1; x2] = [fresh-cname(I) / I-[x1; x2]]
56. [fresh-cname(I) / I-[x1]] = I+-[x1]
57. iota(fresh-cname(I))((x1:=i2)(alpha)) = (x1:=i2)(iota'(I)(alpha))
58. [fresh-cname(I) / I-[x2]] = I+-[x2]
59. iota(fresh-cname(I))((x2:=i3)(alpha)) = (x2:=i3)(iota'(I)(alpha))
60. ((v7 (x1:=i2)(iota'(I)(alpha)) (x2:=i3)) (x2:=i3)((x1:=i2)(iota'(I)(alpha))) ...)
= (v7 (x1:=i2)(iota'(I)(alpha)) ((x2:=i3) o rename-one-name(fresh-cname(I);fresh-cname(I-[x1;
x2]))))
61. v : Cname
62. \mneg{}(v \mmember{} I)
63. fresh-cname(I) = v
64. v9 : Cname
65. \mneg{}(v9 \mmember{} I-[x1; x2])
66. fresh-cname(I-[x1; x2]) = v9
67. [v / I-[x2]] = [v / I]-[x2]
68. [v / I-[x1; x2]] = [v / I-[x2]]-[x1]
69. iota(v) \mmember{} name-morph(I;[v / I])
70. (x2:=i3) \mmember{} name-morph([v / I];[v / I-[x2]])
71. (x1:=i2) \mmember{} name-morph([v / I-[x2]];[v / I-[x1; x2]])
72. rename-one-name(v;v9) \mmember{} name-morph([v / I-[x1; x2]];[v9 / I-[x1; x2]])
73. rename-one-name(v;v9)(((x2:=i3) o (x1:=i2))(iota(v)(alpha)))
= ((iota(v) o ((x2:=i3) o (x1:=i2))) o rename-one-name(v;v9))(alpha)
74. (x2:=i3)[v:=v9](iota(v)((x1:=i2)(alpha))) = (((x1:=i2) o iota(v)) o (x2:=i3)[v:=v9])(alpha)
\mvdash{} ((x2:=i3) o (x1:=i2)) = ((x1:=i2) o (x2:=i3))
By
Latex:
TACTIC:(InstLemma `face-maps-commute` [\mkleeneopen{}[v / I]\mkleeneclose{};\mkleeneopen{}x2\mkleeneclose{};\mkleeneopen{}i3\mkleeneclose{};\mkleeneopen{}x1\mkleeneclose{};\mkleeneopen{}i2\mkleeneclose{}]\mcdot{} THENA Auto)
Home
Index