Step
*
1
1
2
1
2
1
2
4
1
1
1
1
1
2
2
2
1
2
10
1
of Lemma
lift-id-faces-wf
.....antecedent.....
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 : 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)))
33. z : {z:Cname| ¬(z ∈ I-[x1])}
34. v7 : A(iota(fresh-cname(I))((x1:=i2)(alpha)))
35. name-path-endpoints(X;A;a;b;I-[x1];(x1:=i2)(alpha);fresh-cname(I);v7)
36. z = fresh-cname(I) ∈ Cname
37. <fresh-cname(I), v7> = v3 ∈ (Id_A a b)((x1:=i2)(alpha))
38. 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)))}
39. z1 : {z:Cname| ¬(z ∈ I-[x2])}
40. v8 : A(iota(fresh-cname(I))((x2:=i3)(alpha)))
41. name-path-endpoints(X;A;a;b;I-[x2];(x2:=i3)(alpha);fresh-cname(I);v8)
42. z1 = fresh-cname(I) ∈ Cname
43. <fresh-cname(I), v8> = v5 ∈ (Id_A a b)((x2:=i3)(alpha))
44. 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)))}
45. 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))
46. ((x2:=i3) o (x1:=i2)) ∈ name-morph(I;I-[x1; x2])
47. fresh-cname(I-[x1; x2]) = fresh-cname(I-[x1; x2]) ∈ {z:Cname| ¬(z ∈ I-[x1; x2])}
48. (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]))
49. (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)))
50. ((x2:=i3) o (x1:=i2)) ∈ name-morph(I+;I+-[x1; x2])
51. I+-[x1; x2] = [fresh-cname(I) / I-[x1; x2]] ∈ (Cname List)
52. ([fresh-cname(I) / I-[x1]] = I+-[x1] ∈ (Cname List))
∧ (iota(fresh-cname(I))((x1:=i2)(alpha)) = (x1:=i2)(iota'(I)(alpha)) ∈ X([fresh-cname(I) / I-[x1]]))
53. ([fresh-cname(I) / I-[x2]] = I+-[x2] ∈ (Cname List))
∧ (iota(fresh-cname(I))((x2:=i3)(alpha)) = (x2:=i3)(iota'(I)(alpha)) ∈ X([fresh-cname(I) / I-[x2]]))
⊢ ((v7 (x1:=i2)(iota'(I)(alpha)) (x2:=i3)) ((x2:=i3) o (x1:=i2))(iota'(I)(alpha)) rename-one-name(fresh-cname(I);...))
= ((v8 (x2:=i3)(iota'(I)(alpha)) (x1:=i2)) ((x2:=i3) o (x1:=i2))(iota'(I)(alpha)) rename-one-name(fresh-cname(I);...))
∈ A(rename-one-name(fresh-cname(I);fresh-cname(I-[x1; x2]))(((x2:=i3) o (x1:=i2))(iota'(I)(alpha))))
BY
{ (NthHypEq (-5) THEN EqCD) }
1
.....subterm..... T:t
1: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 : 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)))
33. z : {z:Cname| ¬(z ∈ I-[x1])}
34. v7 : A(iota(fresh-cname(I))((x1:=i2)(alpha)))
35. name-path-endpoints(X;A;a;b;I-[x1];(x1:=i2)(alpha);fresh-cname(I);v7)
36. z = fresh-cname(I) ∈ Cname
37. <fresh-cname(I), v7> = v3 ∈ (Id_A a b)((x1:=i2)(alpha))
38. 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)))}
39. z1 : {z:Cname| ¬(z ∈ I-[x2])}
40. v8 : A(iota(fresh-cname(I))((x2:=i3)(alpha)))
41. name-path-endpoints(X;A;a;b;I-[x2];(x2:=i3)(alpha);fresh-cname(I);v8)
42. z1 = fresh-cname(I) ∈ Cname
43. <fresh-cname(I), v8> = v5 ∈ (Id_A a b)((x2:=i3)(alpha))
44. 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)))}
45. 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))
46. ((x2:=i3) o (x1:=i2)) ∈ name-morph(I;I-[x1; x2])
47. fresh-cname(I-[x1; x2]) = fresh-cname(I-[x1; x2]) ∈ {z:Cname| ¬(z ∈ I-[x1; x2])}
48. (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]))
49. (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)))
50. ((x2:=i3) o (x1:=i2)) ∈ name-morph(I+;I+-[x1; x2])
51. I+-[x1; x2] = [fresh-cname(I) / I-[x1; x2]] ∈ (Cname List)
52. ([fresh-cname(I) / I-[x1]] = I+-[x1] ∈ (Cname List))
∧ (iota(fresh-cname(I))((x1:=i2)(alpha)) = (x1:=i2)(iota'(I)(alpha)) ∈ X([fresh-cname(I) / I-[x1]]))
53. ([fresh-cname(I) / I-[x2]] = I+-[x2] ∈ (Cname List))
∧ (iota(fresh-cname(I))((x2:=i3)(alpha)) = (x2:=i3)(iota'(I)(alpha)) ∈ X([fresh-cname(I) / I-[x2]]))
⊢ A(rename-one-name(fresh-cname(I);fresh-cname(I-[x1; x2]))(((x2:=i3) o (x1:=i2))(iota'(I)(alpha))))
= A(iota'(I-[x1; x2])(((x2:=i3) o (x1:=i2))(alpha)))
∈ Type
2
.....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 : 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)))
33. z : {z:Cname| ¬(z ∈ I-[x1])}
34. v7 : A(iota(fresh-cname(I))((x1:=i2)(alpha)))
35. name-path-endpoints(X;A;a;b;I-[x1];(x1:=i2)(alpha);fresh-cname(I);v7)
36. z = fresh-cname(I) ∈ Cname
37. <fresh-cname(I), v7> = v3 ∈ (Id_A a b)((x1:=i2)(alpha))
38. 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)))}
39. z1 : {z:Cname| ¬(z ∈ I-[x2])}
40. v8 : A(iota(fresh-cname(I))((x2:=i3)(alpha)))
41. name-path-endpoints(X;A;a;b;I-[x2];(x2:=i3)(alpha);fresh-cname(I);v8)
42. z1 = fresh-cname(I) ∈ Cname
43. <fresh-cname(I), v8> = v5 ∈ (Id_A a b)((x2:=i3)(alpha))
44. 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)))}
45. 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))
46. ((x2:=i3) o (x1:=i2)) ∈ name-morph(I;I-[x1; x2])
47. fresh-cname(I-[x1; x2]) = fresh-cname(I-[x1; x2]) ∈ {z:Cname| ¬(z ∈ I-[x1; x2])}
48. (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]))
49. (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)))
50. ((x2:=i3) o (x1:=i2)) ∈ name-morph(I+;I+-[x1; x2])
51. I+-[x1; x2] = [fresh-cname(I) / I-[x1; x2]] ∈ (Cname List)
52. ([fresh-cname(I) / I-[x1]] = I+-[x1] ∈ (Cname List))
∧ (iota(fresh-cname(I))((x1:=i2)(alpha)) = (x1:=i2)(iota'(I)(alpha)) ∈ X([fresh-cname(I) / I-[x1]]))
53. ([fresh-cname(I) / I-[x2]] = I+-[x2] ∈ (Cname List))
∧ (iota(fresh-cname(I))((x2:=i3)(alpha)) = (x2:=i3)(iota'(I)(alpha)) ∈ X([fresh-cname(I) / I-[x2]]))
⊢ ((v7 (x1:=i2)(iota'(I)(alpha)) (x2:=i3)) ((x2:=i3) o (x1:=i2))(iota'(I)(alpha)) rename-one-name(fresh-cname(I);...))
= (v7 iota'(I)((x1:=i2)(alpha)) (x2:=i3)[fresh-cname(I):=fresh-cname(I-[x1; x2])])
∈ A(rename-one-name(fresh-cname(I);fresh-cname(I-[x1; x2]))(((x2:=i3) o (x1:=i2))(iota'(I)(alpha))))
3
.....subterm..... T:t
3: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 : 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)))
33. z : {z:Cname| ¬(z ∈ I-[x1])}
34. v7 : A(iota(fresh-cname(I))((x1:=i2)(alpha)))
35. name-path-endpoints(X;A;a;b;I-[x1];(x1:=i2)(alpha);fresh-cname(I);v7)
36. z = fresh-cname(I) ∈ Cname
37. <fresh-cname(I), v7> = v3 ∈ (Id_A a b)((x1:=i2)(alpha))
38. 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)))}
39. z1 : {z:Cname| ¬(z ∈ I-[x2])}
40. v8 : A(iota(fresh-cname(I))((x2:=i3)(alpha)))
41. name-path-endpoints(X;A;a;b;I-[x2];(x2:=i3)(alpha);fresh-cname(I);v8)
42. z1 = fresh-cname(I) ∈ Cname
43. <fresh-cname(I), v8> = v5 ∈ (Id_A a b)((x2:=i3)(alpha))
44. 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)))}
45. 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))
46. ((x2:=i3) o (x1:=i2)) ∈ name-morph(I;I-[x1; x2])
47. fresh-cname(I-[x1; x2]) = fresh-cname(I-[x1; x2]) ∈ {z:Cname| ¬(z ∈ I-[x1; x2])}
48. (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]))
49. (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)))
50. ((x2:=i3) o (x1:=i2)) ∈ name-morph(I+;I+-[x1; x2])
51. I+-[x1; x2] = [fresh-cname(I) / I-[x1; x2]] ∈ (Cname List)
52. ([fresh-cname(I) / I-[x1]] = I+-[x1] ∈ (Cname List))
∧ (iota(fresh-cname(I))((x1:=i2)(alpha)) = (x1:=i2)(iota'(I)(alpha)) ∈ X([fresh-cname(I) / I-[x1]]))
53. ([fresh-cname(I) / I-[x2]] = I+-[x2] ∈ (Cname List))
∧ (iota(fresh-cname(I))((x2:=i3)(alpha)) = (x2:=i3)(iota'(I)(alpha)) ∈ X([fresh-cname(I) / I-[x2]]))
⊢ ((v8 (x2:=i3)(iota'(I)(alpha)) (x1:=i2)) ((x2:=i3) o (x1:=i2))(iota'(I)(alpha)) rename-one-name(fresh-cname(I);...))
= (v8 iota'(I)((x2:=i3)(alpha)) (x1:=i2)[fresh-cname(I):=fresh-cname(I-[x1; x2])])
∈ A(rename-one-name(fresh-cname(I);fresh-cname(I-[x1; x2]))(((x2:=i3) o (x1:=i2))(iota'(I)(alpha))))
4
.....antecedent.....
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 : 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)))
33. z : {z:Cname| ¬(z ∈ I-[x1])}
34. v7 : A(iota(fresh-cname(I))((x1:=i2)(alpha)))
35. name-path-endpoints(X;A;a;b;I-[x1];(x1:=i2)(alpha);fresh-cname(I);v7)
36. z = fresh-cname(I) ∈ Cname
37. <fresh-cname(I), v7> = v3 ∈ (Id_A a b)((x1:=i2)(alpha))
38. 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)))}
39. z1 : {z:Cname| ¬(z ∈ I-[x2])}
40. v8 : A(iota(fresh-cname(I))((x2:=i3)(alpha)))
41. name-path-endpoints(X;A;a;b;I-[x2];(x2:=i3)(alpha);fresh-cname(I);v8)
42. z1 = fresh-cname(I) ∈ Cname
43. <fresh-cname(I), v8> = v5 ∈ (Id_A a b)((x2:=i3)(alpha))
44. 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)))}
45. 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))
46. ((x2:=i3) o (x1:=i2)) ∈ name-morph(I;I-[x1; x2])
47. fresh-cname(I-[x1; x2]) = fresh-cname(I-[x1; x2]) ∈ {z:Cname| ¬(z ∈ I-[x1; x2])}
48. (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]))
49. (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)))
50. ((x2:=i3) o (x1:=i2)) ∈ name-morph(I+;I+-[x1; x2])
51. I+-[x1; x2] = [fresh-cname(I) / I-[x1; x2]] ∈ (Cname List)
52. ([fresh-cname(I) / I-[x1]] = I+-[x1] ∈ (Cname List))
∧ (iota(fresh-cname(I))((x1:=i2)(alpha)) = (x1:=i2)(iota'(I)(alpha)) ∈ X([fresh-cname(I) / I-[x1]]))
53. ([fresh-cname(I) / I-[x2]] = I+-[x2] ∈ (Cname List))
∧ (iota(fresh-cname(I))((x2:=i3)(alpha)) = (x2:=i3)(iota'(I)(alpha)) ∈ X([fresh-cname(I) / I-[x2]]))
⊢ True
Latex:
Latex:
.....antecedent.....
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 : 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))
32. \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)))
33. z : \{z:Cname| \mneg{}(z \mmember{} I-[x1])\}
34. v7 : A(iota(fresh-cname(I))((x1:=i2)(alpha)))
35. name-path-endpoints(X;A;a;b;I-[x1];(x1:=i2)(alpha);fresh-cname(I);v7)
36. z = fresh-cname(I)
37. <fresh-cname(I), v7> = v3
38. set-path-name(X;A;I-[x1];(x1:=i2)(alpha);fresh-cname(I);v3) = <fresh-cname(I), v7>
39. z1 : \{z:Cname| \mneg{}(z \mmember{} I-[x2])\}
40. v8 : A(iota(fresh-cname(I))((x2:=i3)(alpha)))
41. name-path-endpoints(X;A;a;b;I-[x2];(x2:=i3)(alpha);fresh-cname(I);v8)
42. z1 = fresh-cname(I)
43. <fresh-cname(I), v8> = v5
44. set-path-name(X;A;I-[x2];(x2:=i3)(alpha);fresh-cname(I);v5) = <fresh-cname(I), v8>
45. 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>)
46. ((x2:=i3) o (x1:=i2)) \mmember{} name-morph(I;I-[x1; x2])
47. fresh-cname(I-[x1; x2]) = fresh-cname(I-[x1; x2])
48. (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])])
49. (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])])
50. ((x2:=i3) o (x1:=i2)) \mmember{} name-morph(I+;I+-[x1; x2])
51. I+-[x1; x2] = [fresh-cname(I) / I-[x1; x2]]
52. ([fresh-cname(I) / I-[x1]] = I+-[x1])
\mwedge{} (iota(fresh-cname(I))((x1:=i2)(alpha)) = (x1:=i2)(iota'(I)(alpha)))
53. ([fresh-cname(I) / I-[x2]] = I+-[x2])
\mwedge{} (iota(fresh-cname(I))((x2:=i3)(alpha)) = (x2:=i3)(iota'(I)(alpha)))
\mvdash{} ((v7 (x1:=i2)(iota'(I)(alpha)) (x2:=i3)) ((x2:=i3) o (x1:=i2))(iota'(I)(alpha)) ...)
= ((v8 (x2:=i3)(iota'(I)(alpha)) (x1:=i2)) ((x2:=i3) o (x1:=i2))(iota'(I)(alpha)) ...)
By
Latex:
(NthHypEq (-5) THEN EqCD)
Home
Index