---

Step * of Lemma groupoid-nerve-filler-uniform

No Annotations
∀G:Groupoid. uniform-Kan-filler(cubical-nerve(cat(G));λI,J,x,i,box. groupoid-nerve-filler(G;I;J;x;i;box))
BY
{ (Auto THEN D 0 THEN Auto THEN (Decide ↑null(J) THENA 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)
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)

2
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)

---

Latex:

---

Latex:
No  Annotations
\mforall{}G:Groupoid
    uniform-Kan-filler(cubical-nerve(cat(G));\mlambda{}I,J,x,i,box.  groupoid-nerve-filler(G;I;J;x;i;box))


By

---

Latex:
(Auto  THEN  D  0  THEN  Auto  THEN  (Decide  \muparrow{}null(J)  THENA  Auto))

---

Home Index