Step
*
2
1
2
1
2
of Lemma
groupoid-nerve-filler-uniform
1. G : Groupoid
2. True
3. I : Cname List
4. J : nameset(I) List
5. ¬(J = [] ∈ (nameset(I) List))
6. x : nameset(I)
7. i : ℕ2
8. bx : open_box(cubical-nerve(cat(G));I;J;x;i)
9. K : Cname List
10. f : name-morph(I;K)
11. ∀i:nameset(I). ((i ∈ J) ⇒ (↑isname(f i)))
12. ↑isname(f x)
13. ¬False
14. f ∈ nameset(J) ⟶ nameset(K)
15. map(f;J) ∈ nameset(K) List
16. f x ∈ nameset(K)
17. nameset([x / J]) ⊆r name-morph-domain(f;I)
18. ¬↑null(J)
19. ¬↑null(map(f;J))
20. box : open_box(cubical-nerve(cat(G));K;map(f;J);f x;i)
21. open_box_image(cubical-nerve(cat(G));I;K;f;bx) = box ∈ open_box(cubical-nerve(cat(G));K;map(f;J);f x;i)
22. ∀f1:name-morph(K;[]). (nerve_box_label(bx;(f o f1)) = nerve_box_label(box;f1) ∈ cat-ob(cat(G)))
⊢ (∀f1:name-morph(K;[])
((f(if 3 <z ||bx|| then groupoid-nerve-filler2(cat(G);I;J;bx) else groupoid-nerve-filler1(G;I;J;x;i;bx) fi ) f1)
= (if 3 <z ||box||
then groupoid-nerve-filler2(cat(G);K;map(f;J);box)
else groupoid-nerve-filler1(G;K;map(f;J);f x;i;box)
fi
f1)
∈ cat-ob(cat(G))))
∧ (∀x1:nameset(K). ∀f1:{f:name-morph(K;[])| (f x1) = 0 ∈ ℕ2} .
((f(if 3 <z ||bx|| then groupoid-nerve-filler2(cat(G);I;J;bx) else groupoid-nerve-filler1(G;I;J;x;i;bx) fi ) f1
flip(f1;x1)
(λx.Ax))
= (if 3 <z ||box||
then groupoid-nerve-filler2(cat(G);K;map(f;J);box)
else groupoid-nerve-filler1(G;K;map(f;J);f x;i;box)
fi
f1
flip(f1;x1)
(λx.Ax))
∈ (cat-arrow(cat(G))
(f(if 3 <z ||bx|| then groupoid-nerve-filler2(cat(G);I;J;bx) else groupoid-nerve-filler1(G;I;J;x;i;bx) fi ) f1)
(f(if 3 <z ||bx|| then groupoid-nerve-filler2(cat(G);I;J;bx) else groupoid-nerve-filler1(G;I;J;x;i;bx) fi )
flip(f1;x1)))))
BY
{ ((Assert ||bx|| = ||box|| ∈ ℤ BY
((RevHypSubst' (-2) 0 THENA Auto) THEN RWO "length-open_box_image" 0 THEN Auto))
THEN (BoolCase ⌜3 <z ||bx||⌝⋅ THENA Auto)
THEN (((FLemma `length-open_box-ge-3` [-1] THENA Auto)
THEN (Assert 3 < ||box|| BY
Auto)
THEN (FLemma `length-open_box-ge-3` [-1] THENA Auto))
ORELSE (((Assert ||bx|| ≤ 3 BY Auto) THEN (FLemma `length-open_box-le-3` [-1] THENA Auto))
THEN (Assert ||box|| ≤ 3 BY
Auto)
THEN (FLemma `length-open_box-le-3` [-1] THENA Auto))
)
THEN (BoolCase ⌜3 <z ||box||⌝⋅ THENA Auto)
THEN Try (OnMaybeHyp 21 (\h. (DNot h THEN Eliminate ⌜||box||⌝⋅ THEN Hypothesis)))
THEN RepUR ``groupoid-nerve-filler1 groupoid-nerve-filler2`` 0
THEN RepUR ``cube-set-restriction cubical-nerve functor-comp poset-functor`` 0
THEN BetterSplitAndConcl
THEN Try (Hypothesis)
THEN (UnivCD THENA Auto)
THEN RenameVar `k' (-2)) }
1
1. G : Groupoid
2. True
3. I : Cname List
4. J : nameset(I) List
5. ¬(J = [] ∈ (nameset(I) List))
6. x : nameset(I)
7. i : ℕ2
8. bx : open_box(cubical-nerve(cat(G));I;J;x;i)
9. K : Cname List
10. f : name-morph(I;K)
11. ∀i:nameset(I). ((i ∈ J) ⇒ (↑isname(f i)))
12. ↑isname(f x)
13. ¬False
14. f ∈ nameset(J) ⟶ nameset(K)
15. map(f;J) ∈ nameset(K) List
16. f x ∈ nameset(K)
17. nameset([x / J]) ⊆r name-morph-domain(f;I)
18. ¬↑null(J)
19. ¬↑null(map(f;J))
20. box : open_box(cubical-nerve(cat(G));K;map(f;J);f x;i)
21. open_box_image(cubical-nerve(cat(G));I;K;f;bx) = box ∈ open_box(cubical-nerve(cat(G));K;map(f;J);f x;i)
22. ∀f1:name-morph(K;[]). (nerve_box_label(bx;(f o f1)) = nerve_box_label(box;f1) ∈ cat-ob(cat(G)))
23. ||bx|| = ||box|| ∈ ℤ
24. 3 < ||bx||
25. (∃j1∈J. (∃j2∈J. ¬(j1 = j2 ∈ Cname)))
26. 3 < ||box||
27. (∃j1∈map(f;J). (∃j2∈map(f;J). ¬(j1 = j2 ∈ Cname)))
28. 3 < ||box||
29. ∀f1:name-morph(K;[]). (nerve_box_label(bx;(f o f1)) = nerve_box_label(box;f1) ∈ cat-ob(cat(G)))
30. k : nameset(K)
31. f1 : {f:name-morph(K;[])| (f k) = 0 ∈ ℕ2}
⊢ poset_functor_extend(cat(G);I;λc.nerve_box_label(bx;c);λy,c. nerve_box_edge(bx;c;y);(f o f1);(f o flip(f1;k)))
= poset_functor_extend(cat(G);K;λc.nerve_box_label(box;c);λy,c. nerve_box_edge(box;c;y);f1;flip(f1;k))
∈ (cat-arrow(cat(G)) nerve_box_label(bx;(f o f1)) nerve_box_label(bx;(f o flip(f1;k))))
2
1. G : Groupoid
2. True
3. I : Cname List
4. J : nameset(I) List
5. ¬(J = [] ∈ (nameset(I) List))
6. x : nameset(I)
7. i : ℕ2
8. bx : open_box(cubical-nerve(cat(G));I;J;x;i)
9. ¬3 < ||bx||
10. K : Cname List
11. f : name-morph(I;K)
12. ∀i:nameset(I). ((i ∈ J) ⇒ (↑isname(f i)))
13. ↑isname(f x)
14. ¬False
15. f ∈ nameset(J) ⟶ nameset(K)
16. map(f;J) ∈ nameset(K) List
17. f x ∈ nameset(K)
18. nameset([x / J]) ⊆r name-morph-domain(f;I)
19. ¬↑null(J)
20. ¬↑null(map(f;J))
21. box : open_box(cubical-nerve(cat(G));K;map(f;J);f x;i)
22. ¬3 < ||box||
23. open_box_image(cubical-nerve(cat(G));I;K;f;bx) = box ∈ open_box(cubical-nerve(cat(G));K;map(f;J);f x;i)
24. ∀f1:name-morph(K;[]). (nerve_box_label(bx;(f o f1)) = nerve_box_label(box;f1) ∈ cat-ob(cat(G)))
25. ||bx|| = ||box|| ∈ ℤ
26. ||bx|| ≤ 3
27. (∀j'∈J.j' = hd(J) ∈ Cname)
28. ||box|| ≤ 3
29. (∀j'∈map(f;J).j' = hd(map(f;J)) ∈ Cname)
30. ∀f1:name-morph(K;[]). (nerve_box_label(bx;(f o f1)) = nerve_box_label(box;f1) ∈ cat-ob(cat(G)))
31. k : nameset(K)
32. f1 : {f:name-morph(K;[])| (f k) = 0 ∈ ℕ2}
⊢ poset_functor_extend(cat(G);I;λc.nerve_box_label(bx;c);
λy,c. nerve_box_edge1(G;bx;x;i;hd(J);c;y);(f o f1);(f o flip(f1;k)))
= poset_functor_extend(cat(G);K;λc.nerve_box_label(box;c);λy,c. nerve_box_edge1(G;box;f x;i;hd(map(f;J));c;y);f1;flip(f1\000C;k))
∈ (cat-arrow(cat(G)) nerve_box_label(bx;(f o f1)) nerve_box_label(bx;(f o flip(f1;k))))
Latex:
Latex:
1. G : Groupoid
2. True
3. I : Cname List
4. J : nameset(I) List
5. \mneg{}(J = [])
6. x : nameset(I)
7. i : \mBbbN{}2
8. bx : open\_box(cubical-nerve(cat(G));I;J;x;i)
9. K : Cname List
10. f : name-morph(I;K)
11. \mforall{}i:nameset(I). ((i \mmember{} J) {}\mRightarrow{} (\muparrow{}isname(f i)))
12. \muparrow{}isname(f x)
13. \mneg{}False
14. f \mmember{} nameset(J) {}\mrightarrow{} nameset(K)
15. map(f;J) \mmember{} nameset(K) List
16. f x \mmember{} nameset(K)
17. nameset([x / J]) \msubseteq{}r name-morph-domain(f;I)
18. \mneg{}\muparrow{}null(J)
19. \mneg{}\muparrow{}null(map(f;J))
20. box : open\_box(cubical-nerve(cat(G));K;map(f;J);f x;i)
21. open\_box\_image(cubical-nerve(cat(G));I;K;f;bx) = box
22. \mforall{}f1:name-morph(K;[]). (nerve\_box\_label(bx;(f o f1)) = nerve\_box\_label(box;f1))
\mvdash{} (\mforall{}f1:name-morph(K;[])
((f(if 3 <z ||bx||
then groupoid-nerve-filler2(cat(G);I;J;bx)
else groupoid-nerve-filler1(G;I;J;x;i;bx)
fi )
f1)
= (if 3 <z ||box||
then groupoid-nerve-filler2(cat(G);K;map(f;J);box)
else groupoid-nerve-filler1(G;K;map(f;J);f x;i;box)
fi
f1)))
\mwedge{} (\mforall{}x1:nameset(K). \mforall{}f1:\{f:name-morph(K;[])| (f x1) = 0\} .
((f(if 3 <z ||bx||
then groupoid-nerve-filler2(cat(G);I;J;bx)
else groupoid-nerve-filler1(G;I;J;x;i;bx)
fi )
f1
flip(f1;x1)
(\mlambda{}x.Ax))
= (if 3 <z ||box||
then groupoid-nerve-filler2(cat(G);K;map(f;J);box)
else groupoid-nerve-filler1(G;K;map(f;J);f x;i;box)
fi
f1
flip(f1;x1)
(\mlambda{}x.Ax))))
By
Latex:
((Assert ||bx|| = ||box|| BY
((RevHypSubst' (-2) 0 THENA Auto) THEN RWO "length-open\_box\_image" 0 THEN Auto))
THEN (BoolCase \mkleeneopen{}3 <z ||bx||\mkleeneclose{}\mcdot{} THENA Auto)
THEN (((FLemma `length-open\_box-ge-3` [-1] THENA Auto)
THEN (Assert 3 < ||box|| BY
Auto)
THEN (FLemma `length-open\_box-ge-3` [-1] THENA Auto))
ORELSE (((Assert ||bx|| \mleq{} 3 BY Auto) THEN (FLemma `length-open\_box-le-3` [-1] THENA Auto))
THEN (Assert ||box|| \mleq{} 3 BY
Auto)
THEN (FLemma `length-open\_box-le-3` [-1] THENA Auto))
)
THEN (BoolCase \mkleeneopen{}3 <z ||box||\mkleeneclose{}\mcdot{} THENA Auto)
THEN Try (OnMaybeHyp 21 (\mbackslash{}h. (DNot h THEN Eliminate \mkleeneopen{}||box||\mkleeneclose{}\mcdot{} THEN Hypothesis)))
THEN RepUR ``groupoid-nerve-filler1 groupoid-nerve-filler2`` 0
THEN RepUR ``cube-set-restriction cubical-nerve functor-comp poset-functor`` 0
THEN BetterSplitAndConcl
THEN Try (Hypothesis)
THEN (UnivCD THENA Auto)
THEN RenameVar `k' (-2))
Home
Index