Step
*
2
1
3
1
2
of Lemma
poset-functor-extends-box-faces
.....subterm..... T:t
2:n
1. G : Groupoid
2. I : Cname List
3. J : nameset(I) List
4. x : nameset(I)
5. i : ℕ2
6. bx : open_box(cubical-nerve(cat(G));I;J;x;i)
7. ¬↑null(J)
8. (∃j1∈J. (∃j2∈J. ¬(j1 = j2 ∈ Cname)))
9. i1 : ℕ||bx||
10. ∀f:name-morph(I-[dimension(bx[i1])];[]). (((dimension(bx[i1]):=direction(bx[i1])) o f) ∈ name-morph(I;[]))
11. i2 : nameset(I-[dimension(bx[i1])])
12. c : {c:name-morph(I-[dimension(bx[i1])];[])| (c i2) = 0 ∈ ℕ2}
13. ((dimension(bx[i1]):=direction(bx[i1])) o c) ∈ name-morph(I;[])
14. (((dimension(bx[i1]):=direction(bx[i1])) o c) i2) = 0 ∈ ℕ2
15. (cube(bx[i1]) ((dimension(bx[i1]):=direction(bx[i1])) o c) flip(((dimension(bx[i1]):=direction(bx[i1])) o c);i2)
(λx.Ax))
= nerve_box_edge(bx;((dimension(bx[i1]):=direction(bx[i1])) o c);i2)
∈ (cat-arrow(cat(G)) nerve_box_label(bx;((dimension(bx[i1]):=direction(bx[i1])) o c))
nerve_box_label(bx;flip(((dimension(bx[i1]):=direction(bx[i1])) o c);i2)))
⊢ nerve_box_label(bx;flip(((dimension(bx[i1]):=direction(bx[i1])) o c);i2))
= nerve_box_label(bx;((dimension(bx[i1]):=direction(bx[i1])) o flip(c;i2)))
∈ cat-ob(cat(G))
BY
{ Assert ⌜flip(((dimension(bx[i1]):=direction(bx[i1])) o c);i2)
= ((dimension(bx[i1]):=direction(bx[i1])) o flip(c;i2))
∈ name-morph(I;[])⌝⋅ }
1
.....assertion.....
1. G : Groupoid
2. I : Cname List
3. J : nameset(I) List
4. x : nameset(I)
5. i : ℕ2
6. bx : open_box(cubical-nerve(cat(G));I;J;x;i)
7. ¬↑null(J)
8. (∃j1∈J. (∃j2∈J. ¬(j1 = j2 ∈ Cname)))
9. i1 : ℕ||bx||
10. ∀f:name-morph(I-[dimension(bx[i1])];[]). (((dimension(bx[i1]):=direction(bx[i1])) o f) ∈ name-morph(I;[]))
11. i2 : nameset(I-[dimension(bx[i1])])
12. c : {c:name-morph(I-[dimension(bx[i1])];[])| (c i2) = 0 ∈ ℕ2}
13. ((dimension(bx[i1]):=direction(bx[i1])) o c) ∈ name-morph(I;[])
14. (((dimension(bx[i1]):=direction(bx[i1])) o c) i2) = 0 ∈ ℕ2
15. (cube(bx[i1]) ((dimension(bx[i1]):=direction(bx[i1])) o c) flip(((dimension(bx[i1]):=direction(bx[i1])) o c);i2)
(λx.Ax))
= nerve_box_edge(bx;((dimension(bx[i1]):=direction(bx[i1])) o c);i2)
∈ (cat-arrow(cat(G)) nerve_box_label(bx;((dimension(bx[i1]):=direction(bx[i1])) o c))
nerve_box_label(bx;flip(((dimension(bx[i1]):=direction(bx[i1])) o c);i2)))
⊢ flip(((dimension(bx[i1]):=direction(bx[i1])) o c);i2)
= ((dimension(bx[i1]):=direction(bx[i1])) o flip(c;i2))
∈ name-morph(I;[])
2
1. G : Groupoid
2. I : Cname List
3. J : nameset(I) List
4. x : nameset(I)
5. i : ℕ2
6. bx : open_box(cubical-nerve(cat(G));I;J;x;i)
7. ¬↑null(J)
8. (∃j1∈J. (∃j2∈J. ¬(j1 = j2 ∈ Cname)))
9. i1 : ℕ||bx||
10. ∀f:name-morph(I-[dimension(bx[i1])];[]). (((dimension(bx[i1]):=direction(bx[i1])) o f) ∈ name-morph(I;[]))
11. i2 : nameset(I-[dimension(bx[i1])])
12. c : {c:name-morph(I-[dimension(bx[i1])];[])| (c i2) = 0 ∈ ℕ2}
13. ((dimension(bx[i1]):=direction(bx[i1])) o c) ∈ name-morph(I;[])
14. (((dimension(bx[i1]):=direction(bx[i1])) o c) i2) = 0 ∈ ℕ2
15. (cube(bx[i1]) ((dimension(bx[i1]):=direction(bx[i1])) o c) flip(((dimension(bx[i1]):=direction(bx[i1])) o c);i2)
(λx.Ax))
= nerve_box_edge(bx;((dimension(bx[i1]):=direction(bx[i1])) o c);i2)
∈ (cat-arrow(cat(G)) nerve_box_label(bx;((dimension(bx[i1]):=direction(bx[i1])) o c))
nerve_box_label(bx;flip(((dimension(bx[i1]):=direction(bx[i1])) o c);i2)))
16. flip(((dimension(bx[i1]):=direction(bx[i1])) o c);i2)
= ((dimension(bx[i1]):=direction(bx[i1])) o flip(c;i2))
∈ name-morph(I;[])
⊢ nerve_box_label(bx;flip(((dimension(bx[i1]):=direction(bx[i1])) o c);i2))
= nerve_box_label(bx;((dimension(bx[i1]):=direction(bx[i1])) o flip(c;i2)))
∈ cat-ob(cat(G))
Latex:
Latex:
.....subterm..... T:t
2:n
1. G : Groupoid
2. I : Cname List
3. J : nameset(I) List
4. x : nameset(I)
5. i : \mBbbN{}2
6. bx : open\_box(cubical-nerve(cat(G));I;J;x;i)
7. \mneg{}\muparrow{}null(J)
8. (\mexists{}j1\mmember{}J. (\mexists{}j2\mmember{}J. \mneg{}(j1 = j2)))
9. i1 : \mBbbN{}||bx||
10. \mforall{}f:name-morph(I-[dimension(bx[i1])];[])
(((dimension(bx[i1]):=direction(bx[i1])) o f) \mmember{} name-morph(I;[]))
11. i2 : nameset(I-[dimension(bx[i1])])
12. c : \{c:name-morph(I-[dimension(bx[i1])];[])| (c i2) = 0\}
13. ((dimension(bx[i1]):=direction(bx[i1])) o c) \mmember{} name-morph(I;[])
14. (((dimension(bx[i1]):=direction(bx[i1])) o c) i2) = 0
15. (cube(bx[i1]) ((dimension(bx[i1]):=direction(bx[i1])) o c)
flip(((dimension(bx[i1]):=direction(bx[i1])) o c);i2)
(\mlambda{}x.Ax))
= nerve\_box\_edge(bx;((dimension(bx[i1]):=direction(bx[i1])) o c);i2)
\mvdash{} nerve\_box\_label(bx;flip(((dimension(bx[i1]):=direction(bx[i1])) o c);i2))
= nerve\_box\_label(bx;((dimension(bx[i1]):=direction(bx[i1])) o flip(c;i2)))
By
Latex:
Assert \mkleeneopen{}flip(((dimension(bx[i1]):=direction(bx[i1])) o c);i2)
= ((dimension(bx[i1]):=direction(bx[i1])) o flip(c;i2))\mkleeneclose{}\mcdot{}
Home
Index