Step
*
2
1
3
1
2
1
1
1
of Lemma
poset-functor-extends-box-faces
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. i2 = i2 ∈ Cname
17. (i2 ∈ I)
18. ¬(i2 = dimension(bx[i1]) ∈ Cname)
19. x1 : nameset(I)
⊢ (flip(((dimension(bx[i1]):=direction(bx[i1])) o c);i2) x1)
= (((dimension(bx[i1]):=direction(bx[i1])) o flip(c;i2)) x1)
∈ extd-nameset([])
BY
{ (RepUR ``name-morph-flip name-comp face-map uext`` 0
THEN (BoolCase ⌜(x1 =z dimension(bx[i1]))⌝⋅ THENA Auto)
THEN (BoolCase ⌜eq-cname(x1;i2)⌝⋅ THENA Auto)) }
1
1. G : Groupoid
2. I : Cname List
3. J : nameset(I) List
4. x : ℤ
5. 2 ≤ x
6. (x ∈ I)
7. i : ℤ
8. 0 ≤ i
9. i < 2
10. bx : open_box(cubical-nerve(cat(G));I;J;x;i)
11. ¬↑null(J)
12. (∃j1∈J. (∃j2∈J. ¬(j1 = j2 ∈ Cname)))
13. i1 : ℤ
14. 0 ≤ i1
15. i1 < ||bx||
16. ∀f:name-morph(I-[dimension(bx[i1])];[]). (((dimension(bx[i1]):=direction(bx[i1])) o f) ∈ name-morph(I;[]))
17. i2 : ℤ
18. 2 ≤ i2
19. (i2 ∈ I-[dimension(bx[i1])])
20. c : {c:name-morph(I-[dimension(bx[i1])];[])| (c i2) = 0 ∈ ℕ2}
21. ((dimension(bx[i1]):=direction(bx[i1])) o c) ∈ name-morph(I;[])
22. (((dimension(bx[i1]):=direction(bx[i1])) o c) i2) = 0 ∈ ℤ
23. 0 ≤ (((dimension(bx[i1]):=direction(bx[i1])) o c) i2)
24. ((dimension(bx[i1]):=direction(bx[i1])) o c) i2 < 2
25. (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)))
26. i2 = i2 ∈ ℤ
27. 2 ≤ i2
28. (i2 ∈ I)
29. ¬(i2 = dimension(bx[i1]) ∈ Cname)
30. x1 : ℤ
31. 2 ≤ x1
32. (x1 ∈ I)
33. x1 = dimension(bx[i1]) ∈ ℤ
34. x1 = i2 ∈ ℤ
35. 2 ≤ x1
36. dimension(bx[i1]) ∈ ℤ
⊢ ¬(i2 = dimension(bx[i1]) ∈ ℤ)
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. i2 = i2 ∈ Cname
17. (i2 ∈ I)
18. ¬(i2 = dimension(bx[i1]) ∈ Cname)
19. x1 : nameset(I)
20. ¬(x1 = i2 ∈ Cname)
21. x1 = dimension(bx[i1]) ∈ ℤ
⊢ if isname(direction(bx[i1])) then c direction(bx[i1]) else direction(bx[i1]) fi
= if isname(direction(bx[i1]))
then if eq-cname(direction(bx[i1]);i2) then 1 - c direction(bx[i1]) else c direction(bx[i1]) fi
else direction(bx[i1])
fi
∈ extd-nameset([])
3
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. i2 = i2 ∈ Cname
17. (i2 ∈ I)
18. ¬(i2 = dimension(bx[i1]) ∈ Cname)
19. x1 : nameset(I)
20. x1 ≠ dimension(bx[i1])
21. x1 = i2 ∈ Cname
⊢ (1 - if isname(x1) then c x1 else x1 fi ) = if isname(x1) then 1 - c x1 else x1 fi ∈ extd-nameset([])
4
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. i2 = i2 ∈ Cname
17. (i2 ∈ I)
18. ¬(i2 = dimension(bx[i1]) ∈ Cname)
19. x1 : nameset(I)
20. ¬(x1 = i2 ∈ Cname)
21. x1 ≠ dimension(bx[i1])
⊢ if isname(x1) then c x1 else x1 fi = if isname(x1) then c x1 else x1 fi ∈ extd-nameset([])
Latex:
Latex:
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)
16. i2 = i2
17. (i2 \mmember{} I)
18. \mneg{}(i2 = dimension(bx[i1]))
19. x1 : nameset(I)
\mvdash{} (flip(((dimension(bx[i1]):=direction(bx[i1])) o c);i2) x1)
= (((dimension(bx[i1]):=direction(bx[i1])) o flip(c;i2)) x1)
By
Latex:
(RepUR ``name-morph-flip name-comp face-map uext`` 0
THEN (BoolCase \mkleeneopen{}(x1 =\msubz{} dimension(bx[i1]))\mkleeneclose{}\mcdot{} THENA Auto)
THEN (BoolCase \mkleeneopen{}eq-cname(x1;i2)\mkleeneclose{}\mcdot{} THENA Auto))
Home
Index