---

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


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>)
BY
{ ... }

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 ∈ ℤ
⊢ functor-comp(poset-functor(I;I-[x];(x:=i));functor-comp(poset-functor(I-[x];I;iota(x));F))
= F
∈ <λJ.Functor(poset-cat(J);cat(G)), λI,J,f,F. functor-comp(poset-functor(I;J;f);F)>(I-[x])

---

Latex:

---

Latex:

1.  i  :  \mBbbN{}2
2.  G  :  Groupoid
3.  I  :  Cname  List
4.  x  :  nameset(I)
5.  F  :  Functor(poset-cat(I-[x]);cat(G))
6.  i@0  :  \mBbbZ{}
7.  i@0  =  0
\mvdash{}  is-face(cubical-nerve(cat(G));I;groupoid-nerve-filler0(I;x;[<x,  i,  F>]);<x,  i,  F>)


By

---

Latex:
...

---

Home Index