---

Step * 2 1 1 1 of Lemma nerve_box_edge1_wf


1. G : Groupoid
2. I : Cname List
3. J : nameset(I) List
4. j : nameset(J)
5. x : nameset(I)
6. i : ℤ
7. box : open_box(cubical-nerve(cat(G));I;J;x;0)
8. y : nameset(I)
9. c : name-morph(I;[])
10. c x ≠ 0
11. (c y) = 0 ∈ ℕ2
12. (∀j'∈J.j' = j ∈ Cname)
13. ¬↑null(J)
14. y = j ∈ Cname
15. ¬(x = y ∈ Cname)
16. i = 0 ∈ ℤ
17. (c x) = 1 ∈ ℕ2
18. (flip(c;x) x) = 0 ∈ ℕ2
19. (flip(c;x) y) = 0 ∈ ℕ2
20. (flip(flip(c;x);y) x) = 0 ∈ ℕ2
21. flip(flip(flip(c;x);y);x) = flip(c;y) ∈ name-morph(I;[])
⊢ 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)) ∈ cat-arrow(cat(G)) nerve_box_label(box;c) nerve_box_label(box;flip(c;y))
BY
{ (RepeatFor 2 ((DoSubsume THEN Auto)) THEN BLemma `subtype_rel-equal` THEN Auto) }

---

Latex:

---

Latex:

1.  G  :  Groupoid
2.  I  :  Cname  List
3.  J  :  nameset(I)  List
4.  j  :  nameset(J)
5.  x  :  nameset(I)
6.  i  :  \mBbbZ{}
7.  box  :  open\_box(cubical-nerve(cat(G));I;J;x;0)
8.  y  :  nameset(I)
9.  c  :  name-morph(I;[])
10.  c  x  \mneq{}  0
11.  (c  y)  =  0
12.  (\mforall{}j'\mmember{}J.j'  =  j)
13.  \mneg{}\muparrow{}null(J)
14.  y  =  j
15.  \mneg{}(x  =  y)
16.  i  =  0
17.  (c  x)  =  1
18.  (flip(c;x)  x)  =  0
19.  (flip(c;x)  y)  =  0
20.  (flip(flip(c;x);y)  x)  =  0
21.  flip(flip(flip(c;x);y);x)  =  flip(c;y)
\mvdash{}  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))
    \mmember{}  cat-arrow(cat(G))  nerve\_box\_label(box;c)  nerve\_box\_label(box;flip(c;y))


By

---

Latex:
(RepeatFor  2  ((DoSubsume  THEN  Auto))  THEN  BLemma  `subtype\_rel-equal`  THEN  Auto)

---

Home Index