---

Step * of Lemma nerve_box_edge_same1

No Annotations
∀[C:SmallCategory]. ∀[I:Cname List]. ∀[J:nameset(I) List]. ∀[x:nameset(I)]. ∀[i:ℕ2].
∀[box:open_box(cubical-nerve(C);I;J;x;i)]. ∀[y:nameset(I)]. ∀[c:{c:name-morph(I;[])| (c y) = 0 ∈ ℕ2} ].
  ∀f:I-face(cubical-nerve(C);I)
    (cube(f) c flip(c;y) (λx.Ax))
    = nerve_box_edge(box;c;y)
    ∈ (cat-arrow(C) nerve_box_label(box;c) nerve_box_label(box;flip(c;y))) 
    supposing (f ∈ box) ∧ (direction(f) = (c dimension(f)) ∈ ℕ2) ∧ (direction(f) = (flip(c;y) dimension(f)) ∈ ℕ2) 
  supposing (∃j∈J. ¬(j = y ∈ Cname)) ∨ (((c x) = i ∈ ℕ2) ∧ (¬↑null(J)))
BY
{ (InstLemma `nerve_box_label_same` []
   THEN RepeatFor 6 (ParallelLast')
   THEN Auto
   THEN Unfold `nerve_box_edge` 0
   THEN (GenConclTerm ⌜nerve-box-common-face(box;c;y)⌝⋅ THENA (Try (BLemma `nerve-box-common-face_wf2`) THEN Auto))
   THEN D -2
   THEN (Assert ¬↑null(J) BY
               (SplitOrHyps THEN Auto THEN (DVar `J' THEN D 9) THEN All Reduce THEN Auto))
   THEN (Assert (cube(v) c) = nerve_box_label(box;c) ∈ cat-ob(C) BY
               (BackThruSomeHyp THEN Auto))
   THEN (Assert (cube(v) flip(c;y)) = nerve_box_label(box;flip(c;y)) ∈ cat-ob(C) BY
               (BackThruSomeHyp THEN Auto))
   THEN SubsumeC ⌜cat-arrow(C) (cube(v) c) (cube(v) flip(c;y))⌝⋅
   THEN Try ((BLemma `subtype_rel-equal`  THEN Auto))
   THEN RenameTo `g' `v') }

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. ∀[L:name-morph(I;[])]
     ∀f:I-face(cubical-nerve(C);I)
       ((cube(f) L) = nerve_box_label(box;L) ∈ cat-ob(C)) supposing 
          ((f ∈ box) and 
          (direction(f) = (L dimension(f)) ∈ ℕ2)) 
     supposing ((L x) = i ∈ ℕ2) ∨ (¬↑null(J))
8. y : nameset(I)
9. c : {c:name-morph(I;[])| (c y) = 0 ∈ ℕ2} 
10. (∃j∈J. ¬(j = y ∈ Cname)) ∨ (((c x) = i ∈ ℕ2) ∧ (¬↑null(J)))
11. f : I-face(cubical-nerve(C);I)
12. (f ∈ box)
13. direction(f) = (c dimension(f)) ∈ ℕ2
14. direction(f) = (flip(c;y) dimension(f)) ∈ ℕ2
15. g : I-face(cubical-nerve(C);I)
16. (g ∈ box) ∧ (direction(g) = (c dimension(g)) ∈ ℕ2) ∧ (direction(g) = (flip(c;y) dimension(g)) ∈ ℕ2)
17. nerve-box-common-face(box;c;y)
= g
∈ {f:I-face(cubical-nerve(C);I)| 
   (f ∈ box) ∧ (direction(f) = (c dimension(f)) ∈ ℕ2) ∧ (direction(f) = (flip(c;y) dimension(f)) ∈ ℕ2)} 
18. ¬↑null(J)
19. (cube(g) c) = nerve_box_label(box;c) ∈ cat-ob(C)
20. (cube(g) flip(c;y)) = nerve_box_label(box;flip(c;y)) ∈ cat-ob(C)
⊢ (cube(f) c flip(c;y) (λx.Ax)) = (cube(g) c flip(c;y) (λx.Ax)) ∈ (cat-arrow(C) (cube(g) c) (cube(g) flip(c;y)))

---

Latex:

---

Latex:
No  Annotations
\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{}[y:nameset(I)].  \mforall{}[c:\{c:name-morph(I;[])|  (c  y)  =  0\}  ].
    \mforall{}f:I-face(cubical-nerve(C);I)
        (cube(f)  c  flip(c;y)  (\mlambda{}x.Ax))  =  nerve\_box\_edge(box;c;y) 
        supposing  (f  \mmember{}  box)
        \mwedge{}  (direction(f)  =  (c  dimension(f)))
        \mwedge{}  (direction(f)  =  (flip(c;y)  dimension(f))) 
    supposing  (\mexists{}j\mmember{}J.  \mneg{}(j  =  y))  \mvee{}  (((c  x)  =  i)  \mwedge{}  (\mneg{}\muparrow{}null(J)))


By

---

Latex:
(InstLemma  `nerve\_box\_label\_same`  []
  THEN  RepeatFor  6  (ParallelLast')
  THEN  Auto
  THEN  Unfold  `nerve\_box\_edge`  0
  THEN  (GenConclTerm  \mkleeneopen{}nerve-box-common-face(box;c;y)\mkleeneclose{}\mcdot{}
              THENA  (Try  (BLemma  `nerve-box-common-face\_wf2`)  THEN  Auto)
              )
  THEN  D  -2
  THEN  (Assert  \mneg{}\muparrow{}null(J)  BY
                          (SplitOrHyps  THEN  Auto  THEN  (DVar  `J'  THEN  D  9)  THEN  All  Reduce  THEN  Auto))
  THEN  (Assert  (cube(v)  c)  =  nerve\_box\_label(box;c)  BY
                          (BackThruSomeHyp  THEN  Auto))
  THEN  (Assert  (cube(v)  flip(c;y))  =  nerve\_box\_label(box;flip(c;y))  BY
                          (BackThruSomeHyp  THEN  Auto))
  THEN  SubsumeC  \mkleeneopen{}cat-arrow(C)  (cube(v)  c)  (cube(v)  flip(c;y))\mkleeneclose{}\mcdot{}
  THEN  Try  ((BLemma  `subtype\_rel-equal`    THEN  Auto))
  THEN  RenameTo  `g'  `v')

---

Home Index