---

Step * of Lemma same-face-square-commutes

∀[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))) 
  supposing (∃j1∈J. (∃j2∈J. ¬(j1 = j2 ∈ Cname)))
BY
{ (InstLemma `same-face-edge-arrows-commute3` []
   THEN RepeatFor 3 (ParallelLast')
   THEN Intro
   THEN D -2
   THEN Try (Trivial)
   THEN RepeatFor 4 (ParallelLast')
   THEN RepeatFor 3 (Intro)
   THEN ParallelOp -4
   THEN Thin (-6)
   THEN RepeatFor 2 (ParallelLast')
   THEN Auto
   THEN (Assert ¬↑null(J) BY
               (DVar `J' THEN D 3 THEN All Reduce THEN Auto))
   THEN Unfold `cat-square-commutes` 0
   THEN NthHypEq (-2)
   THEN skip{(Repeat ((EqCD
                       THEN Try (Trivial)
                       THEN Try ((Fold `member` 0 THEN Auto))
                       THEN Try (((OrRight THENM Trivial) THEN Auto))))
              THEN Try ((DoSubsume THEN Try (BLemma `subtype_rel-equal`) THEN Auto))
              )}) }

1
.....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))))
∈ ℙ

---

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))))) 
    supposing  (\mexists{}j1\mmember{}J.  (\mexists{}j2\mmember{}J.  \mneg{}(j1  =  j2)))


By

---

Latex:
(InstLemma  `same-face-edge-arrows-commute3`  []
  THEN  RepeatFor  3  (ParallelLast')
  THEN  Intro
  THEN  D  -2
  THEN  Try  (Trivial)
  THEN  RepeatFor  4  (ParallelLast')
  THEN  RepeatFor  3  (Intro)
  THEN  ParallelOp  -4
  THEN  Thin  (-6)
  THEN  RepeatFor  2  (ParallelLast')
  THEN  Auto
  THEN  (Assert  \mneg{}\muparrow{}null(J)  BY
                          (DVar  `J'  THEN  D  3  THEN  All  Reduce  THEN  Auto))
  THEN  Unfold  `cat-square-commutes`  0
  THEN  NthHypEq  (-2)
  THEN  skip\{(Repeat  ((EqCD
                                          THEN  Try  (Trivial)
                                          THEN  Try  ((Fold  `member`  0  THEN  Auto))
                                          THEN  Try  (((OrRight  THENM  Trivial)  THEN  Auto))))
                        THEN  Try  ((DoSubsume  THEN  Try  (BLemma  `subtype\_rel-equal`)  THEN  Auto))
                        )\})

---

Home Index