---

Step * 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. (f j) = 0 ∈ ℕ2
15. (f x) = i ∈ ℤ
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)) 
   nerve_box_edge(box;f;j) 
   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:(InstLemma `same-face-edge-arrows-commute0`
           [⌜cat(G)⌝;⌜I⌝;⌜J⌝;⌜x⌝;⌜i⌝;⌜box⌝;⌜f⌝;⌜a⌝;⌜j⌝]⋅
          THENA ((Auto
                  THEN OrRight
                  THEN Auto
                  THEN DVar `box'
                  THEN RepUR ``name-morph-flip`` 0
                  THEN AutoSplit
                  THEN Eliminate ⌜x⌝⋅
                  THEN Auto
                  THEN D 11
                  THEN Auto)
                 THEN skip{(Try ((BLemma `l_exists_iff` THEN Auto))
                            THEN (InstLemma `get_face-wf` [⌜cubical-nerve(cat(G))⌝;⌜I⌝;⌜J⌝;⌜x⌝;⌜i⌝;⌜box⌝] ⋅ THENA Auto)
                            THEN (MemTypeHD (-1) THENA Auto))}
                 )
          ) }

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. (f j) = 0 ∈ ℕ2
15. (f x) = i ∈ ℤ
16. (flip(f;a) x) = i ∈ ℤ
17. ∀[v:I-face(cubical-nerve(cat(G));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)) 
            nerve_box_edge(box;f;j) 
            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)))) supposing 
         ((v ∈ box) and 
         (¬(dimension(v) = j ∈ Cname)) and 
         (¬(dimension(v) = a ∈ Cname)) and 
         (¬(a = j ∈ nameset(I))) and 
         ((f j) = 0 ∈ ℕ2) and 
         (((f a) = 0 ∈ ℕ2) ∧ (direction(v) = (f dimension(v)) ∈ ℕ2)))
⊢ (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)) 
   nerve_box_edge(box;f;j) 
   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  :  \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.  (f  j)  =  0
15.  (f  x)  =  i
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)) 
      nerve\_box\_edge(box;f;j) 
      nerve\_box\_edge(box;flip(f;j);a))


By

---

Latex:
TACTIC:(InstLemma  `same-face-edge-arrows-commute0`
                  [\mkleeneopen{}cat(G)\mkleeneclose{};\mkleeneopen{}I\mkleeneclose{};\mkleeneopen{}J\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}i\mkleeneclose{};\mkleeneopen{}box\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}j\mkleeneclose{}]\mcdot{}
                THENA  ((Auto
                                THEN  OrRight
                                THEN  Auto
                                THEN  DVar  `box'
                                THEN  RepUR  ``name-morph-flip``  0
                                THEN  AutoSplit
                                THEN  Eliminate  \mkleeneopen{}x\mkleeneclose{}\mcdot{}
                                THEN  Auto
                                THEN  D  11
                                THEN  Auto)
                              THEN  skip\{(Try  ((BLemma  `l\_exists\_iff`  THEN  Auto))
                                                    THEN  (InstLemma  `get\_face-wf`  [\mkleeneopen{}cubical-nerve(cat(G))\mkleeneclose{};\mkleeneopen{}I\mkleeneclose{};\mkleeneopen{}J\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}i\mkleeneclose{};
                                                                \mkleeneopen{}box\mkleeneclose{}]
                                                                \mcdot{}
                                                                THENA  Auto
                                                                )
                                                    THEN  (MemTypeHD  (-1)  THENA  Auto))\}
                              )
                )

---

Home Index