---

Step * 2 1 2 1 1 1 of Lemma groupoid-nerve-filler-uniform


1. G : Groupoid
2. True
3. I : Cname List
4. J : nameset(I) List
5. ¬(J = [] ∈ (nameset(I) List))
6. x : nameset(I)
7. i : ℕ2
8. bx : open_box(cubical-nerve(cat(G));I;J;x;i)
9. K : Cname List
10. f : name-morph(I;K)
11. ∀i:nameset(I). ((i ∈ J) ⇒ (↑isname(f i)))
12. ↑isname(f x)
13. ¬False
14. f ∈ nameset(J) ⟶ nameset(K)
15. map(f;J) ∈ nameset(K) List
16. f x ∈ nameset(K)
17. nameset([x / J]) ⊆r name-morph-domain(f;I)
18. ¬↑null(J)
19. ¬↑null(map(f;J))
20. box : open_box(cubical-nerve(cat(G));K;map(f;J);f x;i)
21. open_box_image(cubical-nerve(cat(G));I;K;f;bx) = box ∈ open_box(cubical-nerve(cat(G));K;map(f;J);f x;i)
22. f1 : name-morph(K;[])
⊢ nerve_box_label(bx;(f o f1)) = nerve_box_label(box;f1) ∈ cat-ob(cat(G))
BY
{ TACTIC:(InstLemma `nerve_box_label_same` [⌜cat(G)⌝;⌜K⌝;⌜map(f;J)⌝;⌜f x⌝;⌜i⌝;⌜box⌝;⌜f1⌝]⋅ THENA Auto) }

1
1. G : Groupoid
2. True
3. I : Cname List
4. J : nameset(I) List
5. ¬(J = [] ∈ (nameset(I) List))
6. x : nameset(I)
7. i : ℕ2
8. bx : open_box(cubical-nerve(cat(G));I;J;x;i)
9. K : Cname List
10. f : name-morph(I;K)
11. ∀i:nameset(I). ((i ∈ J) ⇒ (↑isname(f i)))
12. ↑isname(f x)
13. ¬False
14. f ∈ nameset(J) ⟶ nameset(K)
15. map(f;J) ∈ nameset(K) List
16. f x ∈ nameset(K)
17. nameset([x / J]) ⊆r name-morph-domain(f;I)
18. ¬↑null(J)
19. ¬↑null(map(f;J))
20. box : open_box(cubical-nerve(cat(G));K;map(f;J);f x;i)
21. open_box_image(cubical-nerve(cat(G));I;K;f;bx) = box ∈ open_box(cubical-nerve(cat(G));K;map(f;J);f x;i)
22. f1 : name-morph(K;[])
23. ∀f:I-face(cubical-nerve(cat(G));K)
      ((cube(f) f1) = nerve_box_label(box;f1) ∈ cat-ob(cat(G))) supposing 
         ((f ∈ box) and 
         (direction(f) = (f1 dimension(f)) ∈ ℕ2))
⊢ nerve_box_label(bx;(f o f1)) = nerve_box_label(box;f1) ∈ cat-ob(cat(G))

---

Latex:

---

Latex:

1.  G  :  Groupoid
2.  True
3.  I  :  Cname  List
4.  J  :  nameset(I)  List
5.  \mneg{}(J  =  [])
6.  x  :  nameset(I)
7.  i  :  \mBbbN{}2
8.  bx  :  open\_box(cubical-nerve(cat(G));I;J;x;i)
9.  K  :  Cname  List
10.  f  :  name-morph(I;K)
11.  \mforall{}i:nameset(I).  ((i  \mmember{}  J)  {}\mRightarrow{}  (\muparrow{}isname(f  i)))
12.  \muparrow{}isname(f  x)
13.  \mneg{}False
14.  f  \mmember{}  nameset(J)  {}\mrightarrow{}  nameset(K)
15.  map(f;J)  \mmember{}  nameset(K)  List
16.  f  x  \mmember{}  nameset(K)
17.  nameset([x  /  J])  \msubseteq{}r  name-morph-domain(f;I)
18.  \mneg{}\muparrow{}null(J)
19.  \mneg{}\muparrow{}null(map(f;J))
20.  box  :  open\_box(cubical-nerve(cat(G));K;map(f;J);f  x;i)
21.  open\_box\_image(cubical-nerve(cat(G));I;K;f;bx)  =  box
22.  f1  :  name-morph(K;[])
\mvdash{}  nerve\_box\_label(bx;(f  o  f1))  =  nerve\_box\_label(box;f1)


By

---

Latex:
TACTIC:(InstLemma  `nerve\_box\_label\_same`  [\mkleeneopen{}cat(G)\mkleeneclose{};\mkleeneopen{}K\mkleeneclose{};\mkleeneopen{}map(f;J)\mkleeneclose{};\mkleeneopen{}f  x\mkleeneclose{};\mkleeneopen{}i\mkleeneclose{};\mkleeneopen{}box\mkleeneclose{};\mkleeneopen{}f1\mkleeneclose{}]\mcdot{}  THENA  Auto)

---

Home Index