Step
*
1
1
3
of Lemma
same-face-square-commutes
.....subterm..... T:t
3:n
1. C : SmallCategory
2. I : Cname List
3. J : nameset(I) List
4. (∃j1∈J. (∃j2∈J. ¬(j1 = j2 ∈ Cname)))
5. x : nameset(I)
6. i : ℕ2
7. box : open_box(cubical-nerve(C);I;J;x;i)
8. f : name-morph(I;[])
9. g : name-morph(I;[])
10. h : name-morph(I;[])
11. k : name-morph(I;[])
12. a : nameset(I)
13. b : nameset(I)
14. ¬(a = b ∈ nameset(I))
15. (f a) = 0 ∈ ℕ2
16. (f b) = 0 ∈ ℕ2
17. g = flip(f;a) ∈ name-morph(I;[])
18. h = flip(f;b) ∈ name-morph(I;[])
19. k = flip(flip(f;a);b) ∈ name-morph(I;[])
20. ∃v:I-face(cubical-nerve(C);I)
((v ∈ box)
∧ (¬(dimension(v) = b ∈ Cname))
∧ (¬(dimension(v) = a ∈ Cname))
∧ (direction(v) = (f dimension(v)) ∈ ℕ2))
21. (cat-comp(C) nerve_box_label(box;f) nerve_box_label(box;flip(f;a)) nerve_box_label(box;flip(flip(f;a);b))
nerve_box_edge(box;f;a)
nerve_box_edge(box;flip(f;a);b))
= (cat-comp(C) nerve_box_label(box;f) nerve_box_label(box;flip(f;b)) nerve_box_label(box;flip(flip(f;b);a))
nerve_box_edge(box;f;b)
nerve_box_edge(box;flip(f;b);a))
∈ (cat-arrow(C) nerve_box_label(box;f) nerve_box_label(box;flip(flip(f;a);b)))
22. ¬↑null(J)
23. g = flip(f;a) ∈ {c:name-morph(I;[])| (c b) = 0 ∈ ℕ2}
24. (flip(f;a) b) = 0 ∈ ℕ2
⊢ (cat-comp(C) nerve_box_label(box;f) nerve_box_label(box;h) nerve_box_label(box;k) nerve_box_edge(box;f;b)
nerve_box_edge(box;h;a))
= (cat-comp(C) nerve_box_label(box;f) nerve_box_label(box;flip(f;b)) nerve_box_label(box;flip(flip(f;b);a))
nerve_box_edge(box;f;b)
nerve_box_edge(box;flip(f;b);a))
∈ (cat-arrow(C) nerve_box_label(box;f) nerve_box_label(box;k))
BY
{ (EqCD THEN Try (Trivial) THEN Try ((Fold `member` 0 THEN Auto)) THEN Try (((OrRight THENM Trivial) THEN Auto))) }
1
.....subterm..... T:t
1:n
1. C : SmallCategory
2. I : Cname List
3. J : nameset(I) List
4. (∃j1∈J. (∃j2∈J. ¬(j1 = j2 ∈ Cname)))
5. x : nameset(I)
6. i : ℕ2
7. box : open_box(cubical-nerve(C);I;J;x;i)
8. f : name-morph(I;[])
9. g : name-morph(I;[])
10. h : name-morph(I;[])
11. k : name-morph(I;[])
12. a : nameset(I)
13. b : nameset(I)
14. ¬(a = b ∈ nameset(I))
15. (f a) = 0 ∈ ℕ2
16. (f b) = 0 ∈ ℕ2
17. g = flip(f;a) ∈ name-morph(I;[])
18. h = flip(f;b) ∈ name-morph(I;[])
19. k = flip(flip(f;a);b) ∈ name-morph(I;[])
20. ∃v:I-face(cubical-nerve(C);I)
((v ∈ box)
∧ (¬(dimension(v) = b ∈ Cname))
∧ (¬(dimension(v) = a ∈ Cname))
∧ (direction(v) = (f dimension(v)) ∈ ℕ2))
21. (cat-comp(C) nerve_box_label(box;f) nerve_box_label(box;flip(f;a)) nerve_box_label(box;flip(flip(f;a);b))
nerve_box_edge(box;f;a)
nerve_box_edge(box;flip(f;a);b))
= (cat-comp(C) nerve_box_label(box;f) nerve_box_label(box;flip(f;b)) nerve_box_label(box;flip(flip(f;b);a))
nerve_box_edge(box;f;b)
nerve_box_edge(box;flip(f;b);a))
∈ (cat-arrow(C) nerve_box_label(box;f) nerve_box_label(box;flip(flip(f;a);b)))
22. ¬↑null(J)
23. g = flip(f;a) ∈ {c:name-morph(I;[])| (c b) = 0 ∈ ℕ2}
24. (flip(f;a) b) = 0 ∈ ℕ2
⊢ (cat-comp(C) nerve_box_label(box;f) nerve_box_label(box;h) nerve_box_label(box;k) nerve_box_edge(box;f;b))
= (cat-comp(C) nerve_box_label(box;f) nerve_box_label(box;flip(f;b)) nerve_box_label(box;flip(flip(f;b);a))
nerve_box_edge(box;f;b))
∈ ((cat-arrow(C) nerve_box_label(box;h) nerve_box_label(box;k)) ⟶ (cat-arrow(C) nerve_box_label(box;f)
nerve_box_label(box;k)))
2
.....subterm..... T:t
2:n
1. C : SmallCategory
2. I : Cname List
3. J : nameset(I) List
4. (∃j1∈J. (∃j2∈J. ¬(j1 = j2 ∈ Cname)))
5. x : nameset(I)
6. i : ℕ2
7. box : open_box(cubical-nerve(C);I;J;x;i)
8. f : name-morph(I;[])
9. g : name-morph(I;[])
10. h : name-morph(I;[])
11. k : name-morph(I;[])
12. a : nameset(I)
13. b : nameset(I)
14. ¬(a = b ∈ nameset(I))
15. (f a) = 0 ∈ ℕ2
16. (f b) = 0 ∈ ℕ2
17. g = flip(f;a) ∈ name-morph(I;[])
18. h = flip(f;b) ∈ name-morph(I;[])
19. k = flip(flip(f;a);b) ∈ name-morph(I;[])
20. ∃v:I-face(cubical-nerve(C);I)
((v ∈ box)
∧ (¬(dimension(v) = b ∈ Cname))
∧ (¬(dimension(v) = a ∈ Cname))
∧ (direction(v) = (f dimension(v)) ∈ ℕ2))
21. (cat-comp(C) nerve_box_label(box;f) nerve_box_label(box;flip(f;a)) nerve_box_label(box;flip(flip(f;a);b))
nerve_box_edge(box;f;a)
nerve_box_edge(box;flip(f;a);b))
= (cat-comp(C) nerve_box_label(box;f) nerve_box_label(box;flip(f;b)) nerve_box_label(box;flip(flip(f;b);a))
nerve_box_edge(box;f;b)
nerve_box_edge(box;flip(f;b);a))
∈ (cat-arrow(C) nerve_box_label(box;f) nerve_box_label(box;flip(flip(f;a);b)))
22. ¬↑null(J)
23. g = flip(f;a) ∈ {c:name-morph(I;[])| (c b) = 0 ∈ ℕ2}
24. (flip(f;a) b) = 0 ∈ ℕ2
⊢ nerve_box_edge(box;h;a)
= nerve_box_edge(box;flip(f;b);a)
∈ (cat-arrow(C) nerve_box_label(box;h) nerve_box_label(box;k))
Latex:
Latex:
.....subterm..... T:t
3:n
1. C : SmallCategory
2. I : Cname List
3. J : nameset(I) List
4. (\mexists{}j1\mmember{}J. (\mexists{}j2\mmember{}J. \mneg{}(j1 = j2)))
5. x : nameset(I)
6. i : \mBbbN{}2
7. box : open\_box(cubical-nerve(C);I;J;x;i)
8. f : name-morph(I;[])
9. g : name-morph(I;[])
10. h : name-morph(I;[])
11. k : name-morph(I;[])
12. a : nameset(I)
13. b : nameset(I)
14. \mneg{}(a = b)
15. (f a) = 0
16. (f b) = 0
17. g = flip(f;a)
18. h = flip(f;b)
19. k = flip(flip(f;a);b)
20. \mexists{}v:I-face(cubical-nerve(C);I)
((v \mmember{} box) \mwedge{} (\mneg{}(dimension(v) = b)) \mwedge{} (\mneg{}(dimension(v) = a)) \mwedge{} (direction(v) = (f dimension(v))))
21. (cat-comp(C) nerve\_box\_label(box;f) nerve\_box\_label(box;flip(f;a))
nerve\_box\_label(box;flip(flip(f;a);b))
nerve\_box\_edge(box;f;a)
nerve\_box\_edge(box;flip(f;a);b))
= (cat-comp(C) nerve\_box\_label(box;f) nerve\_box\_label(box;flip(f;b))
nerve\_box\_label(box;flip(flip(f;b);a))
nerve\_box\_edge(box;f;b)
nerve\_box\_edge(box;flip(f;b);a))
22. \mneg{}\muparrow{}null(J)
23. g = flip(f;a)
24. (flip(f;a) b) = 0
\mvdash{} (cat-comp(C) nerve\_box\_label(box;f) nerve\_box\_label(box;h) nerve\_box\_label(box;k)
nerve\_box\_edge(box;f;b)
nerve\_box\_edge(box;h;a))
= (cat-comp(C) nerve\_box\_label(box;f) nerve\_box\_label(box;flip(f;b))
nerve\_box\_label(box;flip(flip(f;b);a))
nerve\_box\_edge(box;f;b)
nerve\_box\_edge(box;flip(f;b);a))
By
Latex:
(EqCD
THEN Try (Trivial)
THEN Try ((Fold `member` 0 THEN Auto))
THEN Try (((OrRight THENM Trivial) THEN Auto)))
Home
Index