---

Step * of Lemma same-face-edge-arrows-commute0

∀[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:name-morph(I;[]). ∀a,b:nameset(I).
    ∀[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))
BY
{ ((Auto THEN (Assert ¬↑null(J) BY (D 10 THEN Auto THEN DVar `J' THEN D 10 THEN All Reduce THEN Auto)))
   THEN (Assert ((ob(cube(v)) flip(flip(f;a);b)) = nerve_box_label(box;flip(flip(f;a);b)) ∈ cat-ob(C))
               ∧ ((ob(cube(v)) f) = nerve_box_label(box;f) ∈ cat-ob(C))
               ∧ ((ob(cube(v)) flip(f;a)) = nerve_box_label(box;flip(f;a)) ∈ cat-ob(C))
               ∧ ((ob(cube(v)) flip(f;b)) = nerve_box_label(box;flip(f;b)) ∈ cat-ob(C))
               ∧ ((ob(cube(v)) flip(flip(f;b);a)) = nerve_box_label(box;flip(flip(f;b);a)) ∈ cat-ob(C)) BY
               (SplitAndConcl
                THEN Try ((BLemma `nerve_box_label_same`
                           THEN Auto
                           THEN RepUR ``name-morph-flip`` 0
                           THEN RepeatFor 2 (AutoSplit)))
                ))
   ) }

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. a : nameset(I)
9. b : nameset(I)
10. ((∃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))
11. v : I-face(cubical-nerve(C);I)
12. (f a) = 0 ∈ ℕ2
13. direction(v) = (f dimension(v)) ∈ ℕ2
14. (f b) = 0 ∈ ℕ2
15. ¬(a = b ∈ nameset(I))
16. ¬(dimension(v) = a ∈ Cname)
17. ¬(dimension(v) = b ∈ Cname)
18. (v ∈ box)
19. ¬↑null(J)
20. ((ob(cube(v)) flip(flip(f;a);b)) = nerve_box_label(box;flip(flip(f;a);b)) ∈ cat-ob(C))
∧ ((ob(cube(v)) f) = nerve_box_label(box;f) ∈ cat-ob(C))
∧ ((ob(cube(v)) flip(f;a)) = nerve_box_label(box;flip(f;a)) ∈ cat-ob(C))
∧ ((ob(cube(v)) flip(f;b)) = nerve_box_label(box;flip(f;b)) ∈ cat-ob(C))
∧ ((ob(cube(v)) flip(flip(f;b);a)) = nerve_box_label(box;flip(flip(f;b);a)) ∈ cat-ob(C))
⊢ (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:
\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:name-morph(I;[]).  \mforall{}a,b:nameset(I).
        \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))


By

---

Latex:
((Auto
    THEN  (Assert  \mneg{}\muparrow{}null(J)  BY
                            (D  10  THEN  Auto  THEN  DVar  `J'  THEN  D  10  THEN  All  Reduce  THEN  Auto))
    )
  THEN  (Assert  ((ob(cube(v))  flip(flip(f;a);b))  =  nerve\_box\_label(box;flip(flip(f;a);b)))
                          \mwedge{}  ((ob(cube(v))  f)  =  nerve\_box\_label(box;f))
                          \mwedge{}  ((ob(cube(v))  flip(f;a))  =  nerve\_box\_label(box;flip(f;a)))
                          \mwedge{}  ((ob(cube(v))  flip(f;b))  =  nerve\_box\_label(box;flip(f;b)))
                          \mwedge{}  ((ob(cube(v))  flip(flip(f;b);a))  =  nerve\_box\_label(box;flip(flip(f;b);a)))  BY
                          (SplitAndConcl
                            THEN  Try  ((BLemma  `nerve\_box\_label\_same`
                                                  THEN  Auto
                                                  THEN  RepUR  ``name-morph-flip``  0
                                                  THEN  RepeatFor  2  (AutoSplit)))
                            ))
  )

---

Home Index