---

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


1. C : SmallCategory
2. I : Cname List
3. J : nameset(I) List
4. x : nameset(I)
5. i : ℕ2
6. box : open_box(cubical-nerve(C);I;J;x;i)
7. f : name-morph(I;[])
8. g : name-morph(I;[])
9. h : name-morph(I;[])
10. k : name-morph(I;[])
11. a : nameset(I)
12. b : nameset(I)
13. ∀[v:I-face(cubical-nerve(C);I)]
      ((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)))) supposing 
         ((v ∈ box) and 
         (¬(dimension(v) = b ∈ Cname)) and 
         (¬(dimension(v) = a ∈ Cname)) and 
         (¬(a = b ∈ nameset(I))) and 
         ((f b) = 0 ∈ ℕ2) and 
         (((f a) = 0 ∈ ℕ2) ∧ (direction(v) = (f dimension(v)) ∈ ℕ2))) 
    supposing ((∃j1∈J. ¬(j1 = a ∈ Cname)) ∧ (∃j2∈J. ¬(j2 = b ∈ Cname)))
    ∨ ((¬↑null(J)) ∧ ((f x) = i ∈ ℤ) ∧ ((flip(f;a) x) = i ∈ ℤ) ∧ ((flip(f;b) x) = i ∈ ℕ2))
14. ((∃j1∈J. ¬(j1 = a ∈ Cname)) ∧ (∃j2∈J. ¬(j2 = b ∈ Cname)))
∨ ((¬↑null(J)) ∧ ((f x) = i ∈ ℤ) ∧ ((flip(f;a) x) = i ∈ ℤ) ∧ ((flip(f;b) x) = i ∈ ℕ2))
15. ¬(a = b ∈ nameset(I))
16. (f a) = 0 ∈ ℕ2
17. (f b) = 0 ∈ ℕ2
18. g = flip(f;a) ∈ name-morph(I;[])
19. h = flip(f;b) ∈ name-morph(I;[])
20. k = flip(flip(f;a);b) ∈ name-morph(I;[])
21. v : I-face(cubical-nerve(C);I)
22. (v ∈ box)
23. ¬(dimension(v) = b ∈ Cname)
24. ¬(dimension(v) = a ∈ Cname)
25. direction(v) = (f dimension(v)) ∈ ℕ2
26. (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)))
⊢ (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))
BY
{ (Assert ¬↑null(J) BY
         (DVar `J' THEN (All Reduce THEN Auto) THEN SplitOrHyps THEN Auto THEN D 12 THEN All Reduce THEN Auto)) }

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

---

Latex:

---

Latex:

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


By

---

Latex:
(Assert  \mneg{}\muparrow{}null(J)  BY
              (DVar  `J'
                THEN  (All  Reduce  THEN  Auto)
                THEN  SplitOrHyps
                THEN  Auto
                THEN  D  12
                THEN  All  Reduce
                THEN  Auto))

---

Home Index