---

Step * of Lemma nerve_box_edge1_wf

∀[G:Groupoid]. ∀[I:Cname List]. ∀[J:nameset(I) List]. ∀[j:nameset(J)]. ∀[x:nameset(I)]. ∀[i:ℕ2].
∀[box:open_box(cubical-nerve(cat(G));I;J;x;i)]. ∀[y:nameset(I)]. ∀[c:{c:name-morph(I;[])| (c y) = 0 ∈ ℕ2} ].
  nerve_box_edge1(G;box;x;i;j;c;y) ∈ cat-arrow(cat(G)) nerve_box_label(box;c) nerve_box_label(box;flip(c;y)) 
  supposing (∀j'∈J.j' = j ∈ Cname)
BY
{ (Auto
   THEN (Assert ¬↑null(J) BY
               (DVar `J' THEN Auto THEN DVar `j' THEN Auto THEN D 4 THEN D 5 THEN All Reduce THEN Auto))
   THEN DVar `c'
   THEN Unfold `nerve_box_edge1` 0
   THEN (BoolCase ⌜(c x =z i)⌝⋅ THENA Auto)) }

1
1. G : Groupoid
2. I : Cname List
3. J : nameset(I) List
4. j : nameset(J)
5. x : nameset(I)
6. i : ℕ2
7. box : open_box(cubical-nerve(cat(G));I;J;x;i)
8. y : nameset(I)
9. c : name-morph(I;[])
10. (c y) = 0 ∈ ℕ2
11. (∀j'∈J.j' = j ∈ Cname)
12. ¬↑null(J)
13. (c x) = i ∈ ℤ
⊢ nerve_box_edge(box;c;y) ∈ cat-arrow(cat(G)) nerve_box_label(box;c) nerve_box_label(box;flip(c;y))

2
1. G : Groupoid
2. I : Cname List
3. J : nameset(I) List
4. j : nameset(J)
5. x : nameset(I)
6. i : ℕ2
7. box : open_box(cubical-nerve(cat(G));I;J;x;i)
8. y : nameset(I)
9. c : name-morph(I;[])
10. c x ≠ i
11. (c y) = 0 ∈ ℕ2
12. (∀j'∈J.j' = j ∈ Cname)
13. ¬↑null(J)
⊢ if ¬beq-cname(y;j) then nerve_box_edge(box;c;y)
  if (i =z 0)
    then groupoid-square1(G;nerve_box_label(box;flip(c;x));nerve_box_label(box;flip(flip(c;x);y));
         nerve_box_label(box;c);nerve_box_label(box;flip(c;y));nerve_box_edge(box;flip(c;x);y);
         nerve_box_edge(box;flip(flip(c;x);y);x);nerve_box_edge(box;flip(c;x);x))
  else groupoid-square2(G;nerve_box_label(box;c);nerve_box_label(box;flip(c;y));
       nerve_box_label(box;flip(c;x));nerve_box_label(box;flip(flip(c;y);x));nerve_box_edge(box;flip(c;y);x);
       nerve_box_edge(box;c;x);nerve_box_edge(box;flip(c;x);y))
  fi  ∈ cat-arrow(cat(G)) nerve_box_label(box;c) nerve_box_label(box;flip(c;y))

---

Latex:

---

Latex:
\mforall{}[G:Groupoid].  \mforall{}[I:Cname  List].  \mforall{}[J:nameset(I)  List].  \mforall{}[j:nameset(J)].  \mforall{}[x:nameset(I)].  \mforall{}[i:\mBbbN{}2].
\mforall{}[box:open\_box(cubical-nerve(cat(G));I;J;x;i)].  \mforall{}[y:nameset(I)].
\mforall{}[c:\{c:name-morph(I;[])|  (c  y)  =  0\}  ].
    nerve\_box\_edge1(G;box;x;i;j;c;y)  \mmember{}  cat-arrow(cat(G))  nerve\_box\_label(box;c) 
                                                                          nerve\_box\_label(box;flip(c;y)) 
    supposing  (\mforall{}j'\mmember{}J.j'  =  j)


By

---

Latex:
(Auto
  THEN  (Assert  \mneg{}\muparrow{}null(J)  BY
                          (DVar  `J'
                            THEN  Auto
                            THEN  DVar  `j'
                            THEN  Auto
                            THEN  D  4
                            THEN  D  5
                            THEN  All  Reduce
                            THEN  Auto))
  THEN  DVar  `c'
  THEN  Unfold  `nerve\_box\_edge1`  0
  THEN  (BoolCase  \mkleeneopen{}(c  x  =\msubz{}  i)\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index