---

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


1. G : Groupoid
2. I : Cname List
3. J : nameset(I) List
4. x : nameset(I)
5. i : ℕ2
6. bx : open_box(cubical-nerve(cat(G));I;J;x;i)
7. K : Cname List
8. f : name-morph(I;K)
9. ∀i:nameset(I). ((i ∈ J) ⇒ (↑isname(f i)))
10. ↑isname(f x)
11. ↑null(J)
⊢ f(groupoid-nerve-filler(G;I;J;x;i;bx))
= groupoid-nerve-filler(G;K;map(f;J);f x;i;open_box_image(cubical-nerve(cat(G));I;K;f;bx))
∈ cubical-nerve(cat(G))(K)
BY
{ ((RWO "cubical-nerve-I-cube" 0 THENA Auto)
   THEN (DVar `J' THEN Auto)
   THEN Reduce 0
   THEN (InstLemma `open_box-nil` [⌜cubical-nerve(cat(G))⌝;⌜I⌝;⌜x⌝;⌜i⌝]⋅ THENA Auto)
   THEN (GenConcl ⌜bx
                   = box
                   ∈ {L:I-face(cubical-nerve(cat(G));I) List| 
                      (||L|| = 1 ∈ ℤ) ∧ (face-name(hd(L)) = <x, i> ∈ (nameset(I) × ℕ2))} ⌝⋅
         THENA Auto
         )
   THEN Thin (-1)
   THEN Thin (-2)
   THEN D -1
   THEN D -2
   THEN Reduce (-1)
   THEN Auto
   THEN D -3
   THEN Auto'
   THEN Thin (-2)
   THEN RepeatFor 2 (D -2)
   THEN RepUR ``face-name`` -1
   THEN (EqHD (-1) THENA Auto)
   THEN All Reduce
   THEN (RWO "cubical-nerve-I-cube" (-3) THENA Auto)
   THEN Eliminate ⌜x1⌝⋅
   THEN Eliminate ⌜u2⌝⋅
   THEN RepUR ``groupoid-nerve-filler groupoid-nerve-filler0`` 0) }

1
1. i : ℕ2
2. G : Groupoid
3. I : Cname List
4. x : nameset(I)
5. bx : open_box(cubical-nerve(cat(G));I;[];x;i)
6. K : Cname List
7. f : name-morph(I;K)
8. ∀i:nameset(I). ((i ∈ []) ⇒ (↑isname(f i)))
9. ↑isname(f x)
10. True
11. x1 : nameset(I)
12. u2 : ℕ2
13. u3 : Functor(poset-cat(I-[x]);cat(G))
14. x1 = x ∈ nameset(I)
15. u2 = i ∈ ℕ2
⊢ f(functor-comp(poset-functor(I-[x];I;iota(x));u3))
= functor-comp(poset-functor(K-[f x];K;iota(f x));snd(snd(hd(open_box_image(cubical-nerve(cat(G));I;K;f;[<x, i, u3>]))))\000C)
∈ Functor(poset-cat(K);cat(G))

---

Latex:

---

Latex:

1.  G  :  Groupoid
2.  I  :  Cname  List
3.  J  :  nameset(I)  List
4.  x  :  nameset(I)
5.  i  :  \mBbbN{}2
6.  bx  :  open\_box(cubical-nerve(cat(G));I;J;x;i)
7.  K  :  Cname  List
8.  f  :  name-morph(I;K)
9.  \mforall{}i:nameset(I).  ((i  \mmember{}  J)  {}\mRightarrow{}  (\muparrow{}isname(f  i)))
10.  \muparrow{}isname(f  x)
11.  \muparrow{}null(J)
\mvdash{}  f(groupoid-nerve-filler(G;I;J;x;i;bx))
=  groupoid-nerve-filler(G;K;map(f;J);f  x;i;open\_box\_image(cubical-nerve(cat(G));I;K;f;bx))


By

---

Latex:
((RWO  "cubical-nerve-I-cube"  0  THENA  Auto)
  THEN  (DVar  `J'  THEN  Auto)
  THEN  Reduce  0
  THEN  (InstLemma  `open\_box-nil`  [\mkleeneopen{}cubical-nerve(cat(G))\mkleeneclose{};\mkleeneopen{}I\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}i\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (GenConcl  \mkleeneopen{}bx  =  box\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Thin  (-1)
  THEN  Thin  (-2)
  THEN  D  -1
  THEN  D  -2
  THEN  Reduce  (-1)
  THEN  Auto
  THEN  D  -3
  THEN  Auto'
  THEN  Thin  (-2)
  THEN  RepeatFor  2  (D  -2)
  THEN  RepUR  ``face-name``  -1
  THEN  (EqHD  (-1)  THENA  Auto)
  THEN  All  Reduce
  THEN  (RWO  "cubical-nerve-I-cube"  (-3)  THENA  Auto)
  THEN  Eliminate  \mkleeneopen{}x1\mkleeneclose{}\mcdot{}
  THEN  Eliminate  \mkleeneopen{}u2\mkleeneclose{}\mcdot{}
  THEN  RepUR  ``groupoid-nerve-filler  groupoid-nerve-filler0``  0)

---

Home Index