---

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


1. G : Groupoid
2. I : Cname List
3. x : nameset(I)
4. i : ℕ2
5. x1 : nameset(I)
6. u2 : ℕ2
7. u3 : cubical-nerve(cat(G))(I-[x1])
8. face-name(<x1, u2, u3>) = <x, i> ∈ (nameset(I) × ℕ2)
⊢ fills-open_box(cubical-nerve(cat(G));I;[<x1, u2, u3>];groupoid-nerve-filler0(I;x;[<x1, u2, u3>]))
BY
{ TACTIC:(RepUR ``face-name`` -1
          THEN (EqHD (-1) THENA Auto)
          THEN All Reduce
          THEN Eliminate ⌜x1⌝⋅
          THEN Eliminate ⌜u2⌝⋅
          THEN All Thin
          THEN (RWO "cubical-nerve-I-cube" (-1) THENA Auto)
          THEN RenameVar `F' (-1)
          THEN (D 0 THENA Auto)
          THEN Reduce (-1)
          THEN IntSegCases (-1)
          THEN Reduce 0) }

1
1. i : ℕ2
2. G : Groupoid
3. I : Cname List
4. x : nameset(I)
5. F : Functor(poset-cat(I-[x]);cat(G))
6. i@0 : ℤ
7. i@0 = 0 ∈ ℤ
⊢ is-face(cubical-nerve(cat(G));I;groupoid-nerve-filler0(I;x;[<x, i, F>]);<x, i, F>)

---

Latex:

---

Latex:

1.  G  :  Groupoid
2.  I  :  Cname  List
3.  x  :  nameset(I)
4.  i  :  \mBbbN{}2
5.  x1  :  nameset(I)
6.  u2  :  \mBbbN{}2
7.  u3  :  cubical-nerve(cat(G))(I-[x1])
8.  face-name(<x1,  u2,  u3>)  =  <x,  i>
\mvdash{}  fills-open\_box(cubical-nerve(cat(G));I;[<x1,  u2,  u3>];groupoid-nerve-filler0(I;x;[<x1,  u2,  u3>]))


By

---

Latex:
TACTIC:(RepUR  ``face-name``  -1
                THEN  (EqHD  (-1)  THENA  Auto)
                THEN  All  Reduce
                THEN  Eliminate  \mkleeneopen{}x1\mkleeneclose{}\mcdot{}
                THEN  Eliminate  \mkleeneopen{}u2\mkleeneclose{}\mcdot{}
                THEN  All  Thin
                THEN  (RWO  "cubical-nerve-I-cube"  (-1)  THENA  Auto)
                THEN  RenameVar  `F'  (-1)
                THEN  (D  0  THENA  Auto)
                THEN  Reduce  (-1)
                THEN  IntSegCases  (-1)
                THEN  Reduce  0)

---

Home Index