Proof of Nuprl Lemma : A-face-compatible-image

Step * 1 1 2 2 3 3 2 1 1 of Lemma A-face-compatible-image

1. X : CubicalSet
2. A : {X ⊢ _}
3. I : Cname List
4. K : Cname List
5. f : name-morph(I;K)
6. alpha : X(I)
7. x : Cname
8. (x ∈ I)
9. i : ℕ2
10. f2 : A((x:=i)(alpha))
11. y : Cname
12. (y ∈ I)
13. i1 : ℕ2
14. f4 : A((y:=i1)(alpha))
15. ↑isname(f x)
16. ↑isname(f y)
17. f y ∈ nameset(K)
18. f x ∈ nameset(K)
19. ¬((f x) = (f y) ∈ Cname)
20. ¬(x = y ∈ Cname)
21. y ∈ nameset(I-[x])
22. x ∈ nameset(I-[y])
23. f ∈ name-morph(I-[x];K-[f x])
24. f ∈ name-morph(I-[y];K-[f y])
25. ((f2 (x:=i)(alpha) f) f((x:=i)(alpha)) (f y:=i1))
= (f2 (x:=i)(alpha) (f o (f y:=i1)))
∈ A((f o (f y:=i1))((x:=i)(alpha)))
26. ((f4 (y:=i1)(alpha) f) f((y:=i1)(alpha)) (f x:=i))
= (f4 (y:=i1)(alpha) (f o (f x:=i)))
∈ A((f o (f x:=i))((y:=i1)(alpha)))
27. (f2 (x:=i)(alpha) (y:=i1)) = (f4 (y:=i1)(alpha) (x:=i)) ∈ A(((y:=i1) o (x:=i))(alpha))
28. f ∈ name-morph(I-[x; y];K-[f x; f y])
29. ((y:=i1) o (x:=i)) ∈ name-morph(I;I-[x; y])
30. f(((y:=i1) o (x:=i))(alpha)) = ((f y:=i1) o (f x:=i))(f(alpha)) ∈ X(K-[f x; f y])
31. ((f2 (x:=i)(alpha) (y:=i1)) ((y:=i1) o (x:=i))(alpha) f)
= ((f4 (y:=i1)(alpha) (x:=i)) ((y:=i1) o (x:=i))(alpha) f)
∈ A(((f y:=i1) o (f x:=i))(f(alpha)))

⊢ (f2 (x:=i)(alpha) ((y:=i1) o f)) = (f4 (y:=i1)(alpha) ((x:=i) o f)) ∈ A(((f y:=i1) o (f x:=i))(f(alpha)))

BY
{ TACTIC:(NthHypEq (-1) THEN EqCD) }

1
.....subterm..... T:t
1:n
1. X : CubicalSet
2. A : {X ⊢ _}
3. I : Cname List
4. K : Cname List
5. f : name-morph(I;K)
6. alpha : X(I)
7. x : Cname
8. (x ∈ I)
9. i : ℕ2
10. f2 : A((x:=i)(alpha))
11. y : Cname
12. (y ∈ I)
13. i1 : ℕ2
14. f4 : A((y:=i1)(alpha))
15. ↑isname(f x)
16. ↑isname(f y)
17. f y ∈ nameset(K)
18. f x ∈ nameset(K)
19. ¬((f x) = (f y) ∈ Cname)
20. ¬(x = y ∈ Cname)
21. y ∈ nameset(I-[x])
22. x ∈ nameset(I-[y])
23. f ∈ name-morph(I-[x];K-[f x])
24. f ∈ name-morph(I-[y];K-[f y])
25. ((f2 (x:=i)(alpha) f) f((x:=i)(alpha)) (f y:=i1))
= (f2 (x:=i)(alpha) (f o (f y:=i1)))
∈ A((f o (f y:=i1))((x:=i)(alpha)))
26. ((f4 (y:=i1)(alpha) f) f((y:=i1)(alpha)) (f x:=i))
= (f4 (y:=i1)(alpha) (f o (f x:=i)))
∈ A((f o (f x:=i))((y:=i1)(alpha)))
27. (f2 (x:=i)(alpha) (y:=i1)) = (f4 (y:=i1)(alpha) (x:=i)) ∈ A(((y:=i1) o (x:=i))(alpha))
28. f ∈ name-morph(I-[x; y];K-[f x; f y])
29. ((y:=i1) o (x:=i)) ∈ name-morph(I;I-[x; y])
30. f(((y:=i1) o (x:=i))(alpha)) = ((f y:=i1) o (f x:=i))(f(alpha)) ∈ X(K-[f x; f y])
31. ((f2 (x:=i)(alpha) (y:=i1)) ((y:=i1) o (x:=i))(alpha) f)
= ((f4 (y:=i1)(alpha) (x:=i)) ((y:=i1) o (x:=i))(alpha) f)
∈ A(((f y:=i1) o (f x:=i))(f(alpha)))
⊢ A(((f y:=i1) o (f x:=i))(f(alpha))) = A(((f y:=i1) o (f x:=i))(f(alpha))) ∈ Type

2
.....subterm..... T:t
2:n
1. X : CubicalSet
2. A : {X ⊢ _}
3. I : Cname List
4. K : Cname List
5. f : name-morph(I;K)
6. alpha : X(I)
7. x : Cname
8. (x ∈ I)
9. i : ℕ2
10. f2 : A((x:=i)(alpha))
11. y : Cname
12. (y ∈ I)
13. i1 : ℕ2
14. f4 : A((y:=i1)(alpha))
15. ↑isname(f x)
16. ↑isname(f y)
17. f y ∈ nameset(K)
18. f x ∈ nameset(K)
19. ¬((f x) = (f y) ∈ Cname)
20. ¬(x = y ∈ Cname)
21. y ∈ nameset(I-[x])
22. x ∈ nameset(I-[y])
23. f ∈ name-morph(I-[x];K-[f x])
24. f ∈ name-morph(I-[y];K-[f y])
25. ((f2 (x:=i)(alpha) f) f((x:=i)(alpha)) (f y:=i1))
= (f2 (x:=i)(alpha) (f o (f y:=i1)))
∈ A((f o (f y:=i1))((x:=i)(alpha)))
26. ((f4 (y:=i1)(alpha) f) f((y:=i1)(alpha)) (f x:=i))
= (f4 (y:=i1)(alpha) (f o (f x:=i)))
∈ A((f o (f x:=i))((y:=i1)(alpha)))
27. (f2 (x:=i)(alpha) (y:=i1)) = (f4 (y:=i1)(alpha) (x:=i)) ∈ A(((y:=i1) o (x:=i))(alpha))
28. f ∈ name-morph(I-[x; y];K-[f x; f y])
29. ((y:=i1) o (x:=i)) ∈ name-morph(I;I-[x; y])
30. f(((y:=i1) o (x:=i))(alpha)) = ((f y:=i1) o (f x:=i))(f(alpha)) ∈ X(K-[f x; f y])
31. ((f2 (x:=i)(alpha) (y:=i1)) ((y:=i1) o (x:=i))(alpha) f)
= ((f4 (y:=i1)(alpha) (x:=i)) ((y:=i1) o (x:=i))(alpha) f)
∈ A(((f y:=i1) o (f x:=i))(f(alpha)))
⊢ (f2 (x:=i)(alpha) ((y:=i1) o f))
= ((f2 (x:=i)(alpha) (y:=i1)) ((y:=i1) o (x:=i))(alpha) f)
∈ A(((f y:=i1) o (f x:=i))(f(alpha)))

3
.....subterm..... T:t
3:n
1. X : CubicalSet
2. A : {X ⊢ _}
3. I : Cname List
4. K : Cname List
5. f : name-morph(I;K)
6. alpha : X(I)
7. x : Cname
8. (x ∈ I)
9. i : ℕ2
10. f2 : A((x:=i)(alpha))
11. y : Cname
12. (y ∈ I)
13. i1 : ℕ2
14. f4 : A((y:=i1)(alpha))
15. ↑isname(f x)
16. ↑isname(f y)
17. f y ∈ nameset(K)
18. f x ∈ nameset(K)
19. ¬((f x) = (f y) ∈ Cname)
20. ¬(x = y ∈ Cname)
21. y ∈ nameset(I-[x])
22. x ∈ nameset(I-[y])
23. f ∈ name-morph(I-[x];K-[f x])
24. f ∈ name-morph(I-[y];K-[f y])
25. ((f2 (x:=i)(alpha) f) f((x:=i)(alpha)) (f y:=i1))
= (f2 (x:=i)(alpha) (f o (f y:=i1)))
∈ A((f o (f y:=i1))((x:=i)(alpha)))
26. ((f4 (y:=i1)(alpha) f) f((y:=i1)(alpha)) (f x:=i))
= (f4 (y:=i1)(alpha) (f o (f x:=i)))
∈ A((f o (f x:=i))((y:=i1)(alpha)))
27. (f2 (x:=i)(alpha) (y:=i1)) = (f4 (y:=i1)(alpha) (x:=i)) ∈ A(((y:=i1) o (x:=i))(alpha))
28. f ∈ name-morph(I-[x; y];K-[f x; f y])
29. ((y:=i1) o (x:=i)) ∈ name-morph(I;I-[x; y])
30. f(((y:=i1) o (x:=i))(alpha)) = ((f y:=i1) o (f x:=i))(f(alpha)) ∈ X(K-[f x; f y])
31. ((f2 (x:=i)(alpha) (y:=i1)) ((y:=i1) o (x:=i))(alpha) f)
= ((f4 (y:=i1)(alpha) (x:=i)) ((y:=i1) o (x:=i))(alpha) f)
∈ A(((f y:=i1) o (f x:=i))(f(alpha)))
⊢ (f4 (y:=i1)(alpha) ((x:=i) o f))
= ((f4 (y:=i1)(alpha) (x:=i)) ((y:=i1) o (x:=i))(alpha) f)
∈ A(((f y:=i1) o (f x:=i))(f(alpha)))

4
.....antecedent.....
1. X : CubicalSet
2. A : {X ⊢ _}
3. I : Cname List
4. K : Cname List
5. f : name-morph(I;K)
6. alpha : X(I)
7. x : Cname
8. (x ∈ I)
9. i : ℕ2
10. f2 : A((x:=i)(alpha))
11. y : Cname
12. (y ∈ I)
13. i1 : ℕ2
14. f4 : A((y:=i1)(alpha))
15. ↑isname(f x)
16. ↑isname(f y)
17. f y ∈ nameset(K)
18. f x ∈ nameset(K)
19. ¬((f x) = (f y) ∈ Cname)
20. ¬(x = y ∈ Cname)
21. y ∈ nameset(I-[x])
22. x ∈ nameset(I-[y])
23. f ∈ name-morph(I-[x];K-[f x])
24. f ∈ name-morph(I-[y];K-[f y])
25. ((f2 (x:=i)(alpha) f) f((x:=i)(alpha)) (f y:=i1))
= (f2 (x:=i)(alpha) (f o (f y:=i1)))
∈ A((f o (f y:=i1))((x:=i)(alpha)))
26. ((f4 (y:=i1)(alpha) f) f((y:=i1)(alpha)) (f x:=i))
= (f4 (y:=i1)(alpha) (f o (f x:=i)))
∈ A((f o (f x:=i))((y:=i1)(alpha)))
27. (f2 (x:=i)(alpha) (y:=i1)) = (f4 (y:=i1)(alpha) (x:=i)) ∈ A(((y:=i1) o (x:=i))(alpha))
28. f ∈ name-morph(I-[x; y];K-[f x; f y])
29. ((y:=i1) o (x:=i)) ∈ name-morph(I;I-[x; y])
30. f(((y:=i1) o (x:=i))(alpha)) = ((f y:=i1) o (f x:=i))(f(alpha)) ∈ X(K-[f x; f y])
31. ((f2 (x:=i)(alpha) (y:=i1)) ((y:=i1) o (x:=i))(alpha) f)
= ((f4 (y:=i1)(alpha) (x:=i)) ((y:=i1) o (x:=i))(alpha) f)
∈ A(((f y:=i1) o (f x:=i))(f(alpha)))
⊢ True

Latex:

Latex:
1. X : CubicalSet 2. A : \{X \mvdash{} \_\} 3. I : Cname List 4. K : Cname List 5. f : name-morph(I;K) 6. alpha : X(I) 7. x : Cname 8. (x \mmember{} I) 9. i : \mBbbN{}2 10. f2 : A((x:=i)(alpha)) 11. y : Cname 12. (y \mmember{} I) 13. i1 : \mBbbN{}2 14. f4 : A((y:=i1)(alpha)) 15. \muparrow{}isname(f x) 16. \muparrow{}isname(f y) 17. f y \mmember{} nameset(K) 18. f x \mmember{} nameset(K) 19. \mneg{}((f x) = (f y)) 20. \mneg{}(x = y) 21. y \mmember{} nameset(I-[x]) 22. x \mmember{} nameset(I-[y]) 23. f \mmember{} name-morph(I-[x];K-[f x]) 24. f \mmember{} name-morph(I-[y];K-[f y]) 25. ((f2 (x:=i)(alpha) f) f((x:=i)(alpha)) (f y:=i1)) = (f2 (x:=i)(alpha) (f o (f y:=i1))) 26. ((f4 (y:=i1)(alpha) f) f((y:=i1)(alpha)) (f x:=i)) = (f4 (y:=i1)(alpha) (f o (f x:=i))) 27. (f2 (x:=i)(alpha) (y:=i1)) = (f4 (y:=i1)(alpha) (x:=i)) 28. f \mmember{} name-morph(I-[x; y];K-[f x; f y]) 29. ((y:=i1) o (x:=i)) \mmember{} name-morph(I;I-[x; y]) 30. f(((y:=i1) o (x:=i))(alpha)) = ((f y:=i1) o (f x:=i))(f(alpha)) 31. ((f2 (x:=i)(alpha) (y:=i1)) ((y:=i1) o (x:=i))(alpha) f) = ((f4 (y:=i1)(alpha) (x:=i)) ((y:=i1) o (x:=i))(alpha) f) \mvdash{} (f2 (x:=i)(alpha) ((y:=i1) o f)) = (f4 (y:=i1)(alpha) ((x:=i) o f)) By Latex: TACTIC:(NthHypEq (-1) THEN EqCD) Home Index