---

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


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))
BY
{ (RepUR ``cube-set-restriction cubical-nerve open_box_image face-image`` 0
   THEN (FLemma `assert-isname` [9] THENA Auto)
   THEN (InstLemma `iota-wf` [⌜I⌝;⌜x⌝]⋅ THEN Auto)
   THEN (InstLemma `iota-wf` [⌜K⌝;⌜f x⌝]⋅ THENA Auto)) }

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
16. f x ∈ nameset(K)
17. iota(x) ∈ name-morph(I-[x];I)
18. iota(f x) ∈ name-morph(K-[f x];K)
⊢ functor-comp(poset-functor(I;K;f);functor-comp(poset-functor(I-[x];I;iota(x));u3))
= functor-comp(poset-functor(K-[f x];K;iota(f x));functor-comp(poset-functor(I-[x];K-[f x];f);u3))
∈ Functor(poset-cat(K);cat(G))

---

Latex:

---

Latex:

1.  i  :  \mBbbN{}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.  \mforall{}i:nameset(I).  ((i  \mmember{}  [])  {}\mRightarrow{}  (\muparrow{}isname(f  i)))
9.  \muparrow{}isname(f  x)
10.  True
11.  x1  :  nameset(I)
12.  u2  :  \mBbbN{}2
13.  u3  :  Functor(poset-cat(I-[x]);cat(G))
14.  x1  =  x
15.  u2  =  i
\mvdash{}  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>])))))


By

---

Latex:
(RepUR  ``cube-set-restriction  cubical-nerve  open\_box\_image  face-image``  0
  THEN  (FLemma  `assert-isname`  [9]  THENA  Auto)
  THEN  (InstLemma  `iota-wf`  [\mkleeneopen{}I\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THEN  Auto)
  THEN  (InstLemma  `iota-wf`  [\mkleeneopen{}K\mkleeneclose{};\mkleeneopen{}f  x\mkleeneclose{}]\mcdot{}  THENA  Auto))

---

Home Index