---

Step * 2 1 2 1 2 2 2 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. ¬3 < ||bx||
10. K : Cname List
11. f : name-morph(I;K)
12. ∀i:nameset(I). ((i ∈ J) ⇒ (↑isname(f i)))
13. ↑isname(f x)
14. ¬False
15. f ∈ nameset(J) ⟶ nameset(K)
16. map(f;J) ∈ nameset(K) List
17. f x ∈ nameset(K)
18. nameset([x / J]) ⊆r name-morph-domain(f;I)
19. ¬↑null(J)
20. ¬↑null(map(f;J))
21. box : open_box(cubical-nerve(cat(G));K;map(f;J);f x;i)
22. ¬3 < ||box||
23. 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)
24. ∀f1:name-morph(K;[]). (nerve_box_label(bx;(f o f1)) = nerve_box_label(box;f1) ∈ cat-ob(cat(G)))
25. ||bx|| = ||box|| ∈ ℤ
26. ||bx|| ≤ 3
27. (∀j'∈J.j' = hd(J) ∈ Cname)
28. ||box|| ≤ 3
29. (∀j'∈map(f;J).j' = hd(map(f;J)) ∈ Cname)
30. ∀f1:name-morph(K;[]). (nerve_box_label(bx;(f o f1)) = nerve_box_label(box;f1) ∈ cat-ob(cat(G)))
31. k : nameset(K)
32. f1 : {f:name-morph(K;[])| (f k) = 0 ∈ ℕ2} 
33. hd(map(f;J)) ∈ nameset(map(f;J))
⊢ poset_functor_extend(cat(G);I;λc.nerve_box_label(bx;c);
                       λy,c. nerve_box_edge1(G;bx;x;i;hd(J);c;y);(f o f1);(f o flip(f1;k)))
= nerve_box_edge1(G;box;f x;i;hd(map(f;J));f1;k)
∈ (cat-arrow(cat(G)) nerve_box_label(bx;(f o f1)) nerve_box_label(bx;(f o flip(f1;k))))
BY
{ ((Assert hd(J) ∈ nameset(J) BY
          (Unfold `nameset` 0 THEN Auto))
   THEN (InstLemma `poset_functor_extend-flip` [⌜cat(G)⌝;⌜I⌝;⌜λc.nerve_box_label(bx;c)⌝;
         ⌜λy,c. nerve_box_edge1(G;bx;x;i;hd(J);c;y)⌝]⋅
         THENA (Reduce 0 THEN Try (QuickAuto) THEN RepeatFor 2 (MemCD') THEN Auto)
         )
   THEN Thin (-2)) }

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. ¬3 < ||bx||
10. K : Cname List
11. f : name-morph(I;K)
12. ∀i:nameset(I). ((i ∈ J) ⇒ (↑isname(f i)))
13. ↑isname(f x)
14. ¬False
15. f ∈ nameset(J) ⟶ nameset(K)
16. map(f;J) ∈ nameset(K) List
17. f x ∈ nameset(K)
18. nameset([x / J]) ⊆r name-morph-domain(f;I)
19. ¬↑null(J)
20. ¬↑null(map(f;J))
21. box : open_box(cubical-nerve(cat(G));K;map(f;J);f x;i)
22. ¬3 < ||box||
23. 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)
24. ∀f1:name-morph(K;[]). (nerve_box_label(bx;(f o f1)) = nerve_box_label(box;f1) ∈ cat-ob(cat(G)))
25. ||bx|| = ||box|| ∈ ℤ
26. ||bx|| ≤ 3
27. (∀j'∈J.j' = hd(J) ∈ Cname)
28. ||box|| ≤ 3
29. (∀j'∈map(f;J).j' = hd(map(f;J)) ∈ Cname)
30. ∀f1:name-morph(K;[]). (nerve_box_label(bx;(f o f1)) = nerve_box_label(box;f1) ∈ cat-ob(cat(G)))
31. k : nameset(K)
32. f1 : {f:name-morph(K;[])| (f k) = 0 ∈ ℕ2} 
33. hd(map(f;J)) ∈ nameset(map(f;J))
34. ∀i@0:nameset(I). ∀c:cat-ob(poset-cat(I)).
      poset_functor_extend(cat(G);I;λc.nerve_box_label(bx;c);λy,c. nerve_box_edge1(G;bx;x;i;hd(J);c;y);c;flip(c;i@0))
      = ((λy,c. nerve_box_edge1(G;bx;x;i;hd(J);c;y)) i@0 c)
      ∈ (cat-arrow(cat(G)) ((λc.nerve_box_label(bx;c)) c) ((λc.nerve_box_label(bx;c)) flip(c;i@0))) 
      supposing (c i@0) = 0 ∈ ℕ2
⊢ poset_functor_extend(cat(G);I;λc.nerve_box_label(bx;c);
                       λy,c. nerve_box_edge1(G;bx;x;i;hd(J);c;y);(f o f1);(f o flip(f1;k)))
= nerve_box_edge1(G;box;f x;i;hd(map(f;J));f1;k)
∈ (cat-arrow(cat(G)) nerve_box_label(bx;(f o f1)) nerve_box_label(bx;(f o flip(f1;k))))

---

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.  \mneg{}3  <  ||bx||
10.  K  :  Cname  List
11.  f  :  name-morph(I;K)
12.  \mforall{}i:nameset(I).  ((i  \mmember{}  J)  {}\mRightarrow{}  (\muparrow{}isname(f  i)))
13.  \muparrow{}isname(f  x)
14.  \mneg{}False
15.  f  \mmember{}  nameset(J)  {}\mrightarrow{}  nameset(K)
16.  map(f;J)  \mmember{}  nameset(K)  List
17.  f  x  \mmember{}  nameset(K)
18.  nameset([x  /  J])  \msubseteq{}r  name-morph-domain(f;I)
19.  \mneg{}\muparrow{}null(J)
20.  \mneg{}\muparrow{}null(map(f;J))
21.  box  :  open\_box(cubical-nerve(cat(G));K;map(f;J);f  x;i)
22.  \mneg{}3  <  ||box||
23.  open\_box\_image(cubical-nerve(cat(G));I;K;f;bx)  =  box
24.  \mforall{}f1:name-morph(K;[]).  (nerve\_box\_label(bx;(f  o  f1))  =  nerve\_box\_label(box;f1))
25.  ||bx||  =  ||box||
26.  ||bx||  \mleq{}  3
27.  (\mforall{}j'\mmember{}J.j'  =  hd(J))
28.  ||box||  \mleq{}  3
29.  (\mforall{}j'\mmember{}map(f;J).j'  =  hd(map(f;J)))
30.  \mforall{}f1:name-morph(K;[]).  (nerve\_box\_label(bx;(f  o  f1))  =  nerve\_box\_label(box;f1))
31.  k  :  nameset(K)
32.  f1  :  \{f:name-morph(K;[])|  (f  k)  =  0\} 
33.  hd(map(f;J))  \mmember{}  nameset(map(f;J))
\mvdash{}  poset\_functor\_extend(cat(G);I;\mlambda{}c.nerve\_box\_label(bx;c);
                                              \mlambda{}y,c.  nerve\_box\_edge1(G;bx;x;i;hd(J);c;y);(f  o  f1);(f  o  flip(f1;k)))
=  nerve\_box\_edge1(G;box;f  x;i;hd(map(f;J));f1;k)


By

---

Latex:
((Assert  hd(J)  \mmember{}  nameset(J)  BY
                (Unfold  `nameset`  0  THEN  Auto))
  THEN  (InstLemma  `poset\_functor\_extend-flip`  [\mkleeneopen{}cat(G)\mkleeneclose{};\mkleeneopen{}I\mkleeneclose{};\mkleeneopen{}\mlambda{}c.nerve\_box\_label(bx;c)\mkleeneclose{};
              \mkleeneopen{}\mlambda{}y,c.  nerve\_box\_edge1(G;bx;x;i;hd(J);c;y)\mkleeneclose{}]\mcdot{}
              THENA  (Reduce  0  THEN  Try  (QuickAuto)  THEN  RepeatFor  2  (MemCD')  THEN  Auto)
              )
  THEN  Thin  (-2))

---

Home Index