Step
*
2
1
2
1
2
2
2
1
1
1
2
3
1
1
1
2
2
1
4
1
1
2
2
2
of Lemma
groupoid-nerve-filler-uniform
1. G : Groupoid
2. True
3. I : Cname List
4. u : nameset(I)
5. J : nameset(I) List
6. u = hd(J) ∈ Cname
7. ¬(J = [] ∈ (nameset(I) List))
8. x : nameset(I)
9. i : ℕ2
10. bx : open_box(cubical-nerve(cat(G));I;J;x;0)
11. ¬3 < ||bx||
12. K : Cname List
13. f : name-morph(I;K)
14. (f u) = hd(map(f;J)) ∈ Cname
15. ∀i:nameset(I). ((i ∈ J) ⇒ (↑isname(f i)))
16. ↑isname(f x)
17. ¬False
18. map(f;J) ∈ nameset(K) List
19. f x ∈ nameset(K)
20. nameset([x / J]) ⊆r name-morph-domain(f;I)
21. ¬↑null(J)
22. ¬↑null(map(f;J))
23. box : open_box(cubical-nerve(cat(G));K;map(f;J);f x;0)
24. ¬3 < ||box||
25. open_box_image(cubical-nerve(cat(G));I;K;f;bx) = box ∈ open_box(cubical-nerve(cat(G));K;map(f;J);f x;0)
26. ∀f1:name-morph(K;[]). (nerve_box_label(bx;(f o f1)) = nerve_box_label(box;f1) ∈ cat-ob(cat(G)))
27. ||bx|| = ||box|| ∈ ℤ
28. ||bx|| ≤ 3
29. (∀j'∈J.j' = hd(J) ∈ Cname)
30. ||box|| ≤ 3
31. (∀j'∈map(f;J).j' = hd(map(f;J)) ∈ Cname)
32. ∀f1:name-morph(K;[]). (nerve_box_label(bx;(f o f1)) = nerve_box_label(box;f1) ∈ cat-ob(cat(G)))
33. k : nameset(K)
34. f1 : {f:name-morph(K;[])| (f k) = 0 ∈ ℕ2}
35. (f o f1) x ≠ 0
36. f1 (f x) ≠ 0
37. hd(map(f;J)) ∈ nameset(map(f;J))
38. ∀i@0:nameset(I). ∀c:cat-ob(poset-cat(I)).
poset_functor_extend(cat(G);I;λc.nerve_box_label(bx;c);λy,c. nerve_box_edge1(G;bx;x;0;hd(J);c;y);c;flip(c;i@0))
= ((λy,c. nerve_box_edge1(G;bx;x;0;hd(J);c;y)) i@0 c)
∈ (cat-arrow(cat(G)) ((λc.nerve_box_label(bx;c)) c) ((λc.nerve_box_label(bx;c)) flip(c;i@0)))
supposing (c i@0) = 0 ∈ ℕ2
39. λi.((↑isname(f i)) ∧ ((f i) = k ∈ Cname)) ∈ nameset(I) ⟶ ℙ
40. i1 : ℕ||I||
41. (f u) = k ∈ Cname
42. u ∈ nameset(I)
43. ((f o f1) u) = 0 ∈ ℕ2
44. poset_functor_extend(cat(G);I;λc.nerve_box_label(bx;c);
λy,c. nerve_box_edge1(G;bx;x;0;hd(J);c;y);(f o f1);flip((f o f1);u))
= ((λy,c. nerve_box_edge1(G;bx;x;0;hd(J);c;y)) u (f o f1))
∈ (cat-arrow(cat(G)) ((λc.nerve_box_label(bx;c)) (f o f1)) ((λc.nerve_box_label(bx;c)) flip((f o f1);u)))
45. (f o flip(f1;k)) = flip((f o f1);u) ∈ name-morph(I;[])
46. I[i1] = u ∈ nameset(I)
47. ↑isname(f u)
48. f u ∈ nameset(K)
49. (f1 (f u)) = 0 ∈ ℕ2
50. ∀f1:name-morph(K;[]). ∀u:nameset(I).
((↑isname(f u))
⇒ ((f1 (f u)) = 0 ∈ ℕ2)
⇒ ((((f1 (f x)) = 0 ∈ ℤ) ∨ (¬((f u) = hd(map(f;J)) ∈ Cname)))
∧ ((((f o f1) x) = 0 ∈ ℤ) ∨ (¬(u = hd(J) ∈ Cname))))
⇒ (nerve_box_edge(box;f1;f u)
= nerve_box_edge(bx;(f o f1);u)
∈ (cat-arrow(cat(G)) nerve_box_label(bx;(f o f1)) nerve_box_label(bx;(f o flip(f1;f u))))))
51. (flip(f1;f x) (f x)) = 0 ∈ ℕ2
52. i = 0 ∈ ℤ
53. ¬(u = x ∈ Cname)
54. ¬((f u) = (f x) ∈ Cname)
55. groupoid-square1(G;nerve_box_label(box;flip(f1;f x));nerve_box_label(box;flip(flip(f1;f x);f u));
nerve_box_label(box;f1);nerve_box_label(box;flip(f1;f u));nerve_box_edge(box;flip(f1;f x);f u);
nerve_box_edge(box;flip(flip(f1;f x);f u);f x);nerve_box_edge(box;flip(f1;f x);f x))
= groupoid-square1(G;nerve_box_label(bx;flip((f o f1);x));nerve_box_label(bx;flip(flip((f o f1);x);u));
nerve_box_label(bx;(f o f1));nerve_box_label(bx;flip((f o f1);u));nerve_box_edge(bx;flip((f o f1);x);u);
nerve_box_edge(bx;flip(flip((f o f1);x);u);x);nerve_box_edge(bx;flip((f o f1);x);x))
∈ {d:cat-arrow(cat(G)) nerve_box_label(box;f1) nerve_box_label(box;flip(f1;f u))|
nerve_box_edge(box;flip(f1;f x);f u) o nerve_box_edge(box;flip(flip(f1;f x);f u);f x)
= nerve_box_edge(box;flip(f1;f x);f x) o d}
56. d : cat-arrow(cat(G)) nerve_box_label(box;f1) nerve_box_label(box;flip(f1;f u))
⊢ istype(nerve_box_edge(box;flip(f1;f x);f u) o nerve_box_edge(box;flip(flip(f1;f x);f u);f x)
= nerve_box_edge(box;flip(f1;f x);f x) o d)
BY
{ (At ⌜Type⌝ (D 0)⋅ THEN MemCD) }
1
.....subterm..... T:t
1:n
1. G : Groupoid
2. True
3. I : Cname List
4. u : nameset(I)
5. J : nameset(I) List
6. u = hd(J) ∈ Cname
7. ¬(J = [] ∈ (nameset(I) List))
8. x : nameset(I)
9. i : ℕ2
10. bx : open_box(cubical-nerve(cat(G));I;J;x;0)
11. ¬3 < ||bx||
12. K : Cname List
13. f : name-morph(I;K)
14. (f u) = hd(map(f;J)) ∈ Cname
15. ∀i:nameset(I). ((i ∈ J) ⇒ (↑isname(f i)))
16. ↑isname(f x)
17. ¬False
18. map(f;J) ∈ nameset(K) List
19. f x ∈ nameset(K)
20. nameset([x / J]) ⊆r name-morph-domain(f;I)
21. ¬↑null(J)
22. ¬↑null(map(f;J))
23. box : open_box(cubical-nerve(cat(G));K;map(f;J);f x;0)
24. ¬3 < ||box||
25. open_box_image(cubical-nerve(cat(G));I;K;f;bx) = box ∈ open_box(cubical-nerve(cat(G));K;map(f;J);f x;0)
26. ∀f1:name-morph(K;[]). (nerve_box_label(bx;(f o f1)) = nerve_box_label(box;f1) ∈ cat-ob(cat(G)))
27. ||bx|| = ||box|| ∈ ℤ
28. ||bx|| ≤ 3
29. (∀j'∈J.j' = hd(J) ∈ Cname)
30. ||box|| ≤ 3
31. (∀j'∈map(f;J).j' = hd(map(f;J)) ∈ Cname)
32. ∀f1:name-morph(K;[]). (nerve_box_label(bx;(f o f1)) = nerve_box_label(box;f1) ∈ cat-ob(cat(G)))
33. k : nameset(K)
34. f1 : {f:name-morph(K;[])| (f k) = 0 ∈ ℕ2}
35. (f o f1) x ≠ 0
36. f1 (f x) ≠ 0
37. hd(map(f;J)) ∈ nameset(map(f;J))
38. ∀i@0:nameset(I). ∀c:cat-ob(poset-cat(I)).
poset_functor_extend(cat(G);I;λc.nerve_box_label(bx;c);λy,c. nerve_box_edge1(G;bx;x;0;hd(J);c;y);c;flip(c;i@0))
= ((λy,c. nerve_box_edge1(G;bx;x;0;hd(J);c;y)) i@0 c)
∈ (cat-arrow(cat(G)) ((λc.nerve_box_label(bx;c)) c) ((λc.nerve_box_label(bx;c)) flip(c;i@0)))
supposing (c i@0) = 0 ∈ ℕ2
39. λi.((↑isname(f i)) ∧ ((f i) = k ∈ Cname)) ∈ nameset(I) ⟶ ℙ
40. i1 : ℕ||I||
41. (f u) = k ∈ Cname
42. u ∈ nameset(I)
43. ((f o f1) u) = 0 ∈ ℕ2
44. poset_functor_extend(cat(G);I;λc.nerve_box_label(bx;c);
λy,c. nerve_box_edge1(G;bx;x;0;hd(J);c;y);(f o f1);flip((f o f1);u))
= ((λy,c. nerve_box_edge1(G;bx;x;0;hd(J);c;y)) u (f o f1))
∈ (cat-arrow(cat(G)) ((λc.nerve_box_label(bx;c)) (f o f1)) ((λc.nerve_box_label(bx;c)) flip((f o f1);u)))
45. (f o flip(f1;k)) = flip((f o f1);u) ∈ name-morph(I;[])
46. I[i1] = u ∈ nameset(I)
47. ↑isname(f u)
48. f u ∈ nameset(K)
49. (f1 (f u)) = 0 ∈ ℕ2
50. ∀f1:name-morph(K;[]). ∀u:nameset(I).
((↑isname(f u))
⇒ ((f1 (f u)) = 0 ∈ ℕ2)
⇒ ((((f1 (f x)) = 0 ∈ ℤ) ∨ (¬((f u) = hd(map(f;J)) ∈ Cname)))
∧ ((((f o f1) x) = 0 ∈ ℤ) ∨ (¬(u = hd(J) ∈ Cname))))
⇒ (nerve_box_edge(box;f1;f u)
= nerve_box_edge(bx;(f o f1);u)
∈ (cat-arrow(cat(G)) nerve_box_label(bx;(f o f1)) nerve_box_label(bx;(f o flip(f1;f u))))))
51. (flip(f1;f x) (f x)) = 0 ∈ ℕ2
52. i = 0 ∈ ℤ
53. ¬(u = x ∈ Cname)
54. ¬((f u) = (f x) ∈ Cname)
55. groupoid-square1(G;nerve_box_label(box;flip(f1;f x));nerve_box_label(box;flip(flip(f1;f x);f u));
nerve_box_label(box;f1);nerve_box_label(box;flip(f1;f u));nerve_box_edge(box;flip(f1;f x);f u);
nerve_box_edge(box;flip(flip(f1;f x);f u);f x);nerve_box_edge(box;flip(f1;f x);f x))
= groupoid-square1(G;nerve_box_label(bx;flip((f o f1);x));nerve_box_label(bx;flip(flip((f o f1);x);u));
nerve_box_label(bx;(f o f1));nerve_box_label(bx;flip((f o f1);u));nerve_box_edge(bx;flip((f o f1);x);u);
nerve_box_edge(bx;flip(flip((f o f1);x);u);x);nerve_box_edge(bx;flip((f o f1);x);x))
∈ {d:cat-arrow(cat(G)) nerve_box_label(box;f1) nerve_box_label(box;flip(f1;f u))|
nerve_box_edge(box;flip(f1;f x);f u) o nerve_box_edge(box;flip(flip(f1;f x);f u);f x)
= nerve_box_edge(box;flip(f1;f x);f x) o d}
56. d : cat-arrow(cat(G)) nerve_box_label(box;f1) nerve_box_label(box;flip(f1;f u))
⊢ cat(G) ∈ SmallCategory
2
.....subterm..... T:t
2:n
1. G : Groupoid
2. True
3. I : Cname List
4. u : nameset(I)
5. J : nameset(I) List
6. u = hd(J) ∈ Cname
7. ¬(J = [] ∈ (nameset(I) List))
8. x : nameset(I)
9. i : ℕ2
10. bx : open_box(cubical-nerve(cat(G));I;J;x;0)
11. ¬3 < ||bx||
12. K : Cname List
13. f : name-morph(I;K)
14. (f u) = hd(map(f;J)) ∈ Cname
15. ∀i:nameset(I). ((i ∈ J) ⇒ (↑isname(f i)))
16. ↑isname(f x)
17. ¬False
18. map(f;J) ∈ nameset(K) List
19. f x ∈ nameset(K)
20. nameset([x / J]) ⊆r name-morph-domain(f;I)
21. ¬↑null(J)
22. ¬↑null(map(f;J))
23. box : open_box(cubical-nerve(cat(G));K;map(f;J);f x;0)
24. ¬3 < ||box||
25. open_box_image(cubical-nerve(cat(G));I;K;f;bx) = box ∈ open_box(cubical-nerve(cat(G));K;map(f;J);f x;0)
26. ∀f1:name-morph(K;[]). (nerve_box_label(bx;(f o f1)) = nerve_box_label(box;f1) ∈ cat-ob(cat(G)))
27. ||bx|| = ||box|| ∈ ℤ
28. ||bx|| ≤ 3
29. (∀j'∈J.j' = hd(J) ∈ Cname)
30. ||box|| ≤ 3
31. (∀j'∈map(f;J).j' = hd(map(f;J)) ∈ Cname)
32. ∀f1:name-morph(K;[]). (nerve_box_label(bx;(f o f1)) = nerve_box_label(box;f1) ∈ cat-ob(cat(G)))
33. k : nameset(K)
34. f1 : {f:name-morph(K;[])| (f k) = 0 ∈ ℕ2}
35. (f o f1) x ≠ 0
36. f1 (f x) ≠ 0
37. hd(map(f;J)) ∈ nameset(map(f;J))
38. ∀i@0:nameset(I). ∀c:cat-ob(poset-cat(I)).
poset_functor_extend(cat(G);I;λc.nerve_box_label(bx;c);λy,c. nerve_box_edge1(G;bx;x;0;hd(J);c;y);c;flip(c;i@0))
= ((λy,c. nerve_box_edge1(G;bx;x;0;hd(J);c;y)) i@0 c)
∈ (cat-arrow(cat(G)) ((λc.nerve_box_label(bx;c)) c) ((λc.nerve_box_label(bx;c)) flip(c;i@0)))
supposing (c i@0) = 0 ∈ ℕ2
39. λi.((↑isname(f i)) ∧ ((f i) = k ∈ Cname)) ∈ nameset(I) ⟶ ℙ
40. i1 : ℕ||I||
41. (f u) = k ∈ Cname
42. u ∈ nameset(I)
43. ((f o f1) u) = 0 ∈ ℕ2
44. poset_functor_extend(cat(G);I;λc.nerve_box_label(bx;c);
λy,c. nerve_box_edge1(G;bx;x;0;hd(J);c;y);(f o f1);flip((f o f1);u))
= ((λy,c. nerve_box_edge1(G;bx;x;0;hd(J);c;y)) u (f o f1))
∈ (cat-arrow(cat(G)) ((λc.nerve_box_label(bx;c)) (f o f1)) ((λc.nerve_box_label(bx;c)) flip((f o f1);u)))
45. (f o flip(f1;k)) = flip((f o f1);u) ∈ name-morph(I;[])
46. I[i1] = u ∈ nameset(I)
47. ↑isname(f u)
48. f u ∈ nameset(K)
49. (f1 (f u)) = 0 ∈ ℕ2
50. ∀f1:name-morph(K;[]). ∀u:nameset(I).
((↑isname(f u))
⇒ ((f1 (f u)) = 0 ∈ ℕ2)
⇒ ((((f1 (f x)) = 0 ∈ ℤ) ∨ (¬((f u) = hd(map(f;J)) ∈ Cname)))
∧ ((((f o f1) x) = 0 ∈ ℤ) ∨ (¬(u = hd(J) ∈ Cname))))
⇒ (nerve_box_edge(box;f1;f u)
= nerve_box_edge(bx;(f o f1);u)
∈ (cat-arrow(cat(G)) nerve_box_label(bx;(f o f1)) nerve_box_label(bx;(f o flip(f1;f u))))))
51. (flip(f1;f x) (f x)) = 0 ∈ ℕ2
52. i = 0 ∈ ℤ
53. ¬(u = x ∈ Cname)
54. ¬((f u) = (f x) ∈ Cname)
55. groupoid-square1(G;nerve_box_label(box;flip(f1;f x));nerve_box_label(box;flip(flip(f1;f x);f u));
nerve_box_label(box;f1);nerve_box_label(box;flip(f1;f u));nerve_box_edge(box;flip(f1;f x);f u);
nerve_box_edge(box;flip(flip(f1;f x);f u);f x);nerve_box_edge(box;flip(f1;f x);f x))
= groupoid-square1(G;nerve_box_label(bx;flip((f o f1);x));nerve_box_label(bx;flip(flip((f o f1);x);u));
nerve_box_label(bx;(f o f1));nerve_box_label(bx;flip((f o f1);u));nerve_box_edge(bx;flip((f o f1);x);u);
nerve_box_edge(bx;flip(flip((f o f1);x);u);x);nerve_box_edge(bx;flip((f o f1);x);x))
∈ {d:cat-arrow(cat(G)) nerve_box_label(box;f1) nerve_box_label(box;flip(f1;f u))|
nerve_box_edge(box;flip(f1;f x);f u) o nerve_box_edge(box;flip(flip(f1;f x);f u);f x)
= nerve_box_edge(box;flip(f1;f x);f x) o d}
56. d : cat-arrow(cat(G)) nerve_box_label(box;f1) nerve_box_label(box;flip(f1;f u))
⊢ nerve_box_label(box;flip(f1;f x)) ∈ cat-ob(cat(G))
3
.....subterm..... T:t
3:n
1. G : Groupoid
2. True
3. I : Cname List
4. u : nameset(I)
5. J : nameset(I) List
6. u = hd(J) ∈ Cname
7. ¬(J = [] ∈ (nameset(I) List))
8. x : nameset(I)
9. i : ℕ2
10. bx : open_box(cubical-nerve(cat(G));I;J;x;0)
11. ¬3 < ||bx||
12. K : Cname List
13. f : name-morph(I;K)
14. (f u) = hd(map(f;J)) ∈ Cname
15. ∀i:nameset(I). ((i ∈ J) ⇒ (↑isname(f i)))
16. ↑isname(f x)
17. ¬False
18. map(f;J) ∈ nameset(K) List
19. f x ∈ nameset(K)
20. nameset([x / J]) ⊆r name-morph-domain(f;I)
21. ¬↑null(J)
22. ¬↑null(map(f;J))
23. box : open_box(cubical-nerve(cat(G));K;map(f;J);f x;0)
24. ¬3 < ||box||
25. open_box_image(cubical-nerve(cat(G));I;K;f;bx) = box ∈ open_box(cubical-nerve(cat(G));K;map(f;J);f x;0)
26. ∀f1:name-morph(K;[]). (nerve_box_label(bx;(f o f1)) = nerve_box_label(box;f1) ∈ cat-ob(cat(G)))
27. ||bx|| = ||box|| ∈ ℤ
28. ||bx|| ≤ 3
29. (∀j'∈J.j' = hd(J) ∈ Cname)
30. ||box|| ≤ 3
31. (∀j'∈map(f;J).j' = hd(map(f;J)) ∈ Cname)
32. ∀f1:name-morph(K;[]). (nerve_box_label(bx;(f o f1)) = nerve_box_label(box;f1) ∈ cat-ob(cat(G)))
33. k : nameset(K)
34. f1 : {f:name-morph(K;[])| (f k) = 0 ∈ ℕ2}
35. (f o f1) x ≠ 0
36. f1 (f x) ≠ 0
37. hd(map(f;J)) ∈ nameset(map(f;J))
38. ∀i@0:nameset(I). ∀c:cat-ob(poset-cat(I)).
poset_functor_extend(cat(G);I;λc.nerve_box_label(bx;c);λy,c. nerve_box_edge1(G;bx;x;0;hd(J);c;y);c;flip(c;i@0))
= ((λy,c. nerve_box_edge1(G;bx;x;0;hd(J);c;y)) i@0 c)
∈ (cat-arrow(cat(G)) ((λc.nerve_box_label(bx;c)) c) ((λc.nerve_box_label(bx;c)) flip(c;i@0)))
supposing (c i@0) = 0 ∈ ℕ2
39. λi.((↑isname(f i)) ∧ ((f i) = k ∈ Cname)) ∈ nameset(I) ⟶ ℙ
40. i1 : ℕ||I||
41. (f u) = k ∈ Cname
42. u ∈ nameset(I)
43. ((f o f1) u) = 0 ∈ ℕ2
44. poset_functor_extend(cat(G);I;λc.nerve_box_label(bx;c);
λy,c. nerve_box_edge1(G;bx;x;0;hd(J);c;y);(f o f1);flip((f o f1);u))
= ((λy,c. nerve_box_edge1(G;bx;x;0;hd(J);c;y)) u (f o f1))
∈ (cat-arrow(cat(G)) ((λc.nerve_box_label(bx;c)) (f o f1)) ((λc.nerve_box_label(bx;c)) flip((f o f1);u)))
45. (f o flip(f1;k)) = flip((f o f1);u) ∈ name-morph(I;[])
46. I[i1] = u ∈ nameset(I)
47. ↑isname(f u)
48. f u ∈ nameset(K)
49. (f1 (f u)) = 0 ∈ ℕ2
50. ∀f1:name-morph(K;[]). ∀u:nameset(I).
((↑isname(f u))
⇒ ((f1 (f u)) = 0 ∈ ℕ2)
⇒ ((((f1 (f x)) = 0 ∈ ℤ) ∨ (¬((f u) = hd(map(f;J)) ∈ Cname)))
∧ ((((f o f1) x) = 0 ∈ ℤ) ∨ (¬(u = hd(J) ∈ Cname))))
⇒ (nerve_box_edge(box;f1;f u)
= nerve_box_edge(bx;(f o f1);u)
∈ (cat-arrow(cat(G)) nerve_box_label(bx;(f o f1)) nerve_box_label(bx;(f o flip(f1;f u))))))
51. (flip(f1;f x) (f x)) = 0 ∈ ℕ2
52. i = 0 ∈ ℤ
53. ¬(u = x ∈ Cname)
54. ¬((f u) = (f x) ∈ Cname)
55. groupoid-square1(G;nerve_box_label(box;flip(f1;f x));nerve_box_label(box;flip(flip(f1;f x);f u));
nerve_box_label(box;f1);nerve_box_label(box;flip(f1;f u));nerve_box_edge(box;flip(f1;f x);f u);
nerve_box_edge(box;flip(flip(f1;f x);f u);f x);nerve_box_edge(box;flip(f1;f x);f x))
= groupoid-square1(G;nerve_box_label(bx;flip((f o f1);x));nerve_box_label(bx;flip(flip((f o f1);x);u));
nerve_box_label(bx;(f o f1));nerve_box_label(bx;flip((f o f1);u));nerve_box_edge(bx;flip((f o f1);x);u);
nerve_box_edge(bx;flip(flip((f o f1);x);u);x);nerve_box_edge(bx;flip((f o f1);x);x))
∈ {d:cat-arrow(cat(G)) nerve_box_label(box;f1) nerve_box_label(box;flip(f1;f u))|
nerve_box_edge(box;flip(f1;f x);f u) o nerve_box_edge(box;flip(flip(f1;f x);f u);f x)
= nerve_box_edge(box;flip(f1;f x);f x) o d}
56. d : cat-arrow(cat(G)) nerve_box_label(box;f1) nerve_box_label(box;flip(f1;f u))
⊢ nerve_box_label(box;flip(flip(f1;f x);f u)) ∈ cat-ob(cat(G))
4
.....subterm..... T:t
4:n
1. G : Groupoid
2. True
3. I : Cname List
4. u : nameset(I)
5. J : nameset(I) List
6. u = hd(J) ∈ Cname
7. ¬(J = [] ∈ (nameset(I) List))
8. x : nameset(I)
9. i : ℕ2
10. bx : open_box(cubical-nerve(cat(G));I;J;x;0)
11. ¬3 < ||bx||
12. K : Cname List
13. f : name-morph(I;K)
14. (f u) = hd(map(f;J)) ∈ Cname
15. ∀i:nameset(I). ((i ∈ J) ⇒ (↑isname(f i)))
16. ↑isname(f x)
17. ¬False
18. map(f;J) ∈ nameset(K) List
19. f x ∈ nameset(K)
20. nameset([x / J]) ⊆r name-morph-domain(f;I)
21. ¬↑null(J)
22. ¬↑null(map(f;J))
23. box : open_box(cubical-nerve(cat(G));K;map(f;J);f x;0)
24. ¬3 < ||box||
25. open_box_image(cubical-nerve(cat(G));I;K;f;bx) = box ∈ open_box(cubical-nerve(cat(G));K;map(f;J);f x;0)
26. ∀f1:name-morph(K;[]). (nerve_box_label(bx;(f o f1)) = nerve_box_label(box;f1) ∈ cat-ob(cat(G)))
27. ||bx|| = ||box|| ∈ ℤ
28. ||bx|| ≤ 3
29. (∀j'∈J.j' = hd(J) ∈ Cname)
30. ||box|| ≤ 3
31. (∀j'∈map(f;J).j' = hd(map(f;J)) ∈ Cname)
32. ∀f1:name-morph(K;[]). (nerve_box_label(bx;(f o f1)) = nerve_box_label(box;f1) ∈ cat-ob(cat(G)))
33. k : nameset(K)
34. f1 : {f:name-morph(K;[])| (f k) = 0 ∈ ℕ2}
35. (f o f1) x ≠ 0
36. f1 (f x) ≠ 0
37. hd(map(f;J)) ∈ nameset(map(f;J))
38. ∀i@0:nameset(I). ∀c:cat-ob(poset-cat(I)).
poset_functor_extend(cat(G);I;λc.nerve_box_label(bx;c);λy,c. nerve_box_edge1(G;bx;x;0;hd(J);c;y);c;flip(c;i@0))
= ((λy,c. nerve_box_edge1(G;bx;x;0;hd(J);c;y)) i@0 c)
∈ (cat-arrow(cat(G)) ((λc.nerve_box_label(bx;c)) c) ((λc.nerve_box_label(bx;c)) flip(c;i@0)))
supposing (c i@0) = 0 ∈ ℕ2
39. λi.((↑isname(f i)) ∧ ((f i) = k ∈ Cname)) ∈ nameset(I) ⟶ ℙ
40. i1 : ℕ||I||
41. (f u) = k ∈ Cname
42. u ∈ nameset(I)
43. ((f o f1) u) = 0 ∈ ℕ2
44. poset_functor_extend(cat(G);I;λc.nerve_box_label(bx;c);
λy,c. nerve_box_edge1(G;bx;x;0;hd(J);c;y);(f o f1);flip((f o f1);u))
= ((λy,c. nerve_box_edge1(G;bx;x;0;hd(J);c;y)) u (f o f1))
∈ (cat-arrow(cat(G)) ((λc.nerve_box_label(bx;c)) (f o f1)) ((λc.nerve_box_label(bx;c)) flip((f o f1);u)))
45. (f o flip(f1;k)) = flip((f o f1);u) ∈ name-morph(I;[])
46. I[i1] = u ∈ nameset(I)
47. ↑isname(f u)
48. f u ∈ nameset(K)
49. (f1 (f u)) = 0 ∈ ℕ2
50. ∀f1:name-morph(K;[]). ∀u:nameset(I).
((↑isname(f u))
⇒ ((f1 (f u)) = 0 ∈ ℕ2)
⇒ ((((f1 (f x)) = 0 ∈ ℤ) ∨ (¬((f u) = hd(map(f;J)) ∈ Cname)))
∧ ((((f o f1) x) = 0 ∈ ℤ) ∨ (¬(u = hd(J) ∈ Cname))))
⇒ (nerve_box_edge(box;f1;f u)
= nerve_box_edge(bx;(f o f1);u)
∈ (cat-arrow(cat(G)) nerve_box_label(bx;(f o f1)) nerve_box_label(bx;(f o flip(f1;f u))))))
51. (flip(f1;f x) (f x)) = 0 ∈ ℕ2
52. i = 0 ∈ ℤ
53. ¬(u = x ∈ Cname)
54. ¬((f u) = (f x) ∈ Cname)
55. groupoid-square1(G;nerve_box_label(box;flip(f1;f x));nerve_box_label(box;flip(flip(f1;f x);f u));
nerve_box_label(box;f1);nerve_box_label(box;flip(f1;f u));nerve_box_edge(box;flip(f1;f x);f u);
nerve_box_edge(box;flip(flip(f1;f x);f u);f x);nerve_box_edge(box;flip(f1;f x);f x))
= groupoid-square1(G;nerve_box_label(bx;flip((f o f1);x));nerve_box_label(bx;flip(flip((f o f1);x);u));
nerve_box_label(bx;(f o f1));nerve_box_label(bx;flip((f o f1);u));nerve_box_edge(bx;flip((f o f1);x);u);
nerve_box_edge(bx;flip(flip((f o f1);x);u);x);nerve_box_edge(bx;flip((f o f1);x);x))
∈ {d:cat-arrow(cat(G)) nerve_box_label(box;f1) nerve_box_label(box;flip(f1;f u))|
nerve_box_edge(box;flip(f1;f x);f u) o nerve_box_edge(box;flip(flip(f1;f x);f u);f x)
= nerve_box_edge(box;flip(f1;f x);f x) o d}
56. d : cat-arrow(cat(G)) nerve_box_label(box;f1) nerve_box_label(box;flip(f1;f u))
⊢ nerve_box_label(box;f1) ∈ cat-ob(cat(G))
5
.....subterm..... T:t
5:n
1. G : Groupoid
2. True
3. I : Cname List
4. u : nameset(I)
5. J : nameset(I) List
6. u = hd(J) ∈ Cname
7. ¬(J = [] ∈ (nameset(I) List))
8. x : nameset(I)
9. i : ℕ2
10. bx : open_box(cubical-nerve(cat(G));I;J;x;0)
11. ¬3 < ||bx||
12. K : Cname List
13. f : name-morph(I;K)
14. (f u) = hd(map(f;J)) ∈ Cname
15. ∀i:nameset(I). ((i ∈ J) ⇒ (↑isname(f i)))
16. ↑isname(f x)
17. ¬False
18. map(f;J) ∈ nameset(K) List
19. f x ∈ nameset(K)
20. nameset([x / J]) ⊆r name-morph-domain(f;I)
21. ¬↑null(J)
22. ¬↑null(map(f;J))
23. box : open_box(cubical-nerve(cat(G));K;map(f;J);f x;0)
24. ¬3 < ||box||
25. open_box_image(cubical-nerve(cat(G));I;K;f;bx) = box ∈ open_box(cubical-nerve(cat(G));K;map(f;J);f x;0)
26. ∀f1:name-morph(K;[]). (nerve_box_label(bx;(f o f1)) = nerve_box_label(box;f1) ∈ cat-ob(cat(G)))
27. ||bx|| = ||box|| ∈ ℤ
28. ||bx|| ≤ 3
29. (∀j'∈J.j' = hd(J) ∈ Cname)
30. ||box|| ≤ 3
31. (∀j'∈map(f;J).j' = hd(map(f;J)) ∈ Cname)
32. ∀f1:name-morph(K;[]). (nerve_box_label(bx;(f o f1)) = nerve_box_label(box;f1) ∈ cat-ob(cat(G)))
33. k : nameset(K)
34. f1 : {f:name-morph(K;[])| (f k) = 0 ∈ ℕ2}
35. (f o f1) x ≠ 0
36. f1 (f x) ≠ 0
37. hd(map(f;J)) ∈ nameset(map(f;J))
38. ∀i@0:nameset(I). ∀c:cat-ob(poset-cat(I)).
poset_functor_extend(cat(G);I;λc.nerve_box_label(bx;c);λy,c. nerve_box_edge1(G;bx;x;0;hd(J);c;y);c;flip(c;i@0))
= ((λy,c. nerve_box_edge1(G;bx;x;0;hd(J);c;y)) i@0 c)
∈ (cat-arrow(cat(G)) ((λc.nerve_box_label(bx;c)) c) ((λc.nerve_box_label(bx;c)) flip(c;i@0)))
supposing (c i@0) = 0 ∈ ℕ2
39. λi.((↑isname(f i)) ∧ ((f i) = k ∈ Cname)) ∈ nameset(I) ⟶ ℙ
40. i1 : ℕ||I||
41. (f u) = k ∈ Cname
42. u ∈ nameset(I)
43. ((f o f1) u) = 0 ∈ ℕ2
44. poset_functor_extend(cat(G);I;λc.nerve_box_label(bx;c);
λy,c. nerve_box_edge1(G;bx;x;0;hd(J);c;y);(f o f1);flip((f o f1);u))
= ((λy,c. nerve_box_edge1(G;bx;x;0;hd(J);c;y)) u (f o f1))
∈ (cat-arrow(cat(G)) ((λc.nerve_box_label(bx;c)) (f o f1)) ((λc.nerve_box_label(bx;c)) flip((f o f1);u)))
45. (f o flip(f1;k)) = flip((f o f1);u) ∈ name-morph(I;[])
46. I[i1] = u ∈ nameset(I)
47. ↑isname(f u)
48. f u ∈ nameset(K)
49. (f1 (f u)) = 0 ∈ ℕ2
50. ∀f1:name-morph(K;[]). ∀u:nameset(I).
((↑isname(f u))
⇒ ((f1 (f u)) = 0 ∈ ℕ2)
⇒ ((((f1 (f x)) = 0 ∈ ℤ) ∨ (¬((f u) = hd(map(f;J)) ∈ Cname)))
∧ ((((f o f1) x) = 0 ∈ ℤ) ∨ (¬(u = hd(J) ∈ Cname))))
⇒ (nerve_box_edge(box;f1;f u)
= nerve_box_edge(bx;(f o f1);u)
∈ (cat-arrow(cat(G)) nerve_box_label(bx;(f o f1)) nerve_box_label(bx;(f o flip(f1;f u))))))
51. (flip(f1;f x) (f x)) = 0 ∈ ℕ2
52. i = 0 ∈ ℤ
53. ¬(u = x ∈ Cname)
54. ¬((f u) = (f x) ∈ Cname)
55. groupoid-square1(G;nerve_box_label(box;flip(f1;f x));nerve_box_label(box;flip(flip(f1;f x);f u));
nerve_box_label(box;f1);nerve_box_label(box;flip(f1;f u));nerve_box_edge(box;flip(f1;f x);f u);
nerve_box_edge(box;flip(flip(f1;f x);f u);f x);nerve_box_edge(box;flip(f1;f x);f x))
= groupoid-square1(G;nerve_box_label(bx;flip((f o f1);x));nerve_box_label(bx;flip(flip((f o f1);x);u));
nerve_box_label(bx;(f o f1));nerve_box_label(bx;flip((f o f1);u));nerve_box_edge(bx;flip((f o f1);x);u);
nerve_box_edge(bx;flip(flip((f o f1);x);u);x);nerve_box_edge(bx;flip((f o f1);x);x))
∈ {d:cat-arrow(cat(G)) nerve_box_label(box;f1) nerve_box_label(box;flip(f1;f u))|
nerve_box_edge(box;flip(f1;f x);f u) o nerve_box_edge(box;flip(flip(f1;f x);f u);f x)
= nerve_box_edge(box;flip(f1;f x);f x) o d}
56. d : cat-arrow(cat(G)) nerve_box_label(box;f1) nerve_box_label(box;flip(f1;f u))
⊢ nerve_box_label(box;flip(f1;f u)) ∈ cat-ob(cat(G))
6
.....subterm..... T:t
6:n
1. G : Groupoid
2. True
3. I : Cname List
4. u : nameset(I)
5. J : nameset(I) List
6. u = hd(J) ∈ Cname
7. ¬(J = [] ∈ (nameset(I) List))
8. x : nameset(I)
9. i : ℕ2
10. bx : open_box(cubical-nerve(cat(G));I;J;x;0)
11. ¬3 < ||bx||
12. K : Cname List
13. f : name-morph(I;K)
14. (f u) = hd(map(f;J)) ∈ Cname
15. ∀i:nameset(I). ((i ∈ J) ⇒ (↑isname(f i)))
16. ↑isname(f x)
17. ¬False
18. map(f;J) ∈ nameset(K) List
19. f x ∈ nameset(K)
20. nameset([x / J]) ⊆r name-morph-domain(f;I)
21. ¬↑null(J)
22. ¬↑null(map(f;J))
23. box : open_box(cubical-nerve(cat(G));K;map(f;J);f x;0)
24. ¬3 < ||box||
25. open_box_image(cubical-nerve(cat(G));I;K;f;bx) = box ∈ open_box(cubical-nerve(cat(G));K;map(f;J);f x;0)
26. ∀f1:name-morph(K;[]). (nerve_box_label(bx;(f o f1)) = nerve_box_label(box;f1) ∈ cat-ob(cat(G)))
27. ||bx|| = ||box|| ∈ ℤ
28. ||bx|| ≤ 3
29. (∀j'∈J.j' = hd(J) ∈ Cname)
30. ||box|| ≤ 3
31. (∀j'∈map(f;J).j' = hd(map(f;J)) ∈ Cname)
32. ∀f1:name-morph(K;[]). (nerve_box_label(bx;(f o f1)) = nerve_box_label(box;f1) ∈ cat-ob(cat(G)))
33. k : nameset(K)
34. f1 : {f:name-morph(K;[])| (f k) = 0 ∈ ℕ2}
35. (f o f1) x ≠ 0
36. f1 (f x) ≠ 0
37. hd(map(f;J)) ∈ nameset(map(f;J))
38. ∀i@0:nameset(I). ∀c:cat-ob(poset-cat(I)).
poset_functor_extend(cat(G);I;λc.nerve_box_label(bx;c);λy,c. nerve_box_edge1(G;bx;x;0;hd(J);c;y);c;flip(c;i@0))
= ((λy,c. nerve_box_edge1(G;bx;x;0;hd(J);c;y)) i@0 c)
∈ (cat-arrow(cat(G)) ((λc.nerve_box_label(bx;c)) c) ((λc.nerve_box_label(bx;c)) flip(c;i@0)))
supposing (c i@0) = 0 ∈ ℕ2
39. λi.((↑isname(f i)) ∧ ((f i) = k ∈ Cname)) ∈ nameset(I) ⟶ ℙ
40. i1 : ℕ||I||
41. (f u) = k ∈ Cname
42. u ∈ nameset(I)
43. ((f o f1) u) = 0 ∈ ℕ2
44. poset_functor_extend(cat(G);I;λc.nerve_box_label(bx;c);
λy,c. nerve_box_edge1(G;bx;x;0;hd(J);c;y);(f o f1);flip((f o f1);u))
= ((λy,c. nerve_box_edge1(G;bx;x;0;hd(J);c;y)) u (f o f1))
∈ (cat-arrow(cat(G)) ((λc.nerve_box_label(bx;c)) (f o f1)) ((λc.nerve_box_label(bx;c)) flip((f o f1);u)))
45. (f o flip(f1;k)) = flip((f o f1);u) ∈ name-morph(I;[])
46. I[i1] = u ∈ nameset(I)
47. ↑isname(f u)
48. f u ∈ nameset(K)
49. (f1 (f u)) = 0 ∈ ℕ2
50. ∀f1:name-morph(K;[]). ∀u:nameset(I).
((↑isname(f u))
⇒ ((f1 (f u)) = 0 ∈ ℕ2)
⇒ ((((f1 (f x)) = 0 ∈ ℤ) ∨ (¬((f u) = hd(map(f;J)) ∈ Cname)))
∧ ((((f o f1) x) = 0 ∈ ℤ) ∨ (¬(u = hd(J) ∈ Cname))))
⇒ (nerve_box_edge(box;f1;f u)
= nerve_box_edge(bx;(f o f1);u)
∈ (cat-arrow(cat(G)) nerve_box_label(bx;(f o f1)) nerve_box_label(bx;(f o flip(f1;f u))))))
51. (flip(f1;f x) (f x)) = 0 ∈ ℕ2
52. i = 0 ∈ ℤ
53. ¬(u = x ∈ Cname)
54. ¬((f u) = (f x) ∈ Cname)
55. groupoid-square1(G;nerve_box_label(box;flip(f1;f x));nerve_box_label(box;flip(flip(f1;f x);f u));
nerve_box_label(box;f1);nerve_box_label(box;flip(f1;f u));nerve_box_edge(box;flip(f1;f x);f u);
nerve_box_edge(box;flip(flip(f1;f x);f u);f x);nerve_box_edge(box;flip(f1;f x);f x))
= groupoid-square1(G;nerve_box_label(bx;flip((f o f1);x));nerve_box_label(bx;flip(flip((f o f1);x);u));
nerve_box_label(bx;(f o f1));nerve_box_label(bx;flip((f o f1);u));nerve_box_edge(bx;flip((f o f1);x);u);
nerve_box_edge(bx;flip(flip((f o f1);x);u);x);nerve_box_edge(bx;flip((f o f1);x);x))
∈ {d:cat-arrow(cat(G)) nerve_box_label(box;f1) nerve_box_label(box;flip(f1;f u))|
nerve_box_edge(box;flip(f1;f x);f u) o nerve_box_edge(box;flip(flip(f1;f x);f u);f x)
= nerve_box_edge(box;flip(f1;f x);f x) o d}
56. d : cat-arrow(cat(G)) nerve_box_label(box;f1) nerve_box_label(box;flip(f1;f u))
⊢ nerve_box_edge(box;flip(f1;f x);f u) ∈ cat-arrow(cat(G)) nerve_box_label(box;flip(f1;f x))
nerve_box_label(box;flip(flip(f1;f x);f u))
7
.....subterm..... T:t
7:n
1. G : Groupoid
2. True
3. I : Cname List
4. u : nameset(I)
5. J : nameset(I) List
6. u = hd(J) ∈ Cname
7. ¬(J = [] ∈ (nameset(I) List))
8. x : nameset(I)
9. i : ℕ2
10. bx : open_box(cubical-nerve(cat(G));I;J;x;0)
11. ¬3 < ||bx||
12. K : Cname List
13. f : name-morph(I;K)
14. (f u) = hd(map(f;J)) ∈ Cname
15. ∀i:nameset(I). ((i ∈ J) ⇒ (↑isname(f i)))
16. ↑isname(f x)
17. ¬False
18. map(f;J) ∈ nameset(K) List
19. f x ∈ nameset(K)
20. nameset([x / J]) ⊆r name-morph-domain(f;I)
21. ¬↑null(J)
22. ¬↑null(map(f;J))
23. box : open_box(cubical-nerve(cat(G));K;map(f;J);f x;0)
24. ¬3 < ||box||
25. open_box_image(cubical-nerve(cat(G));I;K;f;bx) = box ∈ open_box(cubical-nerve(cat(G));K;map(f;J);f x;0)
26. ∀f1:name-morph(K;[]). (nerve_box_label(bx;(f o f1)) = nerve_box_label(box;f1) ∈ cat-ob(cat(G)))
27. ||bx|| = ||box|| ∈ ℤ
28. ||bx|| ≤ 3
29. (∀j'∈J.j' = hd(J) ∈ Cname)
30. ||box|| ≤ 3
31. (∀j'∈map(f;J).j' = hd(map(f;J)) ∈ Cname)
32. ∀f1:name-morph(K;[]). (nerve_box_label(bx;(f o f1)) = nerve_box_label(box;f1) ∈ cat-ob(cat(G)))
33. k : nameset(K)
34. f1 : {f:name-morph(K;[])| (f k) = 0 ∈ ℕ2}
35. (f o f1) x ≠ 0
36. f1 (f x) ≠ 0
37. hd(map(f;J)) ∈ nameset(map(f;J))
38. ∀i@0:nameset(I). ∀c:cat-ob(poset-cat(I)).
poset_functor_extend(cat(G);I;λc.nerve_box_label(bx;c);λy,c. nerve_box_edge1(G;bx;x;0;hd(J);c;y);c;flip(c;i@0))
= ((λy,c. nerve_box_edge1(G;bx;x;0;hd(J);c;y)) i@0 c)
∈ (cat-arrow(cat(G)) ((λc.nerve_box_label(bx;c)) c) ((λc.nerve_box_label(bx;c)) flip(c;i@0)))
supposing (c i@0) = 0 ∈ ℕ2
39. λi.((↑isname(f i)) ∧ ((f i) = k ∈ Cname)) ∈ nameset(I) ⟶ ℙ
40. i1 : ℕ||I||
41. (f u) = k ∈ Cname
42. u ∈ nameset(I)
43. ((f o f1) u) = 0 ∈ ℕ2
44. poset_functor_extend(cat(G);I;λc.nerve_box_label(bx;c);
λy,c. nerve_box_edge1(G;bx;x;0;hd(J);c;y);(f o f1);flip((f o f1);u))
= ((λy,c. nerve_box_edge1(G;bx;x;0;hd(J);c;y)) u (f o f1))
∈ (cat-arrow(cat(G)) ((λc.nerve_box_label(bx;c)) (f o f1)) ((λc.nerve_box_label(bx;c)) flip((f o f1);u)))
45. (f o flip(f1;k)) = flip((f o f1);u) ∈ name-morph(I;[])
46. I[i1] = u ∈ nameset(I)
47. ↑isname(f u)
48. f u ∈ nameset(K)
49. (f1 (f u)) = 0 ∈ ℕ2
50. ∀f1:name-morph(K;[]). ∀u:nameset(I).
((↑isname(f u))
⇒ ((f1 (f u)) = 0 ∈ ℕ2)
⇒ ((((f1 (f x)) = 0 ∈ ℤ) ∨ (¬((f u) = hd(map(f;J)) ∈ Cname)))
∧ ((((f o f1) x) = 0 ∈ ℤ) ∨ (¬(u = hd(J) ∈ Cname))))
⇒ (nerve_box_edge(box;f1;f u)
= nerve_box_edge(bx;(f o f1);u)
∈ (cat-arrow(cat(G)) nerve_box_label(bx;(f o f1)) nerve_box_label(bx;(f o flip(f1;f u))))))
51. (flip(f1;f x) (f x)) = 0 ∈ ℕ2
52. i = 0 ∈ ℤ
53. ¬(u = x ∈ Cname)
54. ¬((f u) = (f x) ∈ Cname)
55. groupoid-square1(G;nerve_box_label(box;flip(f1;f x));nerve_box_label(box;flip(flip(f1;f x);f u));
nerve_box_label(box;f1);nerve_box_label(box;flip(f1;f u));nerve_box_edge(box;flip(f1;f x);f u);
nerve_box_edge(box;flip(flip(f1;f x);f u);f x);nerve_box_edge(box;flip(f1;f x);f x))
= groupoid-square1(G;nerve_box_label(bx;flip((f o f1);x));nerve_box_label(bx;flip(flip((f o f1);x);u));
nerve_box_label(bx;(f o f1));nerve_box_label(bx;flip((f o f1);u));nerve_box_edge(bx;flip((f o f1);x);u);
nerve_box_edge(bx;flip(flip((f o f1);x);u);x);nerve_box_edge(bx;flip((f o f1);x);x))
∈ {d:cat-arrow(cat(G)) nerve_box_label(box;f1) nerve_box_label(box;flip(f1;f u))|
nerve_box_edge(box;flip(f1;f x);f u) o nerve_box_edge(box;flip(flip(f1;f x);f u);f x)
= nerve_box_edge(box;flip(f1;f x);f x) o d}
56. d : cat-arrow(cat(G)) nerve_box_label(box;f1) nerve_box_label(box;flip(f1;f u))
⊢ nerve_box_edge(box;flip(flip(f1;f x);f u);f x) ∈ cat-arrow(cat(G)) nerve_box_label(box;flip(flip(f1;f x);f u))
nerve_box_label(box;flip(f1;f u))
8
.....subterm..... T:t
8:n
1. G : Groupoid
2. True
3. I : Cname List
4. u : nameset(I)
5. J : nameset(I) List
6. u = hd(J) ∈ Cname
7. ¬(J = [] ∈ (nameset(I) List))
8. x : nameset(I)
9. i : ℕ2
10. bx : open_box(cubical-nerve(cat(G));I;J;x;0)
11. ¬3 < ||bx||
12. K : Cname List
13. f : name-morph(I;K)
14. (f u) = hd(map(f;J)) ∈ Cname
15. ∀i:nameset(I). ((i ∈ J) ⇒ (↑isname(f i)))
16. ↑isname(f x)
17. ¬False
18. map(f;J) ∈ nameset(K) List
19. f x ∈ nameset(K)
20. nameset([x / J]) ⊆r name-morph-domain(f;I)
21. ¬↑null(J)
22. ¬↑null(map(f;J))
23. box : open_box(cubical-nerve(cat(G));K;map(f;J);f x;0)
24. ¬3 < ||box||
25. open_box_image(cubical-nerve(cat(G));I;K;f;bx) = box ∈ open_box(cubical-nerve(cat(G));K;map(f;J);f x;0)
26. ∀f1:name-morph(K;[]). (nerve_box_label(bx;(f o f1)) = nerve_box_label(box;f1) ∈ cat-ob(cat(G)))
27. ||bx|| = ||box|| ∈ ℤ
28. ||bx|| ≤ 3
29. (∀j'∈J.j' = hd(J) ∈ Cname)
30. ||box|| ≤ 3
31. (∀j'∈map(f;J).j' = hd(map(f;J)) ∈ Cname)
32. ∀f1:name-morph(K;[]). (nerve_box_label(bx;(f o f1)) = nerve_box_label(box;f1) ∈ cat-ob(cat(G)))
33. k : nameset(K)
34. f1 : {f:name-morph(K;[])| (f k) = 0 ∈ ℕ2}
35. (f o f1) x ≠ 0
36. f1 (f x) ≠ 0
37. hd(map(f;J)) ∈ nameset(map(f;J))
38. ∀i@0:nameset(I). ∀c:cat-ob(poset-cat(I)).
poset_functor_extend(cat(G);I;λc.nerve_box_label(bx;c);λy,c. nerve_box_edge1(G;bx;x;0;hd(J);c;y);c;flip(c;i@0))
= ((λy,c. nerve_box_edge1(G;bx;x;0;hd(J);c;y)) i@0 c)
∈ (cat-arrow(cat(G)) ((λc.nerve_box_label(bx;c)) c) ((λc.nerve_box_label(bx;c)) flip(c;i@0)))
supposing (c i@0) = 0 ∈ ℕ2
39. λi.((↑isname(f i)) ∧ ((f i) = k ∈ Cname)) ∈ nameset(I) ⟶ ℙ
40. i1 : ℕ||I||
41. (f u) = k ∈ Cname
42. u ∈ nameset(I)
43. ((f o f1) u) = 0 ∈ ℕ2
44. poset_functor_extend(cat(G);I;λc.nerve_box_label(bx;c);
λy,c. nerve_box_edge1(G;bx;x;0;hd(J);c;y);(f o f1);flip((f o f1);u))
= ((λy,c. nerve_box_edge1(G;bx;x;0;hd(J);c;y)) u (f o f1))
∈ (cat-arrow(cat(G)) ((λc.nerve_box_label(bx;c)) (f o f1)) ((λc.nerve_box_label(bx;c)) flip((f o f1);u)))
45. (f o flip(f1;k)) = flip((f o f1);u) ∈ name-morph(I;[])
46. I[i1] = u ∈ nameset(I)
47. ↑isname(f u)
48. f u ∈ nameset(K)
49. (f1 (f u)) = 0 ∈ ℕ2
50. ∀f1:name-morph(K;[]). ∀u:nameset(I).
((↑isname(f u))
⇒ ((f1 (f u)) = 0 ∈ ℕ2)
⇒ ((((f1 (f x)) = 0 ∈ ℤ) ∨ (¬((f u) = hd(map(f;J)) ∈ Cname)))
∧ ((((f o f1) x) = 0 ∈ ℤ) ∨ (¬(u = hd(J) ∈ Cname))))
⇒ (nerve_box_edge(box;f1;f u)
= nerve_box_edge(bx;(f o f1);u)
∈ (cat-arrow(cat(G)) nerve_box_label(bx;(f o f1)) nerve_box_label(bx;(f o flip(f1;f u))))))
51. (flip(f1;f x) (f x)) = 0 ∈ ℕ2
52. i = 0 ∈ ℤ
53. ¬(u = x ∈ Cname)
54. ¬((f u) = (f x) ∈ Cname)
55. groupoid-square1(G;nerve_box_label(box;flip(f1;f x));nerve_box_label(box;flip(flip(f1;f x);f u));
nerve_box_label(box;f1);nerve_box_label(box;flip(f1;f u));nerve_box_edge(box;flip(f1;f x);f u);
nerve_box_edge(box;flip(flip(f1;f x);f u);f x);nerve_box_edge(box;flip(f1;f x);f x))
= groupoid-square1(G;nerve_box_label(bx;flip((f o f1);x));nerve_box_label(bx;flip(flip((f o f1);x);u));
nerve_box_label(bx;(f o f1));nerve_box_label(bx;flip((f o f1);u));nerve_box_edge(bx;flip((f o f1);x);u);
nerve_box_edge(bx;flip(flip((f o f1);x);u);x);nerve_box_edge(bx;flip((f o f1);x);x))
∈ {d:cat-arrow(cat(G)) nerve_box_label(box;f1) nerve_box_label(box;flip(f1;f u))|
nerve_box_edge(box;flip(f1;f x);f u) o nerve_box_edge(box;flip(flip(f1;f x);f u);f x)
= nerve_box_edge(box;flip(f1;f x);f x) o d}
56. d : cat-arrow(cat(G)) nerve_box_label(box;f1) nerve_box_label(box;flip(f1;f u))
⊢ nerve_box_edge(box;flip(f1;f x);f x) ∈ cat-arrow(cat(G)) nerve_box_label(box;flip(f1;f x)) nerve_box_label(box;f1)
9
.....subterm..... T:t
9:n
1. G : Groupoid
2. True
3. I : Cname List
4. u : nameset(I)
5. J : nameset(I) List
6. u = hd(J) ∈ Cname
7. ¬(J = [] ∈ (nameset(I) List))
8. x : nameset(I)
9. i : ℕ2
10. bx : open_box(cubical-nerve(cat(G));I;J;x;0)
11. ¬3 < ||bx||
12. K : Cname List
13. f : name-morph(I;K)
14. (f u) = hd(map(f;J)) ∈ Cname
15. ∀i:nameset(I). ((i ∈ J) ⇒ (↑isname(f i)))
16. ↑isname(f x)
17. ¬False
18. map(f;J) ∈ nameset(K) List
19. f x ∈ nameset(K)
20. nameset([x / J]) ⊆r name-morph-domain(f;I)
21. ¬↑null(J)
22. ¬↑null(map(f;J))
23. box : open_box(cubical-nerve(cat(G));K;map(f;J);f x;0)
24. ¬3 < ||box||
25. open_box_image(cubical-nerve(cat(G));I;K;f;bx) = box ∈ open_box(cubical-nerve(cat(G));K;map(f;J);f x;0)
26. ∀f1:name-morph(K;[]). (nerve_box_label(bx;(f o f1)) = nerve_box_label(box;f1) ∈ cat-ob(cat(G)))
27. ||bx|| = ||box|| ∈ ℤ
28. ||bx|| ≤ 3
29. (∀j'∈J.j' = hd(J) ∈ Cname)
30. ||box|| ≤ 3
31. (∀j'∈map(f;J).j' = hd(map(f;J)) ∈ Cname)
32. ∀f1:name-morph(K;[]). (nerve_box_label(bx;(f o f1)) = nerve_box_label(box;f1) ∈ cat-ob(cat(G)))
33. k : nameset(K)
34. f1 : {f:name-morph(K;[])| (f k) = 0 ∈ ℕ2}
35. (f o f1) x ≠ 0
36. f1 (f x) ≠ 0
37. hd(map(f;J)) ∈ nameset(map(f;J))
38. ∀i@0:nameset(I). ∀c:cat-ob(poset-cat(I)).
poset_functor_extend(cat(G);I;λc.nerve_box_label(bx;c);λy,c. nerve_box_edge1(G;bx;x;0;hd(J);c;y);c;flip(c;i@0))
= ((λy,c. nerve_box_edge1(G;bx;x;0;hd(J);c;y)) i@0 c)
∈ (cat-arrow(cat(G)) ((λc.nerve_box_label(bx;c)) c) ((λc.nerve_box_label(bx;c)) flip(c;i@0)))
supposing (c i@0) = 0 ∈ ℕ2
39. λi.((↑isname(f i)) ∧ ((f i) = k ∈ Cname)) ∈ nameset(I) ⟶ ℙ
40. i1 : ℕ||I||
41. (f u) = k ∈ Cname
42. u ∈ nameset(I)
43. ((f o f1) u) = 0 ∈ ℕ2
44. poset_functor_extend(cat(G);I;λc.nerve_box_label(bx;c);
λy,c. nerve_box_edge1(G;bx;x;0;hd(J);c;y);(f o f1);flip((f o f1);u))
= ((λy,c. nerve_box_edge1(G;bx;x;0;hd(J);c;y)) u (f o f1))
∈ (cat-arrow(cat(G)) ((λc.nerve_box_label(bx;c)) (f o f1)) ((λc.nerve_box_label(bx;c)) flip((f o f1);u)))
45. (f o flip(f1;k)) = flip((f o f1);u) ∈ name-morph(I;[])
46. I[i1] = u ∈ nameset(I)
47. ↑isname(f u)
48. f u ∈ nameset(K)
49. (f1 (f u)) = 0 ∈ ℕ2
50. ∀f1:name-morph(K;[]). ∀u:nameset(I).
((↑isname(f u))
⇒ ((f1 (f u)) = 0 ∈ ℕ2)
⇒ ((((f1 (f x)) = 0 ∈ ℤ) ∨ (¬((f u) = hd(map(f;J)) ∈ Cname)))
∧ ((((f o f1) x) = 0 ∈ ℤ) ∨ (¬(u = hd(J) ∈ Cname))))
⇒ (nerve_box_edge(box;f1;f u)
= nerve_box_edge(bx;(f o f1);u)
∈ (cat-arrow(cat(G)) nerve_box_label(bx;(f o f1)) nerve_box_label(bx;(f o flip(f1;f u))))))
51. (flip(f1;f x) (f x)) = 0 ∈ ℕ2
52. i = 0 ∈ ℤ
53. ¬(u = x ∈ Cname)
54. ¬((f u) = (f x) ∈ Cname)
55. groupoid-square1(G;nerve_box_label(box;flip(f1;f x));nerve_box_label(box;flip(flip(f1;f x);f u));
nerve_box_label(box;f1);nerve_box_label(box;flip(f1;f u));nerve_box_edge(box;flip(f1;f x);f u);
nerve_box_edge(box;flip(flip(f1;f x);f u);f x);nerve_box_edge(box;flip(f1;f x);f x))
= groupoid-square1(G;nerve_box_label(bx;flip((f o f1);x));nerve_box_label(bx;flip(flip((f o f1);x);u));
nerve_box_label(bx;(f o f1));nerve_box_label(bx;flip((f o f1);u));nerve_box_edge(bx;flip((f o f1);x);u);
nerve_box_edge(bx;flip(flip((f o f1);x);u);x);nerve_box_edge(bx;flip((f o f1);x);x))
∈ {d:cat-arrow(cat(G)) nerve_box_label(box;f1) nerve_box_label(box;flip(f1;f u))|
nerve_box_edge(box;flip(f1;f x);f u) o nerve_box_edge(box;flip(flip(f1;f x);f u);f x)
= nerve_box_edge(box;flip(f1;f x);f x) o d}
56. d : cat-arrow(cat(G)) nerve_box_label(box;f1) nerve_box_label(box;flip(f1;f u))
⊢ d ∈ cat-arrow(cat(G)) nerve_box_label(box;f1) nerve_box_label(box;flip(f1;f u))
Latex:
Latex:
1. G : Groupoid
2. True
3. I : Cname List
4. u : nameset(I)
5. J : nameset(I) List
6. u = hd(J)
7. \mneg{}(J = [])
8. x : nameset(I)
9. i : \mBbbN{}2
10. bx : open\_box(cubical-nerve(cat(G));I;J;x;0)
11. \mneg{}3 < ||bx||
12. K : Cname List
13. f : name-morph(I;K)
14. (f u) = hd(map(f;J))
15. \mforall{}i:nameset(I). ((i \mmember{} J) {}\mRightarrow{} (\muparrow{}isname(f i)))
16. \muparrow{}isname(f x)
17. \mneg{}False
18. map(f;J) \mmember{} nameset(K) List
19. f x \mmember{} nameset(K)
20. nameset([x / J]) \msubseteq{}r name-morph-domain(f;I)
21. \mneg{}\muparrow{}null(J)
22. \mneg{}\muparrow{}null(map(f;J))
23. box : open\_box(cubical-nerve(cat(G));K;map(f;J);f x;0)
24. \mneg{}3 < ||box||
25. open\_box\_image(cubical-nerve(cat(G));I;K;f;bx) = box
26. \mforall{}f1:name-morph(K;[]). (nerve\_box\_label(bx;(f o f1)) = nerve\_box\_label(box;f1))
27. ||bx|| = ||box||
28. ||bx|| \mleq{} 3
29. (\mforall{}j'\mmember{}J.j' = hd(J))
30. ||box|| \mleq{} 3
31. (\mforall{}j'\mmember{}map(f;J).j' = hd(map(f;J)))
32. \mforall{}f1:name-morph(K;[]). (nerve\_box\_label(bx;(f o f1)) = nerve\_box\_label(box;f1))
33. k : nameset(K)
34. f1 : \{f:name-morph(K;[])| (f k) = 0\}
35. (f o f1) x \mneq{} 0
36. f1 (f x) \mneq{} 0
37. hd(map(f;J)) \mmember{} nameset(map(f;J))
38. \mforall{}i@0:nameset(I). \mforall{}c:cat-ob(poset-cat(I)).
poset\_functor\_extend(cat(G);I;\mlambda{}c.nerve\_box\_label(bx;c);
\mlambda{}y,c. nerve\_box\_edge1(G;bx;x;0;hd(J);c;y);c;flip(c;i@0))
= ((\mlambda{}y,c. nerve\_box\_edge1(G;bx;x;0;hd(J);c;y)) i@0 c)
supposing (c i@0) = 0
39. \mlambda{}i.((\muparrow{}isname(f i)) \mwedge{} ((f i) = k)) \mmember{} nameset(I) {}\mrightarrow{} \mBbbP{}
40. i1 : \mBbbN{}||I||
41. (f u) = k
42. u \mmember{} nameset(I)
43. ((f o f1) u) = 0
44. poset\_functor\_extend(cat(G);I;\mlambda{}c.nerve\_box\_label(bx;c);
\mlambda{}y,c. nerve\_box\_edge1(G;bx;x;0;hd(J);c;y);(f o f1);flip((f o f1);u))
= ((\mlambda{}y,c. nerve\_box\_edge1(G;bx;x;0;hd(J);c;y)) u (f o f1))
45. (f o flip(f1;k)) = flip((f o f1);u)
46. I[i1] = u
47. \muparrow{}isname(f u)
48. f u \mmember{} nameset(K)
49. (f1 (f u)) = 0
50. \mforall{}f1:name-morph(K;[]). \mforall{}u:nameset(I).
((\muparrow{}isname(f u))
{}\mRightarrow{} ((f1 (f u)) = 0)
{}\mRightarrow{} ((((f1 (f x)) = 0) \mvee{} (\mneg{}((f u) = hd(map(f;J))))) \mwedge{} ((((f o f1) x) = 0) \mvee{} (\mneg{}(u = hd(J)))))
{}\mRightarrow{} (nerve\_box\_edge(box;f1;f u) = nerve\_box\_edge(bx;(f o f1);u)))
51. (flip(f1;f x) (f x)) = 0
52. i = 0
53. \mneg{}(u = x)
54. \mneg{}((f u) = (f x))
55. groupoid-square1(G;nerve\_box\_label(box;flip(f1;f x));nerve\_box\_label(box;flip(flip(f1;f x);f
u));
nerve\_box\_label(box;f1);nerve\_box\_label(box;flip(f1;f u));nerve\_box\_edge(box;flip(f1;f x);f u);
nerve\_box\_edge(box;flip(flip(f1;f x);f u);f x);nerve\_box\_edge(box;flip(f1;f x);f x))
= groupoid-square1(G;nerve\_box\_label(bx;flip((f o f1);x));
nerve\_box\_label(bx;flip(flip((f o f1);x);u));nerve\_box\_label(bx;(f o f1));
nerve\_box\_label(bx;flip((f o f1);u));nerve\_box\_edge(bx;flip((f o f1);x);u);
nerve\_box\_edge(bx;flip(flip((f o f1);x);u);x);nerve\_box\_edge(bx;flip((f o f1);x);x))
56. d : cat-arrow(cat(G)) nerve\_box\_label(box;f1) nerve\_box\_label(box;flip(f1;f u))
\mvdash{} istype(nerve\_box\_edge(box;flip(f1;f x);f u) o nerve\_box\_edge(box;flip(flip(f1;f x);f u);f x)
= nerve\_box\_edge(box;flip(f1;f x);f x) o d)
By
Latex:
(At \mkleeneopen{}Type\mkleeneclose{} (D 0)\mcdot{} THEN MemCD)
Home
Index