---

Step * 1 2 1 1 1 1 1 of Lemma groupoid-edges-commute1


1. G : Groupoid
2. I : Cname List
3. J : nameset(I) List
4. j : nameset(I)
5. (j ∈ J)
6. (∀j'∈J.j' = j ∈ Cname)
7. x : nameset(I)
8. i : ℕ2
9. box : open_box(cubical-nerve(cat(G));I;J;x;i)
10. f : name-morph(I;[])
11. a : nameset(I)
12. ¬(a = j ∈ Cname)
13. (f a) = 0 ∈ ℕ2
14. b : nameset(I)
15. ¬(b = j ∈ Cname)
16. (f b) = 0 ∈ ℕ2
17. ¬(a = b ∈ nameset(I))
18. get_face(j;f j;box) ∈ I-face(cubical-nerve(cat(G));I)
19. x1 : nameset(I)
20. v2 : ℕ2
21. v3 : cubical-nerve(cat(G))(I-[x1])
22. get_face(j;f j;box) = <x1, v2, v3> ∈ I-face(cubical-nerve(cat(G));I)
23. (<x1, v2, v3> ∈ box)
24. <x1, v2> = <j, f j> ∈ (nameset(I) × ℕ2)
⊢ (¬(x1 = b ∈ Cname)) ∧ (¬(x1 = a ∈ Cname)) ∧ (v2 = (f x1) ∈ ℕ2)
BY
{ ((EqHD (-1) THENA Auto) THEN All Reduce) }

1
1. G : Groupoid
2. I : Cname List
3. J : nameset(I) List
4. j : nameset(I)
5. (j ∈ J)
6. (∀j'∈J.j' = j ∈ Cname)
7. x : nameset(I)
8. i : ℕ2
9. box : open_box(cubical-nerve(cat(G));I;J;x;i)
10. f : name-morph(I;[])
11. a : nameset(I)
12. ¬(a = j ∈ Cname)
13. (f a) = 0 ∈ ℕ2
14. b : nameset(I)
15. ¬(b = j ∈ Cname)
16. (f b) = 0 ∈ ℕ2
17. ¬(a = b ∈ nameset(I))
18. get_face(j;f j;box) ∈ I-face(cubical-nerve(cat(G));I)
19. x1 : nameset(I)
20. v2 : ℕ2
21. v3 : cubical-nerve(cat(G))(I-[x1])
22. get_face(j;f j;box) = <x1, v2, v3> ∈ I-face(cubical-nerve(cat(G));I)
23. (<x1, v2, v3> ∈ box)
24. x1 = j ∈ nameset(I)
25. v2 = (f j) ∈ ℕ2
⊢ (¬(x1 = b ∈ Cname)) ∧ (¬(x1 = a ∈ Cname)) ∧ (v2 = (f x1) ∈ ℕ2)

---

Latex:

---

Latex:

1.  G  :  Groupoid
2.  I  :  Cname  List
3.  J  :  nameset(I)  List
4.  j  :  nameset(I)
5.  (j  \mmember{}  J)
6.  (\mforall{}j'\mmember{}J.j'  =  j)
7.  x  :  nameset(I)
8.  i  :  \mBbbN{}2
9.  box  :  open\_box(cubical-nerve(cat(G));I;J;x;i)
10.  f  :  name-morph(I;[])
11.  a  :  nameset(I)
12.  \mneg{}(a  =  j)
13.  (f  a)  =  0
14.  b  :  nameset(I)
15.  \mneg{}(b  =  j)
16.  (f  b)  =  0
17.  \mneg{}(a  =  b)
18.  get\_face(j;f  j;box)  \mmember{}  I-face(cubical-nerve(cat(G));I)
19.  x1  :  nameset(I)
20.  v2  :  \mBbbN{}2
21.  v3  :  cubical-nerve(cat(G))(I-[x1])
22.  get\_face(j;f  j;box)  =  <x1,  v2,  v3>
23.  (<x1,  v2,  v3>  \mmember{}  box)
24.  <x1,  v2>  =  <j,  f  j>
\mvdash{}  (\mneg{}(x1  =  b))  \mwedge{}  (\mneg{}(x1  =  a))  \mwedge{}  (v2  =  (f  x1))


By

---

Latex:
((EqHD  (-1)  THENA  Auto)  THEN  All  Reduce)

---

Home Index