---

Step * of Lemma same-face-square-commutes2

∀[C:SmallCategory]. ∀[I:Cname List]. ∀[J:nameset(I) List]. ∀[x:nameset(I)]. ∀[i:ℕ2].
∀[box:open_box(cubical-nerve(C);I;J;x;i)]. ∀[f,g,h,k:name-morph(I;[])].
  ∀a,b:nameset(I).
    (nerve_box_edge(box;f;a) o nerve_box_edge(box;g;b) = nerve_box_edge(box;f;b) o nerve_box_edge(box;h;a)) supposing 
       (((((¬(a = b ∈ nameset(I))) ∧ ((f a) = 0 ∈ ℕ2))
       ∧ ((f b) = 0 ∈ ℕ2)
       ∧ (g = flip(f;a) ∈ name-morph(I;[]))
       ∧ (h = flip(f;b) ∈ name-morph(I;[]))
       ∧ (k = flip(flip(f;a);b) ∈ name-morph(I;[])))
       ∧ (∃v:I-face(cubical-nerve(C);I)
           ((v ∈ box)
           ∧ (¬(dimension(v) = b ∈ Cname))
           ∧ (¬(dimension(v) = a ∈ Cname))
           ∧ (direction(v) = (f dimension(v)) ∈ ℕ2)))) and 
       (((∃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))))
BY
{ (InstLemma `same-face-edge-arrows-commute0` []
   THEN RepeatFor 7 (ParallelLast')
   THEN RepeatFor 3 (Intro)
   THEN ParallelOp -4
   THEN Thin (-6)
   THEN ParallelLast'
   THEN Intros
   THEN Unfold `cat-square-commutes` 0
   THEN SplitAndHyps
   THEN ExRepD
   THEN OnMaybeHyp 13 (\h. (InstHyp [⌜v⌝] h⋅ THENA 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)))
⊢ (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:
\mforall{}[C:SmallCategory].  \mforall{}[I:Cname  List].  \mforall{}[J:nameset(I)  List].  \mforall{}[x:nameset(I)].  \mforall{}[i:\mBbbN{}2].
\mforall{}[box:open\_box(cubical-nerve(C);I;J;x;i)].  \mforall{}[f,g,h,k:name-morph(I;[])].
    \mforall{}a,b:nameset(I).
        (nerve\_box\_edge(box;f;a)  o  nerve\_box\_edge(box;g;b)
          =  nerve\_box\_edge(box;f;b)  o  nerve\_box\_edge(box;h;a))  supposing 
              (((((\mneg{}(a  =  b))  \mwedge{}  ((f  a)  =  0))
              \mwedge{}  ((f  b)  =  0)
              \mwedge{}  (g  =  flip(f;a))
              \mwedge{}  (h  =  flip(f;b))
              \mwedge{}  (k  =  flip(flip(f;a);b)))
              \mwedge{}  (\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))))))  and 
              (((\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))))


By

---

Latex:
(InstLemma  `same-face-edge-arrows-commute0`  []
  THEN  RepeatFor  7  (ParallelLast')
  THEN  RepeatFor  3  (Intro)
  THEN  ParallelOp  -4
  THEN  Thin  (-6)
  THEN  ParallelLast'
  THEN  Intros
  THEN  Unfold  `cat-square-commutes`  0
  THEN  SplitAndHyps
  THEN  ExRepD
  THEN  OnMaybeHyp  13  (\mbackslash{}h.  (InstHyp  [\mkleeneopen{}v\mkleeneclose{}]  h\mcdot{}  THENA  Auto)))

---

Home Index