Step
*
1
1
2
1
1
2
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))
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. v : I-path(X;A;a;b;I-[x1];(x1:=i2)(alpha))
34. (fst(v)) = fresh-cname(I) ∈ Cname
35. v = v3 ∈ (Id_A a b)((x1:=i2)(alpha))
36. set-path-name(X;A;I-[x1];(x1:=i2)(alpha);fresh-cname(I);v3)
= v
∈ {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)))}
37. v6 : I-path(X;A;a;b;I-[x2];(x2:=i3)(alpha))
38. (fst(v6)) = fresh-cname(I) ∈ Cname
39. v6 = v5 ∈ (Id_A a b)((x2:=i3)(alpha))
40. set-path-name(X;A;I-[x2];(x2:=i3)(alpha);fresh-cname(I);v5)
= v6
∈ {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)))}
⊢ ((x2:=i3) o (x1:=i2))(alpha) = (x2:=i3)((x1:=i2)(alpha)) ∈ X(I-[x1; x2])
BY
{ TACTIC:(RWO "cube-set-restriction-comp" 0 THEN Try (Complete (Auto))) }
1
.....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))
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. v : I-path(X;A;a;b;I-[x1];(x1:=i2)(alpha))
34. (fst(v)) = fresh-cname(I) ∈ Cname
35. v = v3 ∈ (Id_A a b)((x1:=i2)(alpha))
36. set-path-name(X;A;I-[x1];(x1:=i2)(alpha);fresh-cname(I);v3)
= v
∈ {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)))}
37. v6 : I-path(X;A;a;b;I-[x2];(x2:=i3)(alpha))
38. (fst(v6)) = fresh-cname(I) ∈ Cname
39. v6 = v5 ∈ (Id_A a b)((x2:=i3)(alpha))
40. set-path-name(X;A;I-[x2];(x2:=i3)(alpha);fresh-cname(I);v5)
= v6
∈ {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)))}
⊢ ((x2:=i3) o (x1:=i2))(alpha) = ((x2:=i3) o (x1:=i2))(alpha) ∈ X(I-[x1; x2])
2
.....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))
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. v : I-path(X;A;a;b;I-[x1];(x1:=i2)(alpha))
34. (fst(v)) = fresh-cname(I) ∈ Cname
35. v = v3 ∈ (Id_A a b)((x1:=i2)(alpha))
36. set-path-name(X;A;I-[x1];(x1:=i2)(alpha);fresh-cname(I);v3)
= v
∈ {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)))}
37. v6 : I-path(X;A;a;b;I-[x2];(x2:=i3)(alpha))
38. (fst(v6)) = fresh-cname(I) ∈ Cname
39. v6 = v5 ∈ (Id_A a b)((x2:=i3)(alpha))
40. set-path-name(X;A;I-[x2];(x2:=i3)(alpha);fresh-cname(I);v5)
= v6
∈ {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)))}
⊢ (x2:=i3) ∈ name-morph(I-[x1];I-[x1; x2])
3
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)))
33. v : I-path(X;A;a;b;I-[x1];(x1:=i2)(alpha))
34. (fst(v)) = fresh-cname(I) ∈ Cname
35. v = v3 ∈ (Id_A a b)((x1:=i2)(alpha))
36. set-path-name(X;A;I-[x1];(x1:=i2)(alpha);fresh-cname(I);v3)
= v
∈ {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)))}
37. v6 : I-path(X;A;a;b;I-[x2];(x2:=i3)(alpha))
38. (fst(v6)) = fresh-cname(I) ∈ Cname
39. v6 = v5 ∈ (Id_A a b)((x2:=i3)(alpha))
40. set-path-name(X;A;I-[x2];(x2:=i3)(alpha);fresh-cname(I);v5)
= v6
∈ {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)))}
⊢ ((x2:=i3) o (x1:=i2))(alpha) = ((x1:=i2) o (x2:=i3))(alpha) ∈ X(I-[x1; x2])
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))
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. v : I-path(X;A;a;b;I-[x1];(x1:=i2)(alpha))
34. (fst(v)) = fresh-cname(I)
35. v = v3
36. set-path-name(X;A;I-[x1];(x1:=i2)(alpha);fresh-cname(I);v3) = v
37. v6 : I-path(X;A;a;b;I-[x2];(x2:=i3)(alpha))
38. (fst(v6)) = fresh-cname(I)
39. v6 = v5
40. set-path-name(X;A;I-[x2];(x2:=i3)(alpha);fresh-cname(I);v5) = v6
\mvdash{} ((x2:=i3) o (x1:=i2))(alpha) = (x2:=i3)((x1:=i2)(alpha))
By
Latex:
TACTIC:(RWO "cube-set-restriction-comp" 0 THEN Try (Complete (Auto)))
Home
Index