---

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


1. G : Groupoid
2. I : Cname List
3. x : nameset(I)
4. J : nameset(I) List
5. j : nameset(I)
6. (j ∈ J)
7. (∀j'∈J.j' = j ∈ Cname)
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. 1 - f x ≠ i
13. ¬(x = j ∈ Cname)
14. (f x) = 0 ∈ ℕ2
15. (f j) = 0 ∈ ℕ2
16. (f x) = i ∈ ℤ
17. x = a ∈ Cname
18. i = 0 ∈ ℕ2
19. flip(flip(f;x);x) = f ∈ name-morph(I;[])
20. (flip(flip(flip(f;x);x);j) x) = 0 ∈ ℕ2
21. (flip(flip(flip(f;x);x);j) x) = i ∈ ℕ2
22. v : {d:cat-arrow(cat(G)) nerve_box_label(box;flip(f;x)) nerve_box_label(box;flip(flip(f;x);j))| 
         nerve_box_edge(box;flip(flip(f;x);x);j) o nerve_box_edge(box;flip(flip(flip(f;x);x);j);x)
         = nerve_box_edge(box;flip(flip(f;x);x);x) o d} 
23. groupoid-square1(G;nerve_box_label(box;flip(flip(f;x);x));nerve_box_label(box;flip(flip(flip(f;x);x);j));
    nerve_box_label(box;flip(f;x));nerve_box_label(box;flip(flip(f;x);j));nerve_box_edge(box;flip(flip(f;x);x);j);
    nerve_box_edge(box;flip(flip(flip(f;x);x);j);x);nerve_box_edge(box;flip(flip(f;x);x);x))
= v
∈ {d:cat-arrow(cat(G)) nerve_box_label(box;flip(f;x)) nerve_box_label(box;flip(flip(f;x);j))| 
   nerve_box_edge(box;flip(flip(f;x);x);j) o nerve_box_edge(box;flip(flip(flip(f;x);x);j);x)
   = nerve_box_edge(box;flip(flip(f;x);x);x) o d} 
⊢ (cat-comp(cat(G)) nerve_box_label(box;f) nerve_box_label(box;flip(f;x)) nerve_box_label(box;flip(flip(f;x);j)) 
   nerve_box_edge(box;f;x) 
   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);x)) 
   nerve_box_edge(box;f;j) 
   nerve_box_edge(box;flip(f;j);x))
∈ (cat-arrow(cat(G)) nerve_box_label(box;f) nerve_box_label(box;flip(flip(f;x);j)))
BY
{ TACTIC:(D -2 THEN Unfold `cat-square-commutes` -2) }

1
1. G : Groupoid
2. I : Cname List
3. x : nameset(I)
4. J : nameset(I) List
5. j : nameset(I)
6. (j ∈ J)
7. (∀j'∈J.j' = j ∈ Cname)
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. 1 - f x ≠ i
13. ¬(x = j ∈ Cname)
14. (f x) = 0 ∈ ℕ2
15. (f j) = 0 ∈ ℕ2
16. (f x) = i ∈ ℤ
17. x = a ∈ Cname
18. i = 0 ∈ ℕ2
19. flip(flip(f;x);x) = f ∈ name-morph(I;[])
20. (flip(flip(flip(f;x);x);j) x) = 0 ∈ ℕ2
21. (flip(flip(flip(f;x);x);j) x) = i ∈ ℕ2
22. v : cat-arrow(cat(G)) nerve_box_label(box;flip(f;x)) nerve_box_label(box;flip(flip(f;x);j))
23. (cat-comp(cat(G)) nerve_box_label(box;flip(flip(f;x);x)) nerve_box_label(box;flip(flip(flip(f;x);x);j)) 
     nerve_box_label(box;flip(flip(f;x);j)) 
     nerve_box_edge(box;flip(flip(f;x);x);j) 
     nerve_box_edge(box;flip(flip(flip(f;x);x);j);x))
= (cat-comp(cat(G)) nerve_box_label(box;flip(flip(f;x);x)) nerve_box_label(box;flip(f;x)) 
   nerve_box_label(box;flip(flip(f;x);j)) 
   nerve_box_edge(box;flip(flip(f;x);x);x) 
   v)
∈ (cat-arrow(cat(G)) nerve_box_label(box;flip(flip(f;x);x)) nerve_box_label(box;flip(flip(f;x);j)))
24. groupoid-square1(G;nerve_box_label(box;flip(flip(f;x);x));nerve_box_label(box;flip(flip(flip(f;x);x);j));
    nerve_box_label(box;flip(f;x));nerve_box_label(box;flip(flip(f;x);j));nerve_box_edge(box;flip(flip(f;x);x);j);
    nerve_box_edge(box;flip(flip(flip(f;x);x);j);x);nerve_box_edge(box;flip(flip(f;x);x);x))
= v
∈ {d:cat-arrow(cat(G)) nerve_box_label(box;flip(f;x)) nerve_box_label(box;flip(flip(f;x);j))| 
   nerve_box_edge(box;flip(flip(f;x);x);j) o nerve_box_edge(box;flip(flip(flip(f;x);x);j);x)
   = nerve_box_edge(box;flip(flip(f;x);x);x) o d} 
⊢ (cat-comp(cat(G)) nerve_box_label(box;f) nerve_box_label(box;flip(f;x)) nerve_box_label(box;flip(flip(f;x);j)) 
   nerve_box_edge(box;f;x) 
   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);x)) 
   nerve_box_edge(box;f;j) 
   nerve_box_edge(box;flip(f;j);x))
∈ (cat-arrow(cat(G)) nerve_box_label(box;f) nerve_box_label(box;flip(flip(f;x);j)))

---

Latex:

---

Latex:

1.  G  :  Groupoid
2.  I  :  Cname  List
3.  x  :  nameset(I)
4.  J  :  nameset(I)  List
5.  j  :  nameset(I)
6.  (j  \mmember{}  J)
7.  (\mforall{}j'\mmember{}J.j'  =  j)
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.  1  -  f  x  \mneq{}  i
13.  \mneg{}(x  =  j)
14.  (f  x)  =  0
15.  (f  j)  =  0
16.  (f  x)  =  i
17.  x  =  a
18.  i  =  0
19.  flip(flip(f;x);x)  =  f
20.  (flip(flip(flip(f;x);x);j)  x)  =  0
21.  (flip(flip(flip(f;x);x);j)  x)  =  i
22.  v  :  \{d:cat-arrow(cat(G))  nerve\_box\_label(box;flip(f;x))  nerve\_box\_label(box;flip(flip(f;x);j))| 
                  nerve\_box\_edge(box;flip(flip(f;x);x);j)  o  nerve\_box\_edge(box;flip(flip(flip(f;x);x);j);x)
                  =  nerve\_box\_edge(box;flip(flip(f;x);x);x)  o  d\} 
23.  groupoid-square1(G;nerve\_box\_label(box;flip(flip(f;x);x));
        nerve\_box\_label(box;flip(flip(flip(f;x);x);j));nerve\_box\_label(box;flip(f;x));
        nerve\_box\_label(box;flip(flip(f;x);j));nerve\_box\_edge(box;flip(flip(f;x);x);j);
        nerve\_box\_edge(box;flip(flip(flip(f;x);x);j);x);nerve\_box\_edge(box;flip(flip(f;x);x);x))
=  v
\mvdash{}  (cat-comp(cat(G))  nerve\_box\_label(box;f)  nerve\_box\_label(box;flip(f;x)) 
      nerve\_box\_label(box;flip(flip(f;x);j)) 
      nerve\_box\_edge(box;f;x) 
      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);x)) 
      nerve\_box\_edge(box;f;j) 
      nerve\_box\_edge(box;flip(f;j);x))


By

---

Latex:
TACTIC:(D  -2  THEN  Unfold  `cat-square-commutes`  -2)

---

Home Index