---

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


1. G : Groupoid
2. I : Cname List
3. J : nameset(I) List
4. ¬(J = [] ∈ (nameset(I) List))
5. x : nameset(I)
6. i : ℕ2
7. bx : open_box(cubical-nerve(cat(G));I;J;x;i)
8. ¬3 < ||bx||
9. ||bx|| ≤ 3
10. (∀j'∈J.j' = hd(J) ∈ Cname)
11. ¬↑null(J)
12. i1 : ℕ||bx||
13. y : nameset(I)
14. a : ℕ2
15. F : Functor(poset-cat(I-[y]);cat(G))
16. bx[i1] = <y, a, F> ∈ I-face(cubical-nerve(cat(G));I)
17. (y = x ∈ Cname) ⇒ (a = i ∈ ℕ2)
18. ∀f:name-morph(I-[y];[]). (((y:=a) o f) ∈ name-morph(I;[]))
19. λx.nerve_box_label(bx;((y:=a) o x)) ∈ name-morph(I-[y];[]) ⟶ cat-ob(cat(G))
20. λz,f. nerve_box_edge1(G;bx;x;i;hd(J);((y:=a) o f);z) ∈ i:nameset(I-[y])
    ⟶ c:{c:name-morph(I-[y];[])| (c i) = 0 ∈ ℕ2} 
    ⟶ (cat-arrow(cat(G)) ((λx.nerve_box_label(bx;((y:=a) o x))) c) ((λx.nerve_box_label(bx;((y:=a) o x))) flip(c;i)))
⊢ poset-functor-extends(cat(G);I-[y];λx.nerve_box_label(bx;((y:=a) o x));
                        λz,f. nerve_box_edge1(G;bx;x;i;hd(J);((y:=a) o f);z);F)
⇒ (functor-comp(poset-functor(I;I-[y];(y:=a));groupoid-nerve-filler1(G;I;J;x;i;bx))
   = F
   ∈ Functor(poset-cat(I-[y]);cat(G)))
BY
{ TACTIC:(Assert ∀f:name-morph(I-[y];[]). (direction(<y, a, F>) = (((y:=a) o f) dimension(<y, a, F>)) ∈ ℕ2) BY
                ((D 0 THENA Auto)
                 THEN RepUR ``face-direction face-dimension name-comp face-map`` 0
                 THEN (Subst' (y =z y) ~ tt 0 THENA Auto)
                 THEN RepUR ``uext`` 0
                 THEN OnVar `a' IntSegCases
                 THEN RepUR ``isname`` 0
                 THEN Auto)) }

1
1. G : Groupoid
2. I : Cname List
3. J : nameset(I) List
4. ¬(J = [] ∈ (nameset(I) List))
5. x : nameset(I)
6. i : ℕ2
7. bx : open_box(cubical-nerve(cat(G));I;J;x;i)
8. ¬3 < ||bx||
9. ||bx|| ≤ 3
10. (∀j'∈J.j' = hd(J) ∈ Cname)
11. ¬↑null(J)
12. i1 : ℕ||bx||
13. y : nameset(I)
14. a : ℕ2
15. F : Functor(poset-cat(I-[y]);cat(G))
16. bx[i1] = <y, a, F> ∈ I-face(cubical-nerve(cat(G));I)
17. (y = x ∈ Cname) ⇒ (a = i ∈ ℕ2)
18. ∀f:name-morph(I-[y];[]). (((y:=a) o f) ∈ name-morph(I;[]))
19. λx.nerve_box_label(bx;((y:=a) o x)) ∈ name-morph(I-[y];[]) ⟶ cat-ob(cat(G))
20. λz,f. nerve_box_edge1(G;bx;x;i;hd(J);((y:=a) o f);z) ∈ i:nameset(I-[y])
    ⟶ c:{c:name-morph(I-[y];[])| (c i) = 0 ∈ ℕ2} 
    ⟶ (cat-arrow(cat(G)) ((λx.nerve_box_label(bx;((y:=a) o x))) c) ((λx.nerve_box_label(bx;((y:=a) o x))) flip(c;i)))
21. ∀f:name-morph(I-[y];[]). (direction(<y, a, F>) = (((y:=a) o f) dimension(<y, a, F>)) ∈ ℕ2)
⊢ poset-functor-extends(cat(G);I-[y];λx.nerve_box_label(bx;((y:=a) o x));
                        λz,f. nerve_box_edge1(G;bx;x;i;hd(J);((y:=a) o f);z);F)
⇒ (functor-comp(poset-functor(I;I-[y];(y:=a));groupoid-nerve-filler1(G;I;J;x;i;bx))
   = F
   ∈ Functor(poset-cat(I-[y]);cat(G)))

---

Latex:

---

Latex:

1.  G  :  Groupoid
2.  I  :  Cname  List
3.  J  :  nameset(I)  List
4.  \mneg{}(J  =  [])
5.  x  :  nameset(I)
6.  i  :  \mBbbN{}2
7.  bx  :  open\_box(cubical-nerve(cat(G));I;J;x;i)
8.  \mneg{}3  <  ||bx||
9.  ||bx||  \mleq{}  3
10.  (\mforall{}j'\mmember{}J.j'  =  hd(J))
11.  \mneg{}\muparrow{}null(J)
12.  i1  :  \mBbbN{}||bx||
13.  y  :  nameset(I)
14.  a  :  \mBbbN{}2
15.  F  :  Functor(poset-cat(I-[y]);cat(G))
16.  bx[i1]  =  <y,  a,  F>
17.  (y  =  x)  {}\mRightarrow{}  (a  =  i)
18.  \mforall{}f:name-morph(I-[y];[]).  (((y:=a)  o  f)  \mmember{}  name-morph(I;[]))
19.  \mlambda{}x.nerve\_box\_label(bx;((y:=a)  o  x))  \mmember{}  name-morph(I-[y];[])  {}\mrightarrow{}  cat-ob(cat(G))
20.  \mlambda{}z,f.  nerve\_box\_edge1(G;bx;x;i;hd(J);((y:=a)  o  f);z)  \mmember{}  i:nameset(I-[y])
        {}\mrightarrow{}  c:\{c:name-morph(I-[y];[])|  (c  i)  =  0\} 
        {}\mrightarrow{}  (cat-arrow(cat(G))  ((\mlambda{}x.nerve\_box\_label(bx;((y:=a)  o  x)))  c) 
                ((\mlambda{}x.nerve\_box\_label(bx;((y:=a)  o  x)))  flip(c;i)))
\mvdash{}  poset-functor-extends(cat(G);I-[y];\mlambda{}x.nerve\_box\_label(bx;((y:=a)  o  x));
                                                \mlambda{}z,f.  nerve\_box\_edge1(G;bx;x;i;hd(J);((y:=a)  o  f);z);F)
{}\mRightarrow{}  (functor-comp(poset-functor(I;I-[y];(y:=a));groupoid-nerve-filler1(G;I;J;x;i;bx))  =  F)


By

---

Latex:
TACTIC:(Assert  \mforall{}f:name-morph(I-[y];[]).  (direction(<y,  a,  F>)  =  (((y:=a)  o  f)  dimension(<y,  a,  F>)))\000C  BY
                            ((D  0  THENA  Auto)
                              THEN  RepUR  ``face-direction  face-dimension  name-comp  face-map``  0
                              THEN  (Subst'  (y  =\msubz{}  y)  \msim{}  tt  0  THENA  Auto)
                              THEN  RepUR  ``uext``  0
                              THEN  OnVar  `a'  IntSegCases
                              THEN  RepUR  ``isname``  0
                              THEN  Auto))

---

Home Index