---

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

.....assertion..... 
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))
⊢ λ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)))
BY
{ TACTIC:(RepeatFor 2 ((MemCD THENA Auto))
          THEN Reduce 0
          THEN D -2
          THEN RepeatFor 2 ((RW  ListC (-2) THENA Auto))
          THEN D -1) }

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 : Cname
21. (z ∈ I) ∧ (¬(z = y ∈ Cname))
22. f : name-morph(I-[y];[])
23. (f z) = 0 ∈ ℕ2
⊢ nerve_box_edge1(G;bx;x;i;hd(J);((y:=a) o f);z) ∈ cat-arrow(cat(G)) nerve_box_label(bx;((y:=a) o f)) 
                                                   nerve_box_label(bx;((y:=a) o flip(f;z)))

---

Latex:

---

Latex:
.....assertion..... 
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))
\mvdash{}  \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)))


By

---

Latex:
TACTIC:(RepeatFor  2  ((MemCD  THENA  Auto))
                THEN  Reduce  0
                THEN  D  -2
                THEN  RepeatFor  2  ((RW    ListC  (-2)  THENA  Auto))
                THEN  D  -1)

---

Home Index