Step
*
1
1
1
2
1
1
1
1
of Lemma
groupoid-nerve-filler-uniform
.....subterm..... T:t
3:n
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])
⊢ (iota(x) o f) = (f o iota(f x)) ∈ name-morph(I-[x];K)
BY
{ BLemma `name-morph-ext` }
1
.....wf.....
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])
⊢ I-[x] ∈ Cname List
2
.....wf.....
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])
⊢ K ∈ Cname List
3
.....wf.....
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])
⊢ (iota(x) o f) ∈ name-morph(I-[x];K)
4
.....wf.....
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])
⊢ (f o iota(f x)) ∈ name-morph(I-[x];K)
5
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])
⊢ ∀x1:nameset(I-[x]). (((iota(x) o f) x1) = ((f o iota(f x)) x1) ∈ extd-nameset(K))
Latex:
Latex:
.....subterm..... T:t
3:n
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{} (iota(x) o f) = (f o iota(f x))
By
Latex:
BLemma `name-morph-ext`
Home
Index