---

Step * 1 2 of Lemma nerve_box_label_same


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;[])
8. ((L x) = i ∈ ℕ2) ∨ (¬↑null(J))
9. f : I-face(cubical-nerve(C);I)
10. direction(f) = (L dimension(f)) ∈ ℕ2
11. (f ∈ box)
12. v : I-face(cubical-nerve(C);I)
13. (v ∈ box) ∧ (direction(v) = (L dimension(v)) ∈ ℕ2)
14. nerve-box-face(box;L) = v ∈ {f:I-face(cubical-nerve(C);I)| (f ∈ box) ∧ (direction(f) = (L dimension(f)) ∈ ℕ2)} 
15. ¬(dimension(v) = dimension(f) ∈ Cname)
⊢ (ob(cube(f)) L) = (ob(cube(v)) L) ∈ cat-ob(C)
BY
{ (DVar `box'
   THEN Auto
   THEN RepUR ``let`` 0
   THEN (RWO "adjacent-compatible-iff" 7 THENA Auto)
   THEN (InstHyp [⌜v⌝;⌜f⌝] 7⋅
         THENA (Auto
                THEN ∀h:hyp. (Unfold `face-name` h
                              THEN (EqHD h THENA Auto)
                              THEN Reduce h
                              THEN Fold `face-dimension` h
                              THEN HypSubst' h 0) 
                THEN Auto)
         )) }

1
1. C : SmallCategory
2. I : Cname List
3. J : nameset(I) List
4. x : nameset(I)
5. i : ℕ2
6. box : I-face(cubical-nerve(C);I) List
7. ∀f1,f2:I-face(cubical-nerve(C);I).
     ((f1 ∈ box)
     ⇒ (f2 ∈ box)
     ⇒ (¬(dimension(f1) = dimension(f2) ∈ Cname))
     ⇒ ((dimension(f2):=direction(f2))(cube(f1))
        = (dimension(f1):=direction(f1))(cube(f2))
        ∈ cubical-nerve(C)(I-[dimension(f1); dimension(f2)])))
8. ¬(x ∈ J)
9. l_subset(Cname;J;I)
10. ∀y:nameset(J). ∀c:ℕ2.  (∃f∈box. face-name(f) = <y, c> ∈ (nameset(I) × ℕ2))
11. (∃f∈box. face-name(f) = <x, i> ∈ (nameset(I) × ℕ2))
12. (∀f∈box.¬(face-name(f) = <x, 1 - i> ∈ (nameset(I) × ℕ2)))
13. (∀f∈box.(fst(f) ∈ [x / J]))
14. (∀f1,f2∈box.  ¬(face-name(f1) = face-name(f2) ∈ (nameset(I) × ℕ2)))
15. L : name-morph(I;[])
16. ((L x) = i ∈ ℕ2) ∨ (¬↑null(J))
17. f : I-face(cubical-nerve(C);I)
18. direction(f) = (L dimension(f)) ∈ ℕ2
19. (f ∈ box)
20. v : I-face(cubical-nerve(C);I)
21. (v ∈ box)
22. direction(v) = (L dimension(v)) ∈ ℕ2
23. nerve-box-face(box;L) = v ∈ {f:I-face(cubical-nerve(C);I)| (f ∈ box) ∧ (direction(f) = (L dimension(f)) ∈ ℕ2)} 
24. ¬(dimension(v) = dimension(f) ∈ Cname)
25. (dimension(f):=direction(f))(cube(v))
= (dimension(v):=direction(v))(cube(f))
∈ cubical-nerve(C)(I-[dimension(v); dimension(f)])
⊢ (ob(cube(f)) L) = (ob(cube(v)) L) ∈ cat-ob(C)

---

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.  L  :  name-morph(I;[])
8.  ((L  x)  =  i)  \mvee{}  (\mneg{}\muparrow{}null(J))
9.  f  :  I-face(cubical-nerve(C);I)
10.  direction(f)  =  (L  dimension(f))
11.  (f  \mmember{}  box)
12.  v  :  I-face(cubical-nerve(C);I)
13.  (v  \mmember{}  box)  \mwedge{}  (direction(v)  =  (L  dimension(v)))
14.  nerve-box-face(box;L)  =  v
15.  \mneg{}(dimension(v)  =  dimension(f))
\mvdash{}  (ob(cube(f))  L)  =  (ob(cube(v))  L)


By

---

Latex:
(DVar  `box'
  THEN  Auto
  THEN  RepUR  ``let``  0
  THEN  (RWO  "adjacent-compatible-iff"  7  THENA  Auto)
  THEN  (InstHyp  [\mkleeneopen{}v\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{}]  7\mcdot{}
              THENA  (Auto
                            THEN  \mforall{}h:hyp.  (Unfold  `face-name`  h
                                                        THEN  (EqHD  h  THENA  Auto)
                                                        THEN  Reduce  h
                                                        THEN  Fold  `face-dimension`  h
                                                        THEN  HypSubst'  h  0) 
                            THEN  Auto)
              ))

---

Home Index