---

Step * of Lemma groupoid-edges-commute1

No Annotations
∀G:Groupoid. ∀I:Cname List. ∀J:nameset(I) List. ∀j:nameset(I).
  ((j ∈ J)
  ⇒ (∀j'∈J.j' = j ∈ Cname)
  ⇒ (∀x:nameset(I). ∀i:ℕ2. ∀box:open_box(cubical-nerve(fst(G));I;J;x;i).
        edge-arrows-commute(fst(G);I;λc.nerve_box_label(box;c);λy,c. nerve_box_edge1(G;box;x;i;j;c;y))))
BY
{ (Auto
   THEN D 0
   THEN Reduce 0
   THEN Auto
   THEN RenameVar `f' (-4)
   THEN RenameVar `a' (-3)
   THEN RenameVar `b' (-2)
   THEN D -3
   THEN D -2) }

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(fst(G));I;J;x;i)
10. f : name-morph(I;[])
11. a : nameset(I)
12. (f a) = 0 ∈ ℕ2
13. b : nameset(I)
14. (f b) = 0 ∈ ℕ2
15. ¬(a = b ∈ nameset(I))
⊢ (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_edge1(G;box;x;i;j;f;a) 
   nerve_box_edge1(G;box;x;i;j;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_edge1(G;box;x;i;j;f;b) 
   nerve_box_edge1(G;box;x;i;j;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{}j:nameset(I).
    ((j  \mmember{}  J)
    {}\mRightarrow{}  (\mforall{}j'\mmember{}J.j'  =  j)
    {}\mRightarrow{}  (\mforall{}x:nameset(I).  \mforall{}i:\mBbbN{}2.  \mforall{}box:open\_box(cubical-nerve(fst(G));I;J;x;i).
                edge-arrows-commute(fst(G);I;\mlambda{}c.nerve\_box\_label(box;c);\mlambda{}y,c.  ...)))


By

---

Latex:
(Auto
  THEN  D  0
  THEN  Reduce  0
  THEN  Auto
  THEN  RenameVar  `f'  (-4)
  THEN  RenameVar  `a'  (-3)
  THEN  RenameVar  `b'  (-2)
  THEN  D  -3
  THEN  D  -2)

---

Home Index