Proof of Nuprl Lemma : nerve_box_label

Step * 1 2 1 1 1 1 of Lemma nerve_box_label_same

1. C : SmallCategory
2. I : Cname List
3. J : nameset(I) List
4. x : nameset(I)
5. i : ℕ2
6. box : I-face(cubical-nerve(C);I) List
7. ∀f1,f2:I-face(cubical-nerve(C);I).
     ((f1 ∈ box)
     ⇒ (f2 ∈ box)
     ⇒ (¬(dimension(f1) = dimension(f2) ∈ Cname))
     ⇒ ((dimension(f2):=direction(f2))(cube(f1))
        = (dimension(f1):=direction(f1))(cube(f2))
        ∈ cubical-nerve(C)(I-[dimension(f1); dimension(f2)])))
8. ¬(x ∈ J)
9. l_subset(Cname;J;I)
10. ∀y:nameset(J). ∀c:ℕ2.  (∃f∈box. face-name(f) = <y, c> ∈ (nameset(I) × ℕ2))
11. (∃f∈box. face-name(f) = <x, i> ∈ (nameset(I) × ℕ2))
12. (∀f∈box.¬(face-name(f) = <x, 1 - i> ∈ (nameset(I) × ℕ2)))
13. (∀f∈box.(fst(f) ∈ [x / J]))
14. (∀f1,f2∈box.  ¬(face-name(f1) = face-name(f2) ∈ (nameset(I) × ℕ2)))
15. L : name-morph(I;[])
16. ((L x) = i ∈ ℕ2) ∨ (¬↑null(J))
17. f : I-face(cubical-nerve(C);I)
18. direction(f) = (L dimension(f)) ∈ ℕ2
19. (f ∈ box)
20. v : I-face(cubical-nerve(C);I)
21. (v ∈ box)
22. direction(v) = (L dimension(v)) ∈ ℕ2

23. nerve-box-face(box;L) = v ∈ {f:I-face(cubical-nerve(C);I)| (f ∈ box) ∧ (direction(f) = (L dimension(f)) ∈ ℕ2)}

24. ¬(dimension(v) = dimension(f) ∈ Cname)
25. (dimension(f):=L dimension(f)) ∈ name-morph(I-[dimension(v)];I-[dimension(v); dimension(f)])
26. (dimension(v):=L dimension(v)) ∈ name-morph(I-[dimension(f)];I-[dimension(v); dimension(f)])
27. G : Functor(poset-cat(I-[dimension(f)]);C)
28. F : Functor(poset-cat(I-[dimension(v)]);C)
29. functor-comp(poset-functor(I-[dimension(v)];I-[dimension(v); dimension(f)];(dimension(f):=direction(f)));F)
= functor-comp(poset-functor(I-[dimension(f)];I-[dimension(v); dimension(f)];(dimension(v):=direction(v)));G)
∈ Functor(poset-cat(I-[dimension(v); dimension(f)]);C)
⊢ (ob(G) L) = (ob(F) L) ∈ cat-ob(C)
BY
{ ApFunToHypEquands `Z' ⌜ob(Z) L⌝ ⌜cat-ob(C)⌝ (-1)⋅ }

1
.....fun wf.....
1. C : SmallCategory
2. I : Cname List
3. J : nameset(I) List
4. x : nameset(I)
5. i : ℕ2
6. box : I-face(cubical-nerve(C);I) List
7. ∀f1,f2:I-face(cubical-nerve(C);I).
     ((f1 ∈ box)
     ⇒ (f2 ∈ box)
     ⇒ (¬(dimension(f1) = dimension(f2) ∈ Cname))
     ⇒ ((dimension(f2):=direction(f2))(cube(f1))
        = (dimension(f1):=direction(f1))(cube(f2))
        ∈ cubical-nerve(C)(I-[dimension(f1); dimension(f2)])))
8. ¬(x ∈ J)
9. l_subset(Cname;J;I)
10. ∀y:nameset(J). ∀c:ℕ2.  (∃f∈box. face-name(f) = <y, c> ∈ (nameset(I) × ℕ2))
11. (∃f∈box. face-name(f) = <x, i> ∈ (nameset(I) × ℕ2))
12. (∀f∈box.¬(face-name(f) = <x, 1 - i> ∈ (nameset(I) × ℕ2)))
13. (∀f∈box.(fst(f) ∈ [x / J]))
14. (∀f1,f2∈box.  ¬(face-name(f1) = face-name(f2) ∈ (nameset(I) × ℕ2)))
15. L : name-morph(I;[])
16. ((L x) = i ∈ ℕ2) ∨ (¬↑null(J))
17. f : I-face(cubical-nerve(C);I)
18. direction(f) = (L dimension(f)) ∈ ℕ2
19. (f ∈ box)
20. v : I-face(cubical-nerve(C);I)
21. (v ∈ box)
22. direction(v) = (L dimension(v)) ∈ ℕ2

23. nerve-box-face(box;L) = v ∈ {f:I-face(cubical-nerve(C);I)| (f ∈ box) ∧ (direction(f) = (L dimension(f)) ∈ ℕ2)}

24. ¬(dimension(v) = dimension(f) ∈ Cname)
25. (dimension(f):=L dimension(f)) ∈ name-morph(I-[dimension(v)];I-[dimension(v); dimension(f)])
26. (dimension(v):=L dimension(v)) ∈ name-morph(I-[dimension(f)];I-[dimension(v); dimension(f)])
27. G : Functor(poset-cat(I-[dimension(f)]);C)
28. F : Functor(poset-cat(I-[dimension(v)]);C)
29. functor-comp(poset-functor(I-[dimension(v)];I-[dimension(v); dimension(f)];(dimension(f):=direction(f)));F)
= functor-comp(poset-functor(I-[dimension(f)];I-[dimension(v); dimension(f)];(dimension(v):=direction(v)));G)
∈ Functor(poset-cat(I-[dimension(v); dimension(f)]);C)
30. Z : Functor(poset-cat(I-[dimension(v); dimension(f)]);C)
⊢ (ob(Z) L) = (ob(Z) L) ∈ 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 : I-face(cubical-nerve(C);I) List
7. ∀f1,f2:I-face(cubical-nerve(C);I).
     ((f1 ∈ box)
     ⇒ (f2 ∈ box)
     ⇒ (¬(dimension(f1) = dimension(f2) ∈ Cname))
     ⇒ ((dimension(f2):=direction(f2))(cube(f1))
        = (dimension(f1):=direction(f1))(cube(f2))
        ∈ cubical-nerve(C)(I-[dimension(f1); dimension(f2)])))
8. ¬(x ∈ J)
9. l_subset(Cname;J;I)
10. ∀y:nameset(J). ∀c:ℕ2.  (∃f∈box. face-name(f) = <y, c> ∈ (nameset(I) × ℕ2))
11. (∃f∈box. face-name(f) = <x, i> ∈ (nameset(I) × ℕ2))
12. (∀f∈box.¬(face-name(f) = <x, 1 - i> ∈ (nameset(I) × ℕ2)))
13. (∀f∈box.(fst(f) ∈ [x / J]))
14. (∀f1,f2∈box.  ¬(face-name(f1) = face-name(f2) ∈ (nameset(I) × ℕ2)))
15. L : name-morph(I;[])
16. ((L x) = i ∈ ℕ2) ∨ (¬↑null(J))
17. f : I-face(cubical-nerve(C);I)
18. direction(f) = (L dimension(f)) ∈ ℕ2
19. (f ∈ box)
20. v : I-face(cubical-nerve(C);I)
21. (v ∈ box)
22. direction(v) = (L dimension(v)) ∈ ℕ2

23. nerve-box-face(box;L) = v ∈ {f:I-face(cubical-nerve(C);I)| (f ∈ box) ∧ (direction(f) = (L dimension(f)) ∈ ℕ2)}

30. (ob(functor-comp(poset-functor(I-[dimension(v)];I-[dimension(v); dimension(f)];(dimension(f):=direction(f)));F)) L)

= (ob(functor-comp(poset-functor(I-[dimension(f)];I-[dimension(v); dimension(f)];(dimension(v):=direction(v)));G)) L)
∈ cat-ob(C)
⊢ (ob(G) L) = (ob(F) L) ∈ cat-ob(C)

Latex:

Latex:
1. C : SmallCategory 2. I : Cname List 3. J : nameset(I) List 4. x : nameset(I) 5. i : \mBbbN{}2 6. box : I-face(cubical-nerve(C);I) List 7. \mforall{}f1,f2:I-face(cubical-nerve(C);I). ((f1 \mmember{} box) {}\mRightarrow{} (f2 \mmember{} box) {}\mRightarrow{} (\mneg{}(dimension(f1) = dimension(f2))) {}\mRightarrow{} ((dimension(f2):=direction(f2))(cube(f1)) = (dimension(f1):=direction(f1))(cube(f2)))) 8. \mneg{}(x \mmember{} J) 9. l\_subset(Cname;J;I) 10. \mforall{}y:nameset(J). \mforall{}c:\mBbbN{}2. (\mexists{}f\mmember{}box. face-name(f) = <y, c>) 11. (\mexists{}f\mmember{}box. face-name(f) = <x, i>) 12. (\mforall{}f\mmember{}box.\mneg{}(face-name(f) = <x, 1 - i>)) 13. (\mforall{}f\mmember{}box.(fst(f) \mmember{} [x / J])) 14. (\mforall{}f1,f2\mmember{}box. \mneg{}(face-name(f1) = face-name(f2))) 15. L : name-morph(I;[]) 16. ((L x) = i) \mvee{} (\mneg{}\muparrow{}null(J)) 17. f : I-face(cubical-nerve(C);I) 18. direction(f) = (L dimension(f)) 19. (f \mmember{} box) 20. v : I-face(cubical-nerve(C);I) 21. (v \mmember{} box) 22. direction(v) = (L dimension(v)) 23. nerve-box-face(box;L) = v 24. \mneg{}(dimension(v) = dimension(f)) 25. (dimension(f):=L dimension(f)) \mmember{} name-morph(I-[dimension(v)];I-[dimension(v); dimension(f)]) 26. (dimension(v):=L dimension(v)) \mmember{} name-morph(I-[dimension(f)];I-[dimension(v); dimension(f)]) 27. G : Functor(poset-cat(I-[dimension(f)]);C) 28. F : Functor(poset-cat(I-[dimension(v)]);C) 29. functor-comp(poset-functor(I-[dimension(v)];I-[dimension(v); dimension(f)];(dimension(f):=direction(f)));F) = functor-comp(poset-functor(I-[dimension(f)];I-[dimension(v); dimension(f)];(dimension(v):=direction(v)));G) \mvdash{} (ob(G) L) = (ob(F) L) By Latex: ApFunToHypEquands `Z' \mkleeneopen{}ob(Z) L\mkleeneclose{} \mkleeneopen{}cat-ob(C)\mkleeneclose{} (-1)\mcdot{} Home Index