---

Step * 2 1 1 7 1 2 2 of Lemma face-compatible-image


1. X : CubicalSet
2. I : Cname List
3. K : Cname List
4. f : name-morph(I;K)
5. x : Cname
6. (x ∈ I)
7. f2 : ℕ2
8. f3 : X(I-[x])
9. y : Cname
10. (y ∈ I)
11. f5 : ℕ2
12. f6 : X(I-[y])
13. ↑isname(f x)
14. ↑isname(f y)
15. f y ∈ nameset(K)
16. f x ∈ nameset(K)
17. ¬((f x) = (f y) ∈ Cname)
18. ¬(x = y ∈ Cname)
19. y ∈ nameset(I-[x])
20. x ∈ nameset(I-[y])
21. f ∈ name-morph(I-[x];K-[f x])
22. f ∈ name-morph(I-[y];K-[f y])
23. f ∈ name-morph(I-[x; y];K-[f x; f y])
24. (y:=f5)(f3) = (x:=f2)(f6) ∈ X(I-[x; y])
25. (f o (f y:=f5))(f3) = f((y:=f5)(f3)) ∈ X(K-[f x; f y])
⊢ (f o (f y:=f5))(f3) = (f o (f x:=f2))(f6) ∈ X(K-[f x; f y])
BY
{ xxxAssert ⌜(f o (f x:=f2))(f6) = f((x:=f2)(f6)) ∈ X(K-[f x; f y])⌝⋅xxx }

1
.....assertion..... 
1. X : CubicalSet
2. I : Cname List
3. K : Cname List
4. f : name-morph(I;K)
5. x : Cname
6. (x ∈ I)
7. f2 : ℕ2
8. f3 : X(I-[x])
9. y : Cname
10. (y ∈ I)
11. f5 : ℕ2
12. f6 : X(I-[y])
13. ↑isname(f x)
14. ↑isname(f y)
15. f y ∈ nameset(K)
16. f x ∈ nameset(K)
17. ¬((f x) = (f y) ∈ Cname)
18. ¬(x = y ∈ Cname)
19. y ∈ nameset(I-[x])
20. x ∈ nameset(I-[y])
21. f ∈ name-morph(I-[x];K-[f x])
22. f ∈ name-morph(I-[y];K-[f y])
23. f ∈ name-morph(I-[x; y];K-[f x; f y])
24. (y:=f5)(f3) = (x:=f2)(f6) ∈ X(I-[x; y])
25. (f o (f y:=f5))(f3) = f((y:=f5)(f3)) ∈ X(K-[f x; f y])
⊢ (f o (f x:=f2))(f6) = f((x:=f2)(f6)) ∈ X(K-[f x; f y])

2
1. X : CubicalSet
2. I : Cname List
3. K : Cname List
4. f : name-morph(I;K)
5. x : Cname
6. (x ∈ I)
7. f2 : ℕ2
8. f3 : X(I-[x])
9. y : Cname
10. (y ∈ I)
11. f5 : ℕ2
12. f6 : X(I-[y])
13. ↑isname(f x)
14. ↑isname(f y)
15. f y ∈ nameset(K)
16. f x ∈ nameset(K)
17. ¬((f x) = (f y) ∈ Cname)
18. ¬(x = y ∈ Cname)
19. y ∈ nameset(I-[x])
20. x ∈ nameset(I-[y])
21. f ∈ name-morph(I-[x];K-[f x])
22. f ∈ name-morph(I-[y];K-[f y])
23. f ∈ name-morph(I-[x; y];K-[f x; f y])
24. (y:=f5)(f3) = (x:=f2)(f6) ∈ X(I-[x; y])
25. (f o (f y:=f5))(f3) = f((y:=f5)(f3)) ∈ X(K-[f x; f y])
26. (f o (f x:=f2))(f6) = f((x:=f2)(f6)) ∈ X(K-[f x; f y])
⊢ (f o (f y:=f5))(f3) = (f o (f x:=f2))(f6) ∈ X(K-[f x; f y])

---

Latex:

---

Latex:

1.  X  :  CubicalSet
2.  I  :  Cname  List
3.  K  :  Cname  List
4.  f  :  name-morph(I;K)
5.  x  :  Cname
6.  (x  \mmember{}  I)
7.  f2  :  \mBbbN{}2
8.  f3  :  X(I-[x])
9.  y  :  Cname
10.  (y  \mmember{}  I)
11.  f5  :  \mBbbN{}2
12.  f6  :  X(I-[y])
13.  \muparrow{}isname(f  x)
14.  \muparrow{}isname(f  y)
15.  f  y  \mmember{}  nameset(K)
16.  f  x  \mmember{}  nameset(K)
17.  \mneg{}((f  x)  =  (f  y))
18.  \mneg{}(x  =  y)
19.  y  \mmember{}  nameset(I-[x])
20.  x  \mmember{}  nameset(I-[y])
21.  f  \mmember{}  name-morph(I-[x];K-[f  x])
22.  f  \mmember{}  name-morph(I-[y];K-[f  y])
23.  f  \mmember{}  name-morph(I-[x;  y];K-[f  x;  f  y])
24.  (y:=f5)(f3)  =  (x:=f2)(f6)
25.  (f  o  (f  y:=f5))(f3)  =  f((y:=f5)(f3))
\mvdash{}  (f  o  (f  y:=f5))(f3)  =  (f  o  (f  x:=f2))(f6)


By

---

Latex:
xxxAssert  \mkleeneopen{}(f  o  (f  x:=f2))(f6)  =  f((x:=f2)(f6))\mkleeneclose{}\mcdot{}xxx

---

Home Index