Step
*
1
2
2
1
1
1
1
1
2
1
1
1
of Lemma
groupoid-nerve-filler-fills
1. G : Groupoid
2. I : Cname List
3. J : nameset(I) List
4. ¬(J = [] ∈ (nameset(I) List))
5. x : nameset(I)
6. i : ℕ2
7. bx : open_box(cubical-nerve(cat(G));I;J;x;i)
8. ¬3 < ||bx||
9. ||bx|| ≤ 3
10. (∀j'∈J.j' = hd(J) ∈ Cname)
11. ¬↑null(J)
12. i1 : ℕ||bx||
13. y : nameset(I)
14. a : ℕ2
15. F : Functor(poset-cat(I-[y]);cat(G))
16. bx[i1] = <y, a, F> ∈ I-face(cubical-nerve(cat(G));I)
17. (y = x ∈ Cname) ⇒ (a = i ∈ ℕ2)
18. ∀f:name-morph(I-[y];[]). (((y:=a) o f) ∈ name-morph(I;[]))
19. λx.nerve_box_label(bx;((y:=a) o x)) ∈ name-morph(I-[y];[]) ⟶ cat-ob(cat(G))
20. λz,f. nerve_box_edge1(G;bx;x;i;hd(J);((y:=a) o f);z) ∈ i:nameset(I-[y])
⟶ c:{c:name-morph(I-[y];[])| (c i) = 0 ∈ ℕ2}
⟶ (cat-arrow(cat(G)) ((λx.nerve_box_label(bx;((y:=a) o x))) c) ((λx.nerve_box_label(bx;((y:=a) o x))) flip(c;i)))
21. ∀f:name-morph(I-[y];[]). (direction(<y, a, F>) = (((y:=a) o f) dimension(<y, a, F>)) ∈ ℕ2)
22. poset-functor-extends(cat(G);I-[y];λx.nerve_box_label(bx;((y:=a) o x));
λz,f. nerve_box_edge1(G;bx;x;i;hd(J);((y:=a) o f);z);F)
23. ∀[F,G@0:Functor(poset-cat(I-[y]);cat(G))].
(F = G@0 ∈ Functor(poset-cat(I-[y]);cat(G))) supposing
(poset-functor-extends(cat(G);I-[y];λx.nerve_box_label(bx;((y:=a) o x));
λz,f. nerve_box_edge1(G;bx;x;i;hd(J);((y:=a) o f);z);G@0) and
poset-functor-extends(cat(G);I-[y];λx.nerve_box_label(bx;((y:=a) o x));
λz,f. nerve_box_edge1(G;bx;x;i;hd(J);((y:=a) o f);z);F))
⊢ poset-functor-extends(cat(G);I-[y];λx.nerve_box_label(bx;((y:=a) o x));
λz,f. nerve_box_edge1(G;bx;x;i;hd(J);((y:=a) o f);z);
functor-comp(poset-functor(I;I-[y];(y:=a));groupoid-nerve-filler1(G;I;J;x;i;bx)))
BY
{ TACTIC:(InstLemma `poset_functor_extend-extends` [⌜cat(G)⌝;⌜I-[y]⌝;⌜λx.nerve_box_label(bx;((y:=a) o x))⌝;
⌜λz,f. nerve_box_edge1(G;bx;x;i;hd(J);((y:=a) o f);z)⌝]⋅
THENA Auto
) }
1
1. G : Groupoid
2. I : Cname List
3. J : nameset(I) List
4. ¬(J = [] ∈ (nameset(I) List))
5. x : nameset(I)
6. i : ℕ2
7. bx : open_box(cubical-nerve(cat(G));I;J;x;i)
8. ¬3 < ||bx||
9. ||bx|| ≤ 3
10. (∀j'∈J.j' = hd(J) ∈ Cname)
11. ¬↑null(J)
12. i1 : ℕ||bx||
13. y : nameset(I)
14. a : ℕ2
15. F : Functor(poset-cat(I-[y]);cat(G))
16. bx[i1] = <y, a, F> ∈ I-face(cubical-nerve(cat(G));I)
17. (y = x ∈ Cname) ⇒ (a = i ∈ ℕ2)
18. ∀f:name-morph(I-[y];[]). (((y:=a) o f) ∈ name-morph(I;[]))
19. λx.nerve_box_label(bx;((y:=a) o x)) ∈ name-morph(I-[y];[]) ⟶ cat-ob(cat(G))
20. λz,f. nerve_box_edge1(G;bx;x;i;hd(J);((y:=a) o f);z) ∈ i:nameset(I-[y])
⟶ c:{c:name-morph(I-[y];[])| (c i) = 0 ∈ ℕ2}
⟶ (cat-arrow(cat(G)) ((λx.nerve_box_label(bx;((y:=a) o x))) c) ((λx.nerve_box_label(bx;((y:=a) o x))) flip(c;i)))
21. ∀f:name-morph(I-[y];[]). (direction(<y, a, F>) = (((y:=a) o f) dimension(<y, a, F>)) ∈ ℕ2)
22. poset-functor-extends(cat(G);I-[y];λx.nerve_box_label(bx;((y:=a) o x));
λz,f. nerve_box_edge1(G;bx;x;i;hd(J);((y:=a) o f);z);F)
23. ∀[F,G@0:Functor(poset-cat(I-[y]);cat(G))].
(F = G@0 ∈ Functor(poset-cat(I-[y]);cat(G))) supposing
(poset-functor-extends(cat(G);I-[y];λx.nerve_box_label(bx;((y:=a) o x));
λz,f. nerve_box_edge1(G;bx;x;i;hd(J);((y:=a) o f);z);G@0) and
poset-functor-extends(cat(G);I-[y];λx.nerve_box_label(bx;((y:=a) o x));
λz,f. nerve_box_edge1(G;bx;x;i;hd(J);((y:=a) o f);z);F))
24. poset-functor-extends(cat(G);I-[y];λx.nerve_box_label(bx;((y:=a) o x));
λz,f. nerve_box_edge1(G;bx;x;i;hd(J);((y:=a) o f);z);
<λx.nerve_box_label(bx;((y:=a) o x))
, λc1,c2,p. poset_functor_extend(cat(G);I-[y];λx.nerve_box_label(bx;((y:=a) o x));
λz,f. nerve_box_edge1(G;bx;x;i;hd(J);((y:=a) o f);z);c1;c2)
>)
⊢ poset-functor-extends(cat(G);I-[y];λx.nerve_box_label(bx;((y:=a) o x));
λz,f. nerve_box_edge1(G;bx;x;i;hd(J);((y:=a) o f);z);
functor-comp(poset-functor(I;I-[y];(y:=a));groupoid-nerve-filler1(G;I;J;x;i;bx)))
Latex:
Latex:
1. G : Groupoid
2. I : Cname List
3. J : nameset(I) List
4. \mneg{}(J = [])
5. x : nameset(I)
6. i : \mBbbN{}2
7. bx : open\_box(cubical-nerve(cat(G));I;J;x;i)
8. \mneg{}3 < ||bx||
9. ||bx|| \mleq{} 3
10. (\mforall{}j'\mmember{}J.j' = hd(J))
11. \mneg{}\muparrow{}null(J)
12. i1 : \mBbbN{}||bx||
13. y : nameset(I)
14. a : \mBbbN{}2
15. F : Functor(poset-cat(I-[y]);cat(G))
16. bx[i1] = <y, a, F>
17. (y = x) {}\mRightarrow{} (a = i)
18. \mforall{}f:name-morph(I-[y];[]). (((y:=a) o f) \mmember{} name-morph(I;[]))
19. \mlambda{}x.nerve\_box\_label(bx;((y:=a) o x)) \mmember{} name-morph(I-[y];[]) {}\mrightarrow{} cat-ob(cat(G))
20. \mlambda{}z,f. nerve\_box\_edge1(G;bx;x;i;hd(J);((y:=a) o f);z) \mmember{} i:nameset(I-[y])
{}\mrightarrow{} c:\{c:name-morph(I-[y];[])| (c i) = 0\}
{}\mrightarrow{} (cat-arrow(cat(G)) ((\mlambda{}x.nerve\_box\_label(bx;((y:=a) o x))) c)
((\mlambda{}x.nerve\_box\_label(bx;((y:=a) o x))) flip(c;i)))
21. \mforall{}f:name-morph(I-[y];[]). (direction(<y, a, F>) = (((y:=a) o f) dimension(<y, a, F>)))
22. poset-functor-extends(cat(G);I-[y];\mlambda{}x.nerve\_box\_label(bx;((y:=a) o x));
\mlambda{}z,f. nerve\_box\_edge1(G;bx;x;i;hd(J);((y:=a) o f);z);F)
23. \mforall{}[F,G@0:Functor(poset-cat(I-[y]);cat(G))].
(F = G@0) supposing
(poset-functor-extends(cat(G);I-[y];\mlambda{}x.nerve\_box\_label(bx;((y:=a) o x));
\mlambda{}z,f. nerve\_box\_edge1(G;bx;x;i;hd(J);((y:=a) o f);z);G@0) and
poset-functor-extends(cat(G);I-[y];\mlambda{}x.nerve\_box\_label(bx;((y:=a) o x));
\mlambda{}z,f. nerve\_box\_edge1(G;bx;x;i;hd(J);((y:=a) o f);z);F))
\mvdash{} poset-functor-extends(cat(G);I-[y];\mlambda{}x.nerve\_box\_label(bx;((y:=a) o x));
\mlambda{}z,f. nerve\_box\_edge1(G;bx;x;i;hd(J);((y:=a) o f);z);
functor-comp(poset-functor(I;I-[y];(y:=a));
groupoid-nerve-filler1(G;I;J;x;i;bx)))
By
Latex:
TACTIC:(InstLemma `poset\_functor\_extend-extends` [\mkleeneopen{}cat(G)\mkleeneclose{};\mkleeneopen{}I-[y]\mkleeneclose{};
\mkleeneopen{}\mlambda{}x.nerve\_box\_label(bx;((y:=a) o x))\mkleeneclose{};\mkleeneopen{}\mlambda{}z,f. nerve\_box\_edge1(G;bx;x;i;hd(J);((y:=a) o f);z)\mkleeneclose{}\000C]\mcdot{}
THENA Auto
)
Home
Index