Step
*
1
1
2
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. (¬(x = y ∈ Cname)) ⇒ ((f2 (x:=i)(alpha) (y:=i1)) = (f4 (y:=i1)(alpha) (x:=i)) ∈ A(((y:=i1) o (x:=i))(alpha)))
18. f y ∈ nameset(K)
19. f x ∈ nameset(K)
20. ¬((f x) = (f y) ∈ Cname)
21. ¬(x = y ∈ Cname)
22. y ∈ nameset(I-[x])
23. x ∈ nameset(I-[y])
24. f ∈ name-morph(I-[x];K-[f x])
25. f ∈ name-morph(I-[y];K-[f y])
26. ((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)))
⊢ ((f2 (x:=i)(alpha) f) (f x:=i)(f(alpha)) (f y:=i1))
= ((f4 (y:=i1)(alpha) f) (f y:=i1)(f(alpha)) (f x:=i))
∈ A(((f y:=i1) o (f x:=i))(f(alpha)))
BY
{ TACTIC:(Assert ((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))) BY
(BLemma `cubical-type-ap-morph-comp` ⋅ THENA Auto)) }
1
.....aux.....
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. (f2 (x:=i)(alpha) (y:=i1)) = (f4 (y:=i1)(alpha) (x:=i)) ∈ A(((y:=i1) o (x:=i))(alpha))
⊢ (f x:=i) ∈ name-morph(K-[f y];K-[f x; f y])
2
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. (¬(x = y ∈ Cname)) ⇒ ((f2 (x:=i)(alpha) (y:=i1)) = (f4 (y:=i1)(alpha) (x:=i)) ∈ A(((y:=i1) o (x:=i))(alpha)))
18. f y ∈ nameset(K)
19. f x ∈ nameset(K)
20. ¬((f x) = (f y) ∈ Cname)
21. ¬(x = y ∈ Cname)
22. y ∈ nameset(I-[x])
23. x ∈ nameset(I-[y])
24. f ∈ name-morph(I-[x];K-[f x])
25. f ∈ name-morph(I-[y];K-[f y])
26. ((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)))
27. ((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)))
⊢ ((f2 (x:=i)(alpha) f) (f x:=i)(f(alpha)) (f y:=i1))
= ((f4 (y:=i1)(alpha) f) (f y:=i1)(f(alpha)) (f x:=i))
∈ A(((f y:=i1) o (f x:=i))(f(alpha)))
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. (\mneg{}(x = y)) {}\mRightarrow{} ((f2 (x:=i)(alpha) (y:=i1)) = (f4 (y:=i1)(alpha) (x:=i)))
18. f y \mmember{} nameset(K)
19. f x \mmember{} nameset(K)
20. \mneg{}((f x) = (f y))
21. \mneg{}(x = y)
22. y \mmember{} nameset(I-[x])
23. x \mmember{} nameset(I-[y])
24. f \mmember{} name-morph(I-[x];K-[f x])
25. f \mmember{} name-morph(I-[y];K-[f y])
26. ((f2 (x:=i)(alpha) f) f((x:=i)(alpha)) (f y:=i1)) = (f2 (x:=i)(alpha) (f o (f y:=i1)))
\mvdash{} ((f2 (x:=i)(alpha) f) (f x:=i)(f(alpha)) (f y:=i1))
= ((f4 (y:=i1)(alpha) f) (f y:=i1)(f(alpha)) (f x:=i))
By
Latex:
TACTIC:(Assert ((f4 (y:=i1)(alpha) f) f((y:=i1)(alpha)) (f x:=i))
= (f4 (y:=i1)(alpha) (f o (f x:=i))) BY
(BLemma `cubical-type-ap-morph-comp` \mcdot{} THENA Auto))
Home
Index