Proof of Nuprl Lemma : nerve_box_edge

Step * 1 2 2 1 1 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. y : nameset(I)
9. c : {c:name-morph(I;[])| (c y) = 0 ∈ ℕ2}
10. (∃j∈J. ¬(j = y ∈ Cname)) ∨ (((c x) = i ∈ ℕ2) ∧ (¬↑null(J)))
11. x1 : nameset(I)
12. f2 : ℕ2
13. f3 : Functor(poset-cat(I-[x1]);C)
14. (<x1, f2, f3> ∈ box)
15. f2 = (c x1) ∈ ℕ2
16. f2 = (flip(c;y) x1) ∈ ℕ2
17. x2 : nameset(I)
18. g2 : ℕ2
19. g3 : Functor(poset-cat(I-[x2]);C)
20. (<x2, g2, g3> ∈ box)
21. g2 = (c x2) ∈ ℕ2
22. g2 = (flip(c;y) x2) ∈ ℕ2
23. nerve-box-common-face(box;c;y)
= <x2, g2, g3>
∈ {f:I-face(cubical-nerve(C);I)|

   (f ∈ box) ∧ ((fst(snd(f))) = (c (fst(f))) ∈ ℕ2) ∧ ((fst(snd(f))) = (flip(c;y) (fst(f))) ∈ ℕ2)}

24. ¬↑null(J)
25. (g3 c) = nerve_box_label(box;c) ∈ cat-ob(C)
26. (g3 flip(c;y)) = nerve_box_label(box;flip(c;y)) ∈ cat-ob(C)
27. ¬(x2 = x1 ∈ Cname)
28. functor-comp(poset-functor(I-[x1];I-[x1; x2];(x2:=g2));f3)
= functor-comp(poset-functor(I-[x2];I-[x1; x2];(x1:=f2));g3)
∈ Functor(poset-cat(I-[x1; x2]);C)
⊢ (f3 c flip(c;y) (λx.Ax)) = (g3 c flip(c;y) (λx.Ax)) ∈ (cat-arrow(C) (g3 c) (g3 flip(c;y)))
BY
{ (RenameTo `a' `y'
   THEN RenameTo `z' `x2'
   THEN RenameTo `y' `x1'
   THEN RenameTo`d' `g2'
   THEN RenameTo`b' `f2'

   THEN Assert ⌜((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))⌝⋅) }

1
.....assertion.....
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)
⊢ ((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))

2
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)}

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. y : nameset(I) 9. c : \{c:name-morph(I;[])| (c y) = 0\} 10. (\mexists{}j\mmember{}J. \mneg{}(j = y)) \mvee{} (((c x) = i) \mwedge{} (\mneg{}\muparrow{}null(J))) 11. x1 : nameset(I) 12. f2 : \mBbbN{}2 13. f3 : Functor(poset-cat(I-[x1]);C) 14. (<x1, f2, f3> \mmember{} box) 15. f2 = (c x1) 16. f2 = (flip(c;y) x1) 17. x2 : nameset(I) 18. g2 : \mBbbN{}2 19. g3 : Functor(poset-cat(I-[x2]);C) 20. (<x2, g2, g3> \mmember{} box) 21. g2 = (c x2) 22. g2 = (flip(c;y) x2) 23. nerve-box-common-face(box;c;y) = <x2, g2, g3> 24. \mneg{}\muparrow{}null(J) 25. (g3 c) = nerve\_box\_label(box;c) 26. (g3 flip(c;y)) = nerve\_box\_label(box;flip(c;y)) 27. \mneg{}(x2 = x1) 28. functor-comp(poset-functor(I-[x1];I-[x1; x2];(x2:=g2));f3) = functor-comp(poset-functor(I-[x2];I-[x1; x2];(x1:=f2));g3) \mvdash{} (f3 c flip(c;y) (\mlambda{}x.Ax)) = (g3 c flip(c;y) (\mlambda{}x.Ax)) By Latex: (RenameTo `a' `y' THEN RenameTo `z' `x2' THEN RenameTo `y' `x1' THEN RenameTo`d' `g2' THEN RenameTo`b' `f2' THEN Assert \mkleeneopen{}((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))\mkleeneclose{}\mcdot{}) Home Index