---

Step * 1 1 1 2 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
16. f x ∈ nameset(K)
17. iota(x) ∈ name-morph(I-[x];I)
18. iota(f x) ∈ name-morph(K-[f x];K)
19. f ∈ name-morph(I-[x];K-[f x])
⊢ 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))
BY
{ (RWO "functor-comp-assoc" 0 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)
19. f ∈ name-morph(I-[x];K-[f x])
⊢ functor-comp(functor-comp(poset-functor(I;K;f);poset-functor(I-[x];I;iota(x)));u3)
= functor-comp(functor-comp(poset-functor(K-[f x];K;iota(f x));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
16.  f  x  \mmember{}  nameset(K)
17.  iota(x)  \mmember{}  name-morph(I-[x];I)
18.  iota(f  x)  \mmember{}  name-morph(K-[f  x];K)
19.  f  \mmember{}  name-morph(I-[x];K-[f  x])
\mvdash{}  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))


By

---

Latex:
(RWO  "functor-comp-assoc"  0  THENA  Auto)

---

Home Index