---

Step * 1 1 1 1 2 1 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. ¬(x = j ∈ Cname)
13. (f x) = 0 ∈ ℕ2
14. (f j) = 0 ∈ ℕ2
15. (f x) = i ∈ ℤ
16. (flip(f;x) 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;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)) 
            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)))) supposing 
         ((v ∈ box) and 
         (¬(dimension(v) = j ∈ Cname)) and 
         (¬(dimension(v) = x ∈ Cname)) and 
         (¬(x = j ∈ nameset(I))) and 
         ((f j) = 0 ∈ ℕ2) and 
         (((f x) = 0 ∈ ℕ2) ∧ (direction(v) = (f dimension(v)) ∈ ℕ2)))
18. get_face(x;i;box) ∈ I-face(cubical-nerve(cat(G));I)
19. (get_face(x;i;box) ∈ box)
20. x1 : nameset(I)
21. v2 : ℕ2
22. v3 : cubical-nerve(cat(G))(I-[x1])
23. get_face(x;i;box) = <x1, v2, v3> ∈ I-face(cubical-nerve(cat(G));I)
24. x1 = x ∈ nameset(I)
25. v2 = i ∈ ℕ2
26. x = a ∈ Cname
⊢ False
BY
{ TACTIC:(RepUR ``name-morph-flip`` 16 THEN SplitOnHypITE 16  THEN Auto) }

---

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.  \mneg{}(x  =  j)
13.  (f  x)  =  0
14.  (f  j)  =  0
15.  (f  x)  =  i
16.  (flip(f;x)  x)  =  i
17.  \mforall{}[v:I-face(cubical-nerve(cat(G));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)) 
                        nerve\_box\_edge(box;f;j) 
                        nerve\_box\_edge(box;flip(f;j);x)))  supposing 
                  ((v  \mmember{}  box)  and 
                  (\mneg{}(dimension(v)  =  j))  and 
                  (\mneg{}(dimension(v)  =  x))  and 
                  (\mneg{}(x  =  j))  and 
                  ((f  j)  =  0)  and 
                  (((f  x)  =  0)  \mwedge{}  (direction(v)  =  (f  dimension(v)))))
18.  get\_face(x;i;box)  \mmember{}  I-face(cubical-nerve(cat(G));I)
19.  (get\_face(x;i;box)  \mmember{}  box)
20.  x1  :  nameset(I)
21.  v2  :  \mBbbN{}2
22.  v3  :  cubical-nerve(cat(G))(I-[x1])
23.  get\_face(x;i;box)  =  <x1,  v2,  v3>
24.  x1  =  x
25.  v2  =  i
26.  x  =  a
\mvdash{}  False


By

---

Latex:
TACTIC:(RepUR  ``name-morph-flip``  16  THEN  SplitOnHypITE  16    THEN  Auto)

---

Home Index