---

Step * of Lemma groupoid-nerve-filler-fills

∀G:Groupoid. ∀I:Cname List. ∀J:nameset(I) List. ∀x:nameset(I). ∀i:ℕ2. ∀bx:open_box(cubical-nerve(cat(G));I;J;x;i).
  fills-open_box(cubical-nerve(cat(G));I;bx;(λI,J,x,i,box. groupoid-nerve-filler(G;I;J;x;i;box)) I J x i bx)
BY
{ TACTIC:Auto }

1
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)
⊢ fills-open_box(cubical-nerve(cat(G));I;bx;(λI,J,x,i,box. groupoid-nerve-filler(G;I;J;x;i;box)) I J x i bx)

---

Latex:

---

Latex:
\mforall{}G:Groupoid.  \mforall{}I:Cname  List.  \mforall{}J:nameset(I)  List.  \mforall{}x:nameset(I).  \mforall{}i:\mBbbN{}2.
\mforall{}bx:open\_box(cubical-nerve(cat(G));I;J;x;i).
    fills-open\_box(cubical-nerve(cat(G));I;bx;(\mlambda{}I,J,x,i,box.  groupoid-nerve-filler(G;I;J;x;i;box))  I  J\000C  x  i  bx)


By

---

Latex:
TACTIC:Auto

---

Home Index