---

Step * 1 1 3 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. f x ≠ i
12. a : nameset(I)
13. ¬(x = j ∈ Cname)
14. (f x) = 0 ∈ ℕ2
15. (f j) = 0 ∈ ℕ2
16. (1 - f x) = i ∈ ℤ
17. x = a ∈ Cname
18. i = 1 ∈ ℕ2
19. flip(flip(f;x);x) = f ∈ name-morph(I;[])
⊢ (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) 
   nerve_box_edge(box;flip(f;x);j))
= (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)) 
   groupoid-square2(G;nerve_box_label(box;f);nerve_box_label(box;flip(f;j));
   nerve_box_label(box;flip(f;x));nerve_box_label(box;flip(flip(f;j);x));nerve_box_edge(box;flip(f;j);x);
   nerve_box_edge(box;f;x);nerve_box_edge(box;flip(f;x);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:((Assert (flip(f;j) x) = 0 ∈ ℕ2 BY
                 (RepUR ``name-morph-flip`` 0 THEN Auto))
          THEN (Assert (flip(f;x) j) = 0 ∈ ℕ2 BY
                      (RepUR ``name-morph-flip`` 0 THEN Auto))
          THEN ((Assert (flip(f;x) x) = i ∈ ℕ2 BY
                       (RepUR ``name-morph-flip`` 0 THEN Auto))
                THEN (Assert (∃j∈J. ¬(j = x ∈ Cname)) BY
                            ((BLemma `l_exists_iff` THENA Auto) THEN With ⌜j⌝ (D 0)⋅ THEN Auto))
                )
          THEN (Assert nerve_box_edge(box;f;x) ∈ cat-arrow(cat(G)) nerve_box_label(box;f) 
                                                 nerve_box_label(box;flip(f;x)) BY
                      (BLemma `nerve_box_edge_wf2` THEN Auto))
          THEN (Assert nerve_box_edge(box;flip(f;j);x) ∈ cat-arrow(cat(G)) nerve_box_label(box;flip(f;j)) 
                                                         nerve_box_label(box;flip(flip(f;j);x)) BY
                      (BLemma `nerve_box_edge_wf2` THEN Auto))
          THEN (Assert nerve_box_edge(box;flip(f;x);j) ∈ cat-arrow(cat(G)) nerve_box_label(box;flip(f;x)) 
                                                         nerve_box_label(box;flip(flip(f;j);x)) BY
                      (DoSubsume
                       THEN Try ((BLemma `nerve_box_edge_wf2` THEN Auto))
                       THEN BLemma `subtype_rel-equal`
                       THEN Auto))) }

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. f x ≠ i
12. a : nameset(I)
13. ¬(x = j ∈ Cname)
14. (f x) = 0 ∈ ℕ2
15. (f j) = 0 ∈ ℕ2
16. (1 - f x) = i ∈ ℤ
17. x = a ∈ Cname
18. i = 1 ∈ ℕ2
19. flip(flip(f;x);x) = f ∈ name-morph(I;[])
20. (flip(f;j) x) = 0 ∈ ℕ2
21. (flip(f;x) j) = 0 ∈ ℕ2
22. (flip(f;x) x) = i ∈ ℕ2
23. (∃j∈J. ¬(j = x ∈ Cname))
24. nerve_box_edge(box;f;x) ∈ cat-arrow(cat(G)) nerve_box_label(box;f) nerve_box_label(box;flip(f;x))
25. nerve_box_edge(box;flip(f;j);x) ∈ cat-arrow(cat(G)) nerve_box_label(box;flip(f;j)) 
                                      nerve_box_label(box;flip(flip(f;j);x))
26. nerve_box_edge(box;flip(f;x);j) ∈ cat-arrow(cat(G)) nerve_box_label(box;flip(f;x)) 
                                      nerve_box_label(box;flip(flip(f;j);x))
⊢ (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) 
   nerve_box_edge(box;flip(f;x);j))
= (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)) 
   groupoid-square2(G;nerve_box_label(box;f);nerve_box_label(box;flip(f;j));
   nerve_box_label(box;flip(f;x));nerve_box_label(box;flip(flip(f;j);x));nerve_box_edge(box;flip(f;j);x);
   nerve_box_edge(box;f;x);nerve_box_edge(box;flip(f;x);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.  f  x  \mneq{}  i
12.  a  :  nameset(I)
13.  \mneg{}(x  =  j)
14.  (f  x)  =  0
15.  (f  j)  =  0
16.  (1  -  f  x)  =  i
17.  x  =  a
18.  i  =  1
19.  flip(flip(f;x);x)  =  f
\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) 
      nerve\_box\_edge(box;flip(f;x);j))
=  (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)) 
      groupoid-square2(G;nerve\_box\_label(box;f);nerve\_box\_label(box;flip(f;j));
      nerve\_box\_label(box;flip(f;x));nerve\_box\_label(box;flip(flip(f;j);x));
      nerve\_box\_edge(box;flip(f;j);x);nerve\_box\_edge(box;f;x);nerve\_box\_edge(box;flip(f;x);j)) 
      nerve\_box\_edge(box;flip(f;j);x))


By

---

Latex:
TACTIC:((Assert  (flip(f;j)  x)  =  0  BY
                              (RepUR  ``name-morph-flip``  0  THEN  Auto))
                THEN  (Assert  (flip(f;x)  j)  =  0  BY
                                        (RepUR  ``name-morph-flip``  0  THEN  Auto))
                THEN  ((Assert  (flip(f;x)  x)  =  i  BY
                                          (RepUR  ``name-morph-flip``  0  THEN  Auto))
                            THEN  (Assert  (\mexists{}j\mmember{}J.  \mneg{}(j  =  x))  BY
                                                    ((BLemma  `l\_exists\_iff`  THENA  Auto)  THEN  With  \mkleeneopen{}j\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto))
                            )
                THEN  (Assert  nerve\_box\_edge(box;f;x)  \mmember{}  cat-arrow(cat(G))  nerve\_box\_label(box;f) 
                                                                                              nerve\_box\_label(box;flip(f;x))  BY
                                        (BLemma  `nerve\_box\_edge\_wf2`  THEN  Auto))
                THEN  (Assert  nerve\_box\_edge(box;flip(f;j);x)  \mmember{}  cat-arrow(cat(G)) 
                                                                                                              nerve\_box\_label(box;flip(f;j)) 
                                                                                                              nerve\_box\_label(box;flip(flip(f;j);x))  BY
                                        (BLemma  `nerve\_box\_edge\_wf2`  THEN  Auto))
                THEN  (Assert  nerve\_box\_edge(box;flip(f;x);j)  \mmember{}  cat-arrow(cat(G)) 
                                                                                                              nerve\_box\_label(box;flip(f;x)) 
                                                                                                              nerve\_box\_label(box;flip(flip(f;j);x))  BY
                                        (DoSubsume
                                          THEN  Try  ((BLemma  `nerve\_box\_edge\_wf2`  THEN  Auto))
                                          THEN  BLemma  `subtype\_rel-equal`
                                          THEN  Auto)))

---

Home Index