Step
*
1
2
2
1
1
2
of Lemma
nerve_box_edge_same1
1. C : SmallCategory
2. I : Cname List
3. J : nameset(I) List
4. x : nameset(I)
5. i : ℕ2
6. box : open_box(cubical-nerve(C);I;J;x;i)
7. ∀[L:name-morph(I;[])]
     ∀f:I-face(cubical-nerve(C);I)
       ((snd(snd(f)) L) = nerve_box_label(box;L) ∈ cat-ob(C)) supposing 
          ((f ∈ box) and 
          ((fst(snd(f))) = (L (fst(f))) ∈ ℕ2)) 
     supposing ((L x) = i ∈ ℕ2) ∨ (¬↑null(J))
8. a : nameset(I)
9. c : {c:name-morph(I;[])| (c a) = 0 ∈ ℕ2} 
10. (∃j∈J. ¬(j = a ∈ Cname)) ∨ (((c x) = i ∈ ℕ2) ∧ (¬↑null(J)))
11. y : nameset(I)
12. b : ℕ2
13. f3 : Functor(poset-cat(I-[y]);C)
14. (<y, b, f3> ∈ box)
15. b = (c y) ∈ ℕ2
16. b = (flip(c;a) y) ∈ ℕ2
17. z : nameset(I)
18. d : ℕ2
19. g3 : Functor(poset-cat(I-[z]);C)
20. (<z, d, g3> ∈ box)
21. d = (c z) ∈ ℕ2
22. d = (flip(c;a) z) ∈ ℕ2
23. nerve-box-common-face(box;c;a)
= <z, d, g3>
∈ {f:I-face(cubical-nerve(C);I)| 
   (f ∈ box) ∧ ((fst(snd(f))) = (c (fst(f))) ∈ ℕ2) ∧ ((fst(snd(f))) = (flip(c;a) (fst(f))) ∈ ℕ2)} 
24. ¬↑null(J)
25. (g3 c) = nerve_box_label(box;c) ∈ cat-ob(C)
26. (g3 flip(c;a)) = nerve_box_label(box;flip(c;a)) ∈ cat-ob(C)
27. ¬(z = y ∈ Cname)
28. functor-comp(poset-functor(I-[y];I-[y; z];(z:=d));f3)
= functor-comp(poset-functor(I-[z];I-[y; z];(y:=b));g3)
∈ Functor(poset-cat(I-[y; z]);C)
29. ((functor-comp(poset-functor(I-[z];I-[y; z];(y:=b));g3) flip(c;a)) = (g3 flip(c;a)) ∈ cat-ob(C))
∧ ((functor-comp(poset-functor(I-[y];I-[y; z];(z:=d));f3) c) = (f3 c) ∈ cat-ob(C))
⊢ (f3 c flip(c;a) (λx.Ax)) = (g3 c flip(c;a) (λx.Ax)) ∈ (cat-arrow(C) (g3 c) (g3 flip(c;a)))
BY
{ D -1 }
1
1. C : SmallCategory
2. I : Cname List
3. J : nameset(I) List
4. x : nameset(I)
5. i : ℕ2
6. box : open_box(cubical-nerve(C);I;J;x;i)
7. ∀[L:name-morph(I;[])]
     ∀f:I-face(cubical-nerve(C);I)
       ((snd(snd(f)) L) = nerve_box_label(box;L) ∈ cat-ob(C)) supposing 
          ((f ∈ box) and 
          ((fst(snd(f))) = (L (fst(f))) ∈ ℕ2)) 
     supposing ((L x) = i ∈ ℕ2) ∨ (¬↑null(J))
8. a : nameset(I)
9. c : {c:name-morph(I;[])| (c a) = 0 ∈ ℕ2} 
10. (∃j∈J. ¬(j = a ∈ Cname)) ∨ (((c x) = i ∈ ℕ2) ∧ (¬↑null(J)))
11. y : nameset(I)
12. b : ℕ2
13. f3 : Functor(poset-cat(I-[y]);C)
14. (<y, b, f3> ∈ box)
15. b = (c y) ∈ ℕ2
16. b = (flip(c;a) y) ∈ ℕ2
17. z : nameset(I)
18. d : ℕ2
19. g3 : Functor(poset-cat(I-[z]);C)
20. (<z, d, g3> ∈ box)
21. d = (c z) ∈ ℕ2
22. d = (flip(c;a) z) ∈ ℕ2
23. nerve-box-common-face(box;c;a)
= <z, d, g3>
∈ {f:I-face(cubical-nerve(C);I)| 
   (f ∈ box) ∧ ((fst(snd(f))) = (c (fst(f))) ∈ ℕ2) ∧ ((fst(snd(f))) = (flip(c;a) (fst(f))) ∈ ℕ2)} 
24. ¬↑null(J)
25. (g3 c) = nerve_box_label(box;c) ∈ cat-ob(C)
26. (g3 flip(c;a)) = nerve_box_label(box;flip(c;a)) ∈ cat-ob(C)
27. ¬(z = y ∈ Cname)
28. functor-comp(poset-functor(I-[y];I-[y; z];(z:=d));f3)
= functor-comp(poset-functor(I-[z];I-[y; z];(y:=b));g3)
∈ Functor(poset-cat(I-[y; z]);C)
29. (functor-comp(poset-functor(I-[z];I-[y; z];(y:=b));g3) flip(c;a)) = (g3 flip(c;a)) ∈ cat-ob(C)
30. (functor-comp(poset-functor(I-[y];I-[y; z];(z:=d));f3) c) = (f3 c) ∈ cat-ob(C)
⊢ (f3 c flip(c;a) (λx.Ax)) = (g3 c flip(c;a) (λx.Ax)) ∈ (cat-arrow(C) (g3 c) (g3 flip(c;a)))
Latex:
Latex:
1.  C  :  SmallCategory
2.  I  :  Cname  List
3.  J  :  nameset(I)  List
4.  x  :  nameset(I)
5.  i  :  \mBbbN{}2
6.  box  :  open\_box(cubical-nerve(C);I;J;x;i)
7.  \mforall{}[L:name-morph(I;[])]
          \mforall{}f:I-face(cubical-nerve(C);I)
              ((snd(snd(f))  L)  =  nerve\_box\_label(box;L))  supposing 
                    ((f  \mmember{}  box)  and 
                    ((fst(snd(f)))  =  (L  (fst(f))))) 
          supposing  ((L  x)  =  i)  \mvee{}  (\mneg{}\muparrow{}null(J))
8.  a  :  nameset(I)
9.  c  :  \{c:name-morph(I;[])|  (c  a)  =  0\} 
10.  (\mexists{}j\mmember{}J.  \mneg{}(j  =  a))  \mvee{}  (((c  x)  =  i)  \mwedge{}  (\mneg{}\muparrow{}null(J)))
11.  y  :  nameset(I)
12.  b  :  \mBbbN{}2
13.  f3  :  Functor(poset-cat(I-[y]);C)
14.  (<y,  b,  f3>  \mmember{}  box)
15.  b  =  (c  y)
16.  b  =  (flip(c;a)  y)
17.  z  :  nameset(I)
18.  d  :  \mBbbN{}2
19.  g3  :  Functor(poset-cat(I-[z]);C)
20.  (<z,  d,  g3>  \mmember{}  box)
21.  d  =  (c  z)
22.  d  =  (flip(c;a)  z)
23.  nerve-box-common-face(box;c;a)  =  <z,  d,  g3>
24.  \mneg{}\muparrow{}null(J)
25.  (g3  c)  =  nerve\_box\_label(box;c)
26.  (g3  flip(c;a))  =  nerve\_box\_label(box;flip(c;a))
27.  \mneg{}(z  =  y)
28.  functor-comp(poset-functor(I-[y];I-[y;  z];(z:=d));f3)
=  functor-comp(poset-functor(I-[z];I-[y;  z];(y:=b));g3)
29.  ((functor-comp(poset-functor(I-[z];I-[y;  z];(y:=b));g3)  flip(c;a))  =  (g3  flip(c;a)))
\mwedge{}  ((functor-comp(poset-functor(I-[y];I-[y;  z];(z:=d));f3)  c)  =  (f3  c))
\mvdash{}  (f3  c  flip(c;a)  (\mlambda{}x.Ax))  =  (g3  c  flip(c;a)  (\mlambda{}x.Ax))
By
Latex:
D  -1
Home
Index