---

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

.....assertion..... 
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 y:=i1) ∈ name-morph(K-[f x];K-[f x; f y])
29. (f x:=i) ∈ name-morph(K-[f y];K-[f x; f y])
⊢ f((x:=i)(alpha)) = (f x:=i)(f(alpha)) ∈ X(K-[f x])
BY
{ TACTIC:((RWO  "cube-set-restriction-comp" 0 THENM EqCD) THEN Auto) }

1
.....subterm..... T:t
4: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 y:=i1) ∈ name-morph(K-[f x];K-[f x; f y])
29. (f x:=i) ∈ name-morph(K-[f y];K-[f x; f y])
⊢ ((x:=i) o f) = (f o (f x:=i)) ∈ name-morph(I;K-[f x])

---

Latex:

---

Latex:
.....assertion..... 
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  y:=i1)  \mmember{}  name-morph(K-[f  x];K-[f  x;  f  y])
29.  (f  x:=i)  \mmember{}  name-morph(K-[f  y];K-[f  x;  f  y])
\mvdash{}  f((x:=i)(alpha))  =  (f  x:=i)(f(alpha))


By

---

Latex:
TACTIC:((RWO    "cube-set-restriction-comp"  0  THENM  EqCD)  THEN  Auto)

---

Home Index