Step
*
2
1
2
1
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))
⊢ (∀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 ||open_box_image(cubical-nerve(cat(G));I;K;f;bx)||
then groupoid-nerve-filler2(cat(G);K;map(f;J);open_box_image(cubical-nerve(cat(G));I;K;f;bx))
else groupoid-nerve-filler1(G;K;map(f;J);f x;i;open_box_image(cubical-nerve(cat(G));I;K;f;bx))
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 ||open_box_image(cubical-nerve(cat(G));I;K;f;bx)||
then groupoid-nerve-filler2(cat(G);K;map(f;J);open_box_image(cubical-nerve(cat(G));I;K;f;bx))
else groupoid-nerve-filler1(G;K;map(f;J);f x;i;open_box_image(cubical-nerve(cat(G));I;K;f;bx))
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
{ ((GenConclTerm ⌜open_box_image(cubical-nerve(cat(G));I;K;f;bx)⌝⋅ THENA Auto)
THEN RenameVar `box' (-2)
THEN Assert ⌜∀f1:name-morph(K;[]). (nerve_box_label(bx;(f o f1)) = nerve_box_label(box;f1) ∈ cat-ob(cat(G)))⌝⋅) }
1
.....assertion.....
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)
⊢ ∀f1:name-morph(K;[]). (nerve_box_label(bx;(f o f1)) = nerve_box_label(box;f1) ∈ cat-ob(cat(G)))
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. 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)))))
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))
\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 ||open\_box\_image(cubical-nerve(cat(G));I;K;f;bx)||
then groupoid-nerve-filler2(cat(G);K;map(f;
J);open\_box\_image(cubical-nerve(cat(G));I;K;f;bx))
else groupoid-nerve-filler1(G;K;map(f;J);f
x;i;open\_box\_image(cubical-nerve(cat(G));I;K;f;bx))
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 ||open\_box\_image(cubical-nerve(cat(G));I;K;f;bx)||
then groupoid-nerve-filler2(cat(G);K;map(f;
J);open\_box\_image(cubical-nerve(cat(G));I;K;f;bx))
else groupoid-nerve-filler1(G;K;map(f;J);f
x;i;open\_box\_image(cubical-nerve(cat(G));I;K;f;bx))
fi
f1
flip(f1;x1)
(\mlambda{}x.Ax))))
By
Latex:
((GenConclTerm \mkleeneopen{}open\_box\_image(cubical-nerve(cat(G));I;K;f;bx)\mkleeneclose{}\mcdot{} THENA Auto)
THEN RenameVar `box' (-2)
THEN Assert \mkleeneopen{}\mforall{}f1:name-morph(K;[]). (nerve\_box\_label(bx;(f o f1)) = nerve\_box\_label(box;f1))\mkleeneclose{}\mcdot{})
Home
Index