---

Step * of Lemma nerve_box_label_wf

∀[C:SmallCategory]. ∀[I:Cname List]. ∀[J:nameset(I) List]. ∀[x:nameset(I)]. ∀[i:ℕ2].
∀[box:open_box(cubical-nerve(C);I;J;x;i)]. ∀[L:name-morph(I;[])].
  nerve_box_label(box;L) ∈ cat-ob(C) supposing ((L x) = i ∈ ℕ2) ∨ (¬↑null(J))
BY
{ (Auto
   THEN Unfold `nerve_box_label` 0
   THEN (GenConclTerm ⌜nerve-box-face(box;L)⌝⋅ THENA Auto)
   THEN D -2
   THEN RepeatFor 2 (D -3)
   THEN RepUR ``face-cube`` 0
   THEN (RWO "cubical-nerve-I-cube" (-3) THENA Auto)
   THEN MemCD) }

1
.....subterm..... T:t
1:n
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. x1 : nameset(I)@i
10. v2 : ℕ2@i
11. v3 : Functor(poset-cat(I-[x1]);C)@i
12. (<x1, v2, v3> ∈ box) ∧ (direction(<x1, v2, v3>) = (L dimension(<x1, v2, v3>)) ∈ ℕ2)@i
13. nerve-box-face(box;L)
= <x1, v2, v3>
∈ {f:I-face(cubical-nerve(C);I)| (f ∈ box) ∧ (direction(f) = (L dimension(f)) ∈ ℕ2)} @i
⊢ functor-ob(v3) ∈ cat-ob(poset-cat(I-[x1])) ⟶ cat-ob(C)

2
.....subterm..... T:t
2:n
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. x1 : nameset(I)@i
10. v2 : ℕ2@i
11. v3 : Functor(poset-cat(I-[x1]);C)@i
12. (<x1, v2, v3> ∈ box) ∧ (direction(<x1, v2, v3>) = (L dimension(<x1, v2, v3>)) ∈ ℕ2)@i
13. nerve-box-face(box;L)
= <x1, v2, v3>
∈ {f:I-face(cubical-nerve(C);I)| (f ∈ box) ∧ (direction(f) = (L dimension(f)) ∈ ℕ2)} @i
⊢ L ∈ cat-ob(poset-cat(I-[x1]))

---

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{}[L:name-morph(I;[])].
    nerve\_box\_label(box;L)  \mmember{}  cat-ob(C)  supposing  ((L  x)  =  i)  \mvee{}  (\mneg{}\muparrow{}null(J))


By

---

Latex:
(Auto
  THEN  Unfold  `nerve\_box\_label`  0
  THEN  (GenConclTerm  \mkleeneopen{}nerve-box-face(box;L)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  D  -2
  THEN  RepeatFor  2  (D  -3)
  THEN  RepUR  ``face-cube``  0
  THEN  (RWO  "cubical-nerve-I-cube"  (-3)  THENA  Auto)
  THEN  MemCD)

---

Home Index