---

Step * 1 2 1 1 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 : 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)
⊢ ∀G:Functor(poset-cat(I-[dimension(f)]);C). ∀F:Functor(poset-cat(I-[dimension(v)]);C).
    (((dimension(f):=direction(f))(F)
    = (dimension(v):=direction(v))(G)
    ∈ cubical-nerve(C)(I-[dimension(v); dimension(f)]))
    ⇒ ((ob(G) L) = (ob(F) L) ∈ cat-ob(C)))
BY
{ (∀h:hyp. (Unfold `face-name` h
            THEN (EqHD h THENA Auto)
            THEN Reduce h
            THEN Fold `face-dimension` h
            THEN HypSubst' h 0
            THEN Reduce (h+1)
            THEN Fold `face-direction` (h+1)
            THEN HypSubst' (h+1) 0) 
   THEN (RWO "cubical-nerve-I-cube" 0 THENA Auto)
   THEN RepUR ``cube-set-restriction cubical-nerve`` 0) }

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)
⊢ ∀G:Functor(poset-cat(I-[dimension(f)]);C). ∀F:Functor(poset-cat(I-[dimension(v)]);C).
    ((functor-comp(poset-functor(I-[dimension(v)];I-[dimension(v); dimension(f)];(dimension(f):=direction(f)));F)
    = functor-comp(poset-functor(I-[dimension(f)];I-[dimension(v); dimension(f)];(dimension(v):=direction(v)));G)
    ∈ Functor(poset-cat(I-[dimension(v); dimension(f)]);C))
    ⇒ ((ob(G) L) = (ob(F) 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  :  I-face(cubical-nerve(C);I)  List
7.  \mforall{}f1,f2:I-face(cubical-nerve(C);I).
          ((f1  \mmember{}  box)
          {}\mRightarrow{}  (f2  \mmember{}  box)
          {}\mRightarrow{}  (\mneg{}(dimension(f1)  =  dimension(f2)))
          {}\mRightarrow{}  ((dimension(f2):=direction(f2))(cube(f1))  =  (dimension(f1):=direction(f1))(cube(f2))))
8.  \mneg{}(x  \mmember{}  J)
9.  l\_subset(Cname;J;I)
10.  \mforall{}y:nameset(J).  \mforall{}c:\mBbbN{}2.    (\mexists{}f\mmember{}box.  face-name(f)  =  <y,  c>)
11.  (\mexists{}f\mmember{}box.  face-name(f)  =  <x,  i>)
12.  (\mforall{}f\mmember{}box.\mneg{}(face-name(f)  =  <x,  1  -  i>))
13.  (\mforall{}f\mmember{}box.(fst(f)  \mmember{}  [x  /  J]))
14.  (\mforall{}f1,f2\mmember{}box.    \mneg{}(face-name(f1)  =  face-name(f2)))
15.  L  :  name-morph(I;[])
16.  ((L  x)  =  i)  \mvee{}  (\mneg{}\muparrow{}null(J))
17.  f  :  I-face(cubical-nerve(C);I)
18.  direction(f)  =  (L  dimension(f))
19.  (f  \mmember{}  box)
20.  v  :  I-face(cubical-nerve(C);I)
21.  (v  \mmember{}  box)
22.  direction(v)  =  (L  dimension(v))
23.  nerve-box-face(box;L)  =  v
24.  \mneg{}(dimension(v)  =  dimension(f))
\mvdash{}  \mforall{}G:Functor(poset-cat(I-[dimension(f)]);C).  \mforall{}F:Functor(poset-cat(I-[dimension(v)]);C).
        (((dimension(f):=direction(f))(F)  =  (dimension(v):=direction(v))(G))  {}\mRightarrow{}  ((ob(G)  L)  =  (ob(F)  L)))


By

---

Latex:
(\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  Reduce  (h+1)
                    THEN  Fold  `face-direction`  (h+1)
                    THEN  HypSubst'  (h+1)  0) 
  THEN  (RWO  "cubical-nerve-I-cube"  0  THENA  Auto)
  THEN  RepUR  ``cube-set-restriction  cubical-nerve``  0)

---

Home Index