---

Step * of Lemma groupoid-edges-commute

No Annotations
∀G:Groupoid. ∀I:Cname List. ∀J:nameset(I) List. ∀x:nameset(I). ∀i:ℕ2. ∀box:open_box(cubical-nerve(fst(G));I;J;x;i).
  ((∃j1∈J. (∃j2∈J. ¬(j1 = j2 ∈ Cname)))
  ⇒ edge-arrows-commute(fst(G);I;λc.nerve_box_label(box;c);λy,c. nerve_box_edge(box;c;y)))
BY
{ (Intros
   THEN (D 0 THENW Auto)
   THEN RenameVar `f' (-1)
   THEN (D 0 THENA Auto)
   THEN RenameVar `a' (-1)
   THEN D -1
   THEN (D 0 THENA Auto)
   THEN RenameVar `b' (-1)
   THEN D -1
   THEN (D 0 THENA Auto)
   THEN Reduce 0
   THEN (Decide ⌜(∃v∈box. (¬(dimension(v) = b ∈ Cname))
                 ∧ (¬(dimension(v) = a ∈ Cname))
                 ∧ (direction(v) = (f dimension(v)) ∈ ℕ2))⌝⋅
         THENA Auto
         )) }

1
1. G : Groupoid
2. I : Cname List
3. J : nameset(I) List
4. x : nameset(I)
5. i : ℕ2
6. box : open_box(cubical-nerve(fst(G));I;J;x;i)
7. (∃j1∈J. (∃j2∈J. ¬(j1 = j2 ∈ Cname)))
8. f : name-morph(I;[])
9. a : nameset(I)
10. (f a) = 0 ∈ ℕ2
11. b : nameset(I)
12. (f b) = 0 ∈ ℕ2
13. ¬(a = b ∈ nameset(I))
14. (∃v∈box. (¬(dimension(v) = b ∈ Cname)) ∧ (¬(dimension(v) = a ∈ Cname)) ∧ (direction(v) = (f dimension(v)) ∈ ℕ2))
⊢ (cat-comp(fst(G)) nerve_box_label(box;f) nerve_box_label(box;flip(f;a)) nerve_box_label(box;flip(flip(f;a);b)) 
   nerve_box_edge(box;f;a) 
   nerve_box_edge(box;flip(f;a);b))
= (cat-comp(fst(G)) nerve_box_label(box;f) nerve_box_label(box;flip(f;b)) nerve_box_label(box;flip(flip(f;b);a)) 
   nerve_box_edge(box;f;b) 
   nerve_box_edge(box;flip(f;b);a))
∈ (cat-arrow(fst(G)) nerve_box_label(box;f) nerve_box_label(box;flip(flip(f;a);b)))

2
1. G : Groupoid
2. I : Cname List
3. J : nameset(I) List
4. x : nameset(I)
5. i : ℕ2
6. box : open_box(cubical-nerve(fst(G));I;J;x;i)
7. (∃j1∈J. (∃j2∈J. ¬(j1 = j2 ∈ Cname)))
8. f : name-morph(I;[])
9. a : nameset(I)
10. (f a) = 0 ∈ ℕ2
11. b : nameset(I)
12. (f b) = 0 ∈ ℕ2
13. ¬(a = b ∈ nameset(I))
14. ¬(∃v∈box. (¬(dimension(v) = b ∈ Cname)) ∧ (¬(dimension(v) = a ∈ Cname)) ∧ (direction(v) = (f dimension(v)) ∈ ℕ2))
⊢ (cat-comp(fst(G)) nerve_box_label(box;f) nerve_box_label(box;flip(f;a)) nerve_box_label(box;flip(flip(f;a);b)) 
   nerve_box_edge(box;f;a) 
   nerve_box_edge(box;flip(f;a);b))
= (cat-comp(fst(G)) nerve_box_label(box;f) nerve_box_label(box;flip(f;b)) nerve_box_label(box;flip(flip(f;b);a)) 
   nerve_box_edge(box;f;b) 
   nerve_box_edge(box;flip(f;b);a))
∈ (cat-arrow(fst(G)) nerve_box_label(box;f) nerve_box_label(box;flip(flip(f;a);b)))

---

Latex:

---

Latex:
No  Annotations
\mforall{}G:Groupoid.  \mforall{}I:Cname  List.  \mforall{}J:nameset(I)  List.  \mforall{}x:nameset(I).  \mforall{}i:\mBbbN{}2.
\mforall{}box:open\_box(cubical-nerve(fst(G));I;J;x;i).
    ((\mexists{}j1\mmember{}J.  (\mexists{}j2\mmember{}J.  \mneg{}(j1  =  j2)))
    {}\mRightarrow{}  edge-arrows-commute(fst(G);I;\mlambda{}c.nerve\_box\_label(box;c);\mlambda{}y,c.  nerve\_box\_edge(box;c;y)))


By

---

Latex:
(Intros
  THEN  (D  0  THENW  Auto)
  THEN  RenameVar  `f'  (-1)
  THEN  (D  0  THENA  Auto)
  THEN  RenameVar  `a'  (-1)
  THEN  D  -1
  THEN  (D  0  THENA  Auto)
  THEN  RenameVar  `b'  (-1)
  THEN  D  -1
  THEN  (D  0  THENA  Auto)
  THEN  Reduce  0
  THEN  (Decide  \mkleeneopen{}(\mexists{}v\mmember{}box.  (\mneg{}(dimension(v)  =  b))
                              \mwedge{}  (\mneg{}(dimension(v)  =  a))
                              \mwedge{}  (direction(v)  =  (f  dimension(v))))\mkleeneclose{}\mcdot{}
              THENA  Auto
              ))

---

Home Index