---

Step * 1 of Lemma same-face-square-commutes

.....assertion..... 
1. C : SmallCategory
2. I : Cname List
3. J : nameset(I) List
4. (∃j1∈J. (∃j2∈J. ¬(j1 = j2 ∈ Cname)))
5. x : nameset(I)
6. i : ℕ2
7. box : open_box(cubical-nerve(C);I;J;x;i)
8. f : name-morph(I;[])
9. g : name-morph(I;[])
10. h : name-morph(I;[])
11. k : name-morph(I;[])
12. a : nameset(I)
13. b : nameset(I)
14. ¬(a = b ∈ nameset(I))
15. (f a) = 0 ∈ ℕ2
16. (f b) = 0 ∈ ℕ2
17. g = flip(f;a) ∈ name-morph(I;[])
18. h = flip(f;b) ∈ name-morph(I;[])
19. k = flip(flip(f;a);b) ∈ name-morph(I;[])
20. ∃v:I-face(cubical-nerve(C);I)
     ((v ∈ box)
     ∧ (¬(dimension(v) = b ∈ Cname))
     ∧ (¬(dimension(v) = a ∈ Cname))
     ∧ (direction(v) = (f dimension(v)) ∈ ℕ2))
21. (cat-comp(C) 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(C) 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(C) nerve_box_label(box;f) nerve_box_label(box;flip(flip(f;a);b)))
22. ¬↑null(J)
⊢ ((cat-comp(C) nerve_box_label(box;f) nerve_box_label(box;g) nerve_box_label(box;k) nerve_box_edge(box;f;a) 
    nerve_box_edge(box;g;b))
= (cat-comp(C) nerve_box_label(box;f) nerve_box_label(box;h) nerve_box_label(box;k) nerve_box_edge(box;f;b) 
   nerve_box_edge(box;h;a))
∈ (cat-arrow(C) nerve_box_label(box;f) nerve_box_label(box;k)))
= ((cat-comp(C) 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(C) 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(C) nerve_box_label(box;f) nerve_box_label(box;flip(flip(f;a);b))))
∈ ℙ
BY
{ ((Assert g = flip(f;a) ∈ {c:name-morph(I;[])| (c b) = 0 ∈ ℕ2}  BY
          (Symmetry THEN EqTypeCD THEN Auto))
   THEN (Assert (flip(f;a) b) = 0 ∈ ℕ2 BY
               (RepUR ``name-morph-flip`` 0 THEN AutoSplit THEN D 14 THEN HypSubst' (-1) 0 THEN Auto))
   ) }

1
1. C : SmallCategory
2. I : Cname List
3. J : nameset(I) List
4. (∃j1∈J. (∃j2∈J. ¬(j1 = j2 ∈ Cname)))
5. x : nameset(I)
6. i : ℕ2
7. box : open_box(cubical-nerve(C);I;J;x;i)
8. f : name-morph(I;[])
9. g : name-morph(I;[])
10. h : name-morph(I;[])
11. k : name-morph(I;[])
12. a : nameset(I)
13. b : nameset(I)
14. ¬(a = b ∈ nameset(I))
15. (f a) = 0 ∈ ℕ2
16. (f b) = 0 ∈ ℕ2
17. g = flip(f;a) ∈ name-morph(I;[])
18. h = flip(f;b) ∈ name-morph(I;[])
19. k = flip(flip(f;a);b) ∈ name-morph(I;[])
20. ∃v:I-face(cubical-nerve(C);I)
     ((v ∈ box)
     ∧ (¬(dimension(v) = b ∈ Cname))
     ∧ (¬(dimension(v) = a ∈ Cname))
     ∧ (direction(v) = (f dimension(v)) ∈ ℕ2))
21. (cat-comp(C) 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(C) 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(C) nerve_box_label(box;f) nerve_box_label(box;flip(flip(f;a);b)))
22. ¬↑null(J)
23. g = flip(f;a) ∈ {c:name-morph(I;[])| (c b) = 0 ∈ ℕ2} 
24. (flip(f;a) b) = 0 ∈ ℕ2
⊢ ((cat-comp(C) nerve_box_label(box;f) nerve_box_label(box;g) nerve_box_label(box;k) nerve_box_edge(box;f;a) 
    nerve_box_edge(box;g;b))
= (cat-comp(C) nerve_box_label(box;f) nerve_box_label(box;h) nerve_box_label(box;k) nerve_box_edge(box;f;b) 
   nerve_box_edge(box;h;a))
∈ (cat-arrow(C) nerve_box_label(box;f) nerve_box_label(box;k)))
= ((cat-comp(C) 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(C) 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(C) nerve_box_label(box;f) nerve_box_label(box;flip(flip(f;a);b))))
∈ ℙ

---

Latex:

---

Latex:
.....assertion..... 
1.  C  :  SmallCategory
2.  I  :  Cname  List
3.  J  :  nameset(I)  List
4.  (\mexists{}j1\mmember{}J.  (\mexists{}j2\mmember{}J.  \mneg{}(j1  =  j2)))
5.  x  :  nameset(I)
6.  i  :  \mBbbN{}2
7.  box  :  open\_box(cubical-nerve(C);I;J;x;i)
8.  f  :  name-morph(I;[])
9.  g  :  name-morph(I;[])
10.  h  :  name-morph(I;[])
11.  k  :  name-morph(I;[])
12.  a  :  nameset(I)
13.  b  :  nameset(I)
14.  \mneg{}(a  =  b)
15.  (f  a)  =  0
16.  (f  b)  =  0
17.  g  =  flip(f;a)
18.  h  =  flip(f;b)
19.  k  =  flip(flip(f;a);b)
20.  \mexists{}v:I-face(cubical-nerve(C);I)
          ((v  \mmember{}  box)  \mwedge{}  (\mneg{}(dimension(v)  =  b))  \mwedge{}  (\mneg{}(dimension(v)  =  a))  \mwedge{}  (direction(v)  =  (f  dimension(v))))
21.  (cat-comp(C)  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(C)  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))
22.  \mneg{}\muparrow{}null(J)
\mvdash{}  ((cat-comp(C)  nerve\_box\_label(box;f)  nerve\_box\_label(box;g)  nerve\_box\_label(box;k) 
        nerve\_box\_edge(box;f;a) 
        nerve\_box\_edge(box;g;b))
=  (cat-comp(C)  nerve\_box\_label(box;f)  nerve\_box\_label(box;h)  nerve\_box\_label(box;k) 
      nerve\_box\_edge(box;f;b) 
      nerve\_box\_edge(box;h;a)))
=  ((cat-comp(C)  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(C)  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)))


By

---

Latex:
((Assert  g  =  flip(f;a)  BY
                (Symmetry  THEN  EqTypeCD  THEN  Auto))
  THEN  (Assert  (flip(f;a)  b)  =  0  BY
                          (RepUR  ``name-morph-flip``  0  THEN  AutoSplit  THEN  D  14  THEN  HypSubst'  (-1)  0  THEN  Auto))
  )

---

Home Index