Proof of Nuprl Lemma : lift-id-faces-wf

Step * 1 1 2 1 2 1 2 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) ∧ (v = v3 ∈ (Id_A a b)((x1:=i2)(alpha)))
35. 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)))}
36. v6 : I-path(X;A;a;b;I-[x2];(x2:=i3)(alpha))
37. ((fst(v6)) = fresh-cname(I) ∈ Cname) ∧ (v6 = v5 ∈ (Id_A a b)((x2:=i3)(alpha)))
38. 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)))}
39. (v (x1:=i2)(alpha) (x2:=i3))
= (v6 (x2:=i3)(alpha) (x1:=i2))
∈ cubical-path(X;A;a;b;I-[x1; x2];((x2:=i3) o (x1:=i2))(alpha))
40. ((x2:=i3) o (x1:=i2)) ∈ name-morph(I;I-[x1; x2])
⊢ (snd(v) (x1:=i2)(iota'(I)(alpha)) (x2:=i3))
= (snd(v6) (x2:=i3)(iota'(I)(alpha)) (x1:=i2))
∈ A(((x2:=i3) o (x1:=i2))(iota'(I)(alpha)))
BY
{ (RepUR ``cubical-type-ap-morph`` -2 THEN FLemma `cubical-path-same-name` [-2] THEN Try (QuickAuto)) }

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))

                                                                                     x2];((x2:=i3) o (x1:=i2))(alpha))

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))

                                                                                      x2];((x2:=i3) o (x1:=i2))(alpha))

3
.....antecedent.....
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) ∧ (v = v3 ∈ (Id_A a b)((x1:=i2)(alpha)))
35. 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)))}
36. v6 : I-path(X;A;a;b;I-[x2];(x2:=i3)(alpha))
37. ((fst(v6)) = fresh-cname(I) ∈ Cname) ∧ (v6 = v5 ∈ (Id_A a b)((x2:=i3)(alpha)))
38. 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)))}
39. I-path-morph(X;A;I-[x1];I-[x1; x2];(x2:=i3);(x1:=i2)(alpha);v)
= I-path-morph(X;A;I-[x2];I-[x1; x2];(x1:=i2);(x2:=i3)(alpha);v6)
∈ cubical-path(X;A;a;b;I-[x1; x2];((x2:=i3) o (x1:=i2))(alpha))
40. ((x2:=i3) o (x1:=i2)) ∈ name-morph(I;I-[x1; x2])
⊢ (fst(I-path-morph(X;A;I-[x1];I-[x1; x2];(x2:=i3);(x1:=i2)(alpha);v)))
= (fst(I-path-morph(X;A;I-[x2];I-[x1; x2];(x1:=i2);(x2:=i3)(alpha);v6)))
∈ Cname

4
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))

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)) \mwedge{} (v = v3) 35. set-path-name(X;A;I-[x1];(x1:=i2)(alpha);fresh-cname(I);v3) = v 36. v6 : I-path(X;A;a;b;I-[x2];(x2:=i3)(alpha)) 37. ((fst(v6)) = fresh-cname(I)) \mwedge{} (v6 = v5) 38. set-path-name(X;A;I-[x2];(x2:=i3)(alpha);fresh-cname(I);v5) = v6 39. (v (x1:=i2)(alpha) (x2:=i3)) = (v6 (x2:=i3)(alpha) (x1:=i2)) 40. ((x2:=i3) o (x1:=i2)) \mmember{} name-morph(I;I-[x1; x2]) \mvdash{} (snd(v) (x1:=i2)(iota'(I)(alpha)) (x2:=i3)) = (snd(v6) (x2:=i3)(iota'(I)(alpha)) (x1:=i2)) By Latex: (RepUR ``cubical-type-ap-morph`` -2 THEN FLemma `cubical-path-same-name` [-2] THEN Try (QuickAuto)) Home Index