---

Step * 1 1 3 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. f x ≠ i
12. a : nameset(I)
13. ¬(a = j ∈ Cname)
14. (f a) = 0 ∈ ℕ2
15. (f j) = 0 ∈ ℕ2
16. (flip(f;a) x) = i ∈ ℤ
⊢ (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) 
   nerve_box_edge(box;flip(f;a);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);a)) 
   if (i =z 0)
   then 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))
   else 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))
   fi  
   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
{ TACTIC:(RepUR ``name-morph-flip`` -1
          THEN SplitOnHypITE -1 
          THEN Auto
          THEN Eliminate ⌜a⌝⋅
          THEN (Assert i = 1 ∈ ℕ2 BY
                      Auto)
          THEN HypSubst' (-1) 0
          THEN Reduce 0
          THEN (Assert flip(flip(f;x);x) = f ∈ name-morph(I;[]) BY
                      (BLemma `name-morph-ext` 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;[])
⊢ (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.  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.  f  x  \mneq{}  i
12.  a  :  nameset(I)
13.  \mneg{}(a  =  j)
14.  (f  a)  =  0
15.  (f  j)  =  0
16.  (flip(f;a)  x)  =  i
\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) 
      nerve\_box\_edge(box;flip(f;a);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);a)) 
      if  (i  =\msubz{}  0)
      then  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))
      else  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))
      fi   
      nerve\_box\_edge(box;flip(f;j);a))


By

---

Latex:
TACTIC:(RepUR  ``name-morph-flip``  -1
                THEN  SplitOnHypITE  -1 
                THEN  Auto
                THEN  Eliminate  \mkleeneopen{}a\mkleeneclose{}\mcdot{}
                THEN  (Assert  i  =  1  BY
                                        Auto)
                THEN  HypSubst'  (-1)  0
                THEN  Reduce  0
                THEN  (Assert  flip(flip(f;x);x)  =  f  BY
                                        (BLemma  `name-morph-ext`  THEN  Auto)))

---

Home Index