---

Step * 1 1 4 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 : ℤ
9. box : open_box(cubical-nerve(cat(G));I;J;x;0)
10. f : name-morph(I;[])
11. f x ≠ 0
12. a : nameset(I)
13. flip(f;a) x ≠ 0
14. ¬(a = j ∈ Cname)
15. (f a) = 0 ∈ ℕ2
16. (f j) = 0 ∈ ℕ2
17. ¬(x = j ∈ Cname)
18. i = 0 ∈ ℤ
19. (f x) = 1 ∈ ℕ2
20. (flip(f;a) x) = 1 ∈ ℕ2
21. v : {d:cat-arrow(cat(G)) nerve_box_label(box;flip(f;a)) nerve_box_label(box;flip(flip(f;a);j))| 
         nerve_box_edge(box;flip(flip(f;a);x);j) o nerve_box_edge(box;flip(flip(flip(f;a);x);j);x)
         = nerve_box_edge(box;flip(flip(f;a);x);x) o d} 
22. groupoid-square1(G;nerve_box_label(box;flip(flip(f;a);x));nerve_box_label(box;flip(flip(flip(f;a);x);j));
    nerve_box_label(box;flip(f;a));nerve_box_label(box;flip(flip(f;a);j));nerve_box_edge(box;flip(flip(f;a);x);j);
    nerve_box_edge(box;flip(flip(flip(f;a);x);j);x);nerve_box_edge(box;flip(flip(f;a);x);x))
= v
∈ {d:cat-arrow(cat(G)) nerve_box_label(box;flip(f;a)) nerve_box_label(box;flip(flip(f;a);j))| 
   nerve_box_edge(box;flip(flip(f;a);x);j) o nerve_box_edge(box;flip(flip(flip(f;a);x);j);x)
   = nerve_box_edge(box;flip(flip(f;a);x);x) o d} 
23. v1 : {d:cat-arrow(cat(G)) nerve_box_label(box;f) nerve_box_label(box;flip(f;j))| 
          nerve_box_edge(box;flip(f;x);j) o nerve_box_edge(box;flip(flip(f;x);j);x)
          = nerve_box_edge(box;flip(f;x);x) o d} 
24. groupoid-square1(G;nerve_box_label(box;flip(f;x));nerve_box_label(box;flip(flip(f;x);j));nerve_box_label(box;f);
    nerve_box_label(box;flip(f;j));nerve_box_edge(box;flip(f;x);j);nerve_box_edge(box;flip(flip(f;x);j);x);
    nerve_box_edge(box;flip(f;x);x))
= v1
∈ {d:cat-arrow(cat(G)) nerve_box_label(box;f) nerve_box_label(box;flip(f;j))| 
   nerve_box_edge(box;flip(f;x);j) o nerve_box_edge(box;flip(flip(f;x);j);x) = nerve_box_edge(box;flip(f;x);x) o d} 
⊢ (cat-comp(cat(G)) nerve_box_label(box;f) nerve_box_label(box;flip(f;a)) nerve_box_label(box;flip(flip(f;a);j)) 
   nerve_box_edge(box;f;a) 
   v)
= (cat-comp(cat(G)) nerve_box_label(box;f) nerve_box_label(box;flip(f;j)) nerve_box_label(box;flip(flip(f;j);a)) v1 
   nerve_box_edge(box;flip(f;j);a))
∈ (cat-arrow(cat(G)) nerve_box_label(box;f) nerve_box_label(box;flip(flip(f;a);j)))
BY
{ ((D -4 THEN D -2) THEN Assert ⌜nerve_box_edge(box;f;a) o v = v1 o nerve_box_edge(box;flip(f;j);a)⌝⋅) }

1
.....assertion..... 
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 : ℤ
9. box : open_box(cubical-nerve(cat(G));I;J;x;0)
10. f : name-morph(I;[])
11. f x ≠ 0
12. a : nameset(I)
13. flip(f;a) x ≠ 0
14. ¬(a = j ∈ Cname)
15. (f a) = 0 ∈ ℕ2
16. (f j) = 0 ∈ ℕ2
17. ¬(x = j ∈ Cname)
18. i = 0 ∈ ℤ
19. (f x) = 1 ∈ ℕ2
20. (flip(f;a) x) = 1 ∈ ℕ2
21. v : cat-arrow(cat(G)) nerve_box_label(box;flip(f;a)) nerve_box_label(box;flip(flip(f;a);j))
22. nerve_box_edge(box;flip(flip(f;a);x);j) o nerve_box_edge(box;flip(flip(flip(f;a);x);j);x)
    = nerve_box_edge(box;flip(flip(f;a);x);x) o v
23. groupoid-square1(G;nerve_box_label(box;flip(flip(f;a);x));nerve_box_label(box;flip(flip(flip(f;a);x);j));
    nerve_box_label(box;flip(f;a));nerve_box_label(box;flip(flip(f;a);j));nerve_box_edge(box;flip(flip(f;a);x);j);
    nerve_box_edge(box;flip(flip(flip(f;a);x);j);x);nerve_box_edge(box;flip(flip(f;a);x);x))
= v
∈ {d:cat-arrow(cat(G)) nerve_box_label(box;flip(f;a)) nerve_box_label(box;flip(flip(f;a);j))| 
   nerve_box_edge(box;flip(flip(f;a);x);j) o nerve_box_edge(box;flip(flip(flip(f;a);x);j);x)
   = nerve_box_edge(box;flip(flip(f;a);x);x) o d} 
24. v1 : cat-arrow(cat(G)) nerve_box_label(box;f) nerve_box_label(box;flip(f;j))
25. nerve_box_edge(box;flip(f;x);j) o nerve_box_edge(box;flip(flip(f;x);j);x) = nerve_box_edge(box;flip(f;x);x) o v1
26. groupoid-square1(G;nerve_box_label(box;flip(f;x));nerve_box_label(box;flip(flip(f;x);j));nerve_box_label(box;f);
    nerve_box_label(box;flip(f;j));nerve_box_edge(box;flip(f;x);j);nerve_box_edge(box;flip(flip(f;x);j);x);
    nerve_box_edge(box;flip(f;x);x))
= v1
∈ {d:cat-arrow(cat(G)) nerve_box_label(box;f) nerve_box_label(box;flip(f;j))| 
   nerve_box_edge(box;flip(f;x);j) o nerve_box_edge(box;flip(flip(f;x);j);x) = nerve_box_edge(box;flip(f;x);x) o d} 
⊢ nerve_box_edge(box;f;a) o v = v1 o nerve_box_edge(box;flip(f;j);a)

2
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 : ℤ
9. box : open_box(cubical-nerve(cat(G));I;J;x;0)
10. f : name-morph(I;[])
11. f x ≠ 0
12. a : nameset(I)
13. flip(f;a) x ≠ 0
14. ¬(a = j ∈ Cname)
15. (f a) = 0 ∈ ℕ2
16. (f j) = 0 ∈ ℕ2
17. ¬(x = j ∈ Cname)
18. i = 0 ∈ ℤ
19. (f x) = 1 ∈ ℕ2
20. (flip(f;a) x) = 1 ∈ ℕ2
21. v : cat-arrow(cat(G)) nerve_box_label(box;flip(f;a)) nerve_box_label(box;flip(flip(f;a);j))
22. nerve_box_edge(box;flip(flip(f;a);x);j) o nerve_box_edge(box;flip(flip(flip(f;a);x);j);x)
    = nerve_box_edge(box;flip(flip(f;a);x);x) o v
23. groupoid-square1(G;nerve_box_label(box;flip(flip(f;a);x));nerve_box_label(box;flip(flip(flip(f;a);x);j));
    nerve_box_label(box;flip(f;a));nerve_box_label(box;flip(flip(f;a);j));nerve_box_edge(box;flip(flip(f;a);x);j);
    nerve_box_edge(box;flip(flip(flip(f;a);x);j);x);nerve_box_edge(box;flip(flip(f;a);x);x))
= v
∈ {d:cat-arrow(cat(G)) nerve_box_label(box;flip(f;a)) nerve_box_label(box;flip(flip(f;a);j))| 
   nerve_box_edge(box;flip(flip(f;a);x);j) o nerve_box_edge(box;flip(flip(flip(f;a);x);j);x)
   = nerve_box_edge(box;flip(flip(f;a);x);x) o d} 
24. v1 : cat-arrow(cat(G)) nerve_box_label(box;f) nerve_box_label(box;flip(f;j))
25. nerve_box_edge(box;flip(f;x);j) o nerve_box_edge(box;flip(flip(f;x);j);x) = nerve_box_edge(box;flip(f;x);x) o v1
26. groupoid-square1(G;nerve_box_label(box;flip(f;x));nerve_box_label(box;flip(flip(f;x);j));nerve_box_label(box;f);
    nerve_box_label(box;flip(f;j));nerve_box_edge(box;flip(f;x);j);nerve_box_edge(box;flip(flip(f;x);j);x);
    nerve_box_edge(box;flip(f;x);x))
= v1
∈ {d:cat-arrow(cat(G)) nerve_box_label(box;f) nerve_box_label(box;flip(f;j))| 
   nerve_box_edge(box;flip(f;x);j) o nerve_box_edge(box;flip(flip(f;x);j);x) = nerve_box_edge(box;flip(f;x);x) o d} 
27. nerve_box_edge(box;f;a) o v = v1 o nerve_box_edge(box;flip(f;j);a)
⊢ (cat-comp(cat(G)) nerve_box_label(box;f) nerve_box_label(box;flip(f;a)) nerve_box_label(box;flip(flip(f;a);j)) 
   nerve_box_edge(box;f;a) 
   v)
= (cat-comp(cat(G)) nerve_box_label(box;f) nerve_box_label(box;flip(f;j)) nerve_box_label(box;flip(flip(f;j);a)) v1 
   nerve_box_edge(box;flip(f;j);a))
∈ (cat-arrow(cat(G)) nerve_box_label(box;f) nerve_box_label(box;flip(flip(f;a);j)))

---

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  :  \mBbbZ{}
9.  box  :  open\_box(cubical-nerve(cat(G));I;J;x;0)
10.  f  :  name-morph(I;[])
11.  f  x  \mneq{}  0
12.  a  :  nameset(I)
13.  flip(f;a)  x  \mneq{}  0
14.  \mneg{}(a  =  j)
15.  (f  a)  =  0
16.  (f  j)  =  0
17.  \mneg{}(x  =  j)
18.  i  =  0
19.  (f  x)  =  1
20.  (flip(f;a)  x)  =  1
21.  v  :  \{d:cat-arrow(cat(G))  nerve\_box\_label(box;flip(f;a))  nerve\_box\_label(box;flip(flip(f;a);j))| 
                  nerve\_box\_edge(box;flip(flip(f;a);x);j)  o  nerve\_box\_edge(box;flip(flip(flip(f;a);x);j);x)
                  =  nerve\_box\_edge(box;flip(flip(f;a);x);x)  o  d\} 
22.  groupoid-square1(G;nerve\_box\_label(box;flip(flip(f;a);x));
        nerve\_box\_label(box;flip(flip(flip(f;a);x);j));nerve\_box\_label(box;flip(f;a));
        nerve\_box\_label(box;flip(flip(f;a);j));nerve\_box\_edge(box;flip(flip(f;a);x);j);
        nerve\_box\_edge(box;flip(flip(flip(f;a);x);j);x);nerve\_box\_edge(box;flip(flip(f;a);x);x))
=  v
23.  v1  :  \{d:cat-arrow(cat(G))  nerve\_box\_label(box;f)  nerve\_box\_label(box;flip(f;j))| 
                    nerve\_box\_edge(box;flip(f;x);j)  o  nerve\_box\_edge(box;flip(flip(f;x);j);x)
                    =  nerve\_box\_edge(box;flip(f;x);x)  o  d\} 
24.  groupoid-square1(G;nerve\_box\_label(box;flip(f;x));nerve\_box\_label(box;flip(flip(f;x);j));
        nerve\_box\_label(box;f);nerve\_box\_label(box;flip(f;j));nerve\_box\_edge(box;flip(f;x);j);
        nerve\_box\_edge(box;flip(flip(f;x);j);x);nerve\_box\_edge(box;flip(f;x);x))
=  v1
\mvdash{}  (cat-comp(cat(G))  nerve\_box\_label(box;f)  nerve\_box\_label(box;flip(f;a)) 
      nerve\_box\_label(box;flip(flip(f;a);j)) 
      nerve\_box\_edge(box;f;a) 
      v)
=  (cat-comp(cat(G))  nerve\_box\_label(box;f)  nerve\_box\_label(box;flip(f;j)) 
      nerve\_box\_label(box;flip(flip(f;j);a)) 
      v1 
      nerve\_box\_edge(box;flip(f;j);a))


By

---

Latex:
((D  -4  THEN  D  -2)  THEN  Assert  \mkleeneopen{}nerve\_box\_edge(box;f;a)  o  v  =  v1  o  nerve\_box\_edge(box;flip(f;j);a)\mkleeneclose{}\mcdot{})

---

Home Index