Step
*
2
2
1
1
1
1
of Lemma
groupoid-edges-commute
1. G : Groupoid
2. I : Cname List
3. J : nameset(I) List
4. x : nameset(I)
5. i : ℕ2
6. box : open_box(cubical-nerve(fst(G));I;J;x;i)
7. (∃j1∈J. (∃j2∈J. ¬(j1 = j2 ∈ Cname)))
8. f : name-morph(I;[])
9. a : nameset(I)
10. (f a) = 0 ∈ ℕ2
11. b : nameset(I)
12. (f b) = 0 ∈ ℕ2
13. ¬(a = b ∈ nameset(I))
14. ¬(∃v∈box. (¬(dimension(v) = b ∈ Cname)) ∧ (¬(dimension(v) = a ∈ Cname)) ∧ (direction(v) = (f dimension(v)) ∈ ℕ2))
15. (∀j∈J.(j = a ∈ Cname) ∨ (j = b ∈ Cname))
16. (a ∈ J) ∧ (b ∈ J) ∧ (¬(x = a ∈ Cname)) ∧ (¬(x = b ∈ Cname))
17. ¬((f x) = i ∈ ℕ2)
18. eq-cname(a;b) ~ ff
19. eq-cname(b;a) ~ eq-cname(a;b)
20. (((flip(f;x) a) = 0 ∈ ℕ2) ∧ ((flip(f;b) a) = 0 ∈ ℕ2))
∧ (((flip(f;x) b) = 0 ∈ ℕ2) ∧ ((flip(f;a) b) = 0 ∈ ℕ2))
∧ ((flip(flip(f;x);b) a) = 0 ∈ ℕ2)
∧ ((flip(flip(f;x);a) b) = 0 ∈ ℕ2)
⊢ (cat-comp(fst(G)) 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(fst(G)) 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(fst(G)) nerve_box_label(box;f) nerve_box_label(box;flip(flip(f;a);b)))
BY
{ (ExRepD
THEN (InstLemma `groupoid-cube-lemma2`
[⌜G⌝
;⌜nerve_box_label(box;f)⌝
; ⌜nerve_box_label(box;flip(f;a))⌝
; ⌜nerve_box_label(box;flip(f;b))⌝
; ⌜nerve_box_label(box;flip(flip(f;a);b))⌝
; ⌜nerve_box_label(box;flip(f;x))⌝
; ⌜nerve_box_label(box;flip(flip(f;x);a))⌝
; ⌜nerve_box_label(box;flip(flip(f;x);b))⌝
; ⌜nerve_box_label(box;flip(flip(flip(f;x);a);b))⌝
; ⌜nerve_box_edge(box;flip(f;x);b)⌝
; ⌜nerve_box_edge(box;flip(flip(f;x);b);a)⌝
; ⌜nerve_box_edge(box;flip(f;x);a)⌝
; ⌜nerve_box_edge(box;flip(flip(f;x);a);b)⌝
; ⌜nerve_box_edge(box;f;b)⌝
; ⌜nerve_box_edge(box;flip(f;b);a)⌝
; ⌜nerve_box_edge(box;f;a)⌝
; ⌜nerve_box_edge(box;flip(f;a);b)⌝
]⋅
THENA (Auto THEN Try ((DoSubsume THEN Try (BLemma `subtype_rel-equal`) THEN Auto)))
)
) }
1
.....antecedent.....
1. G : Groupoid
2. I : Cname List
3. J : nameset(I) List
4. x : nameset(I)
5. i : ℕ2
6. box : open_box(cubical-nerve(fst(G));I;J;x;i)
7. (∃j1∈J. (∃j2∈J. ¬(j1 = j2 ∈ Cname)))
8. f : name-morph(I;[])
9. a : nameset(I)
10. (f a) = 0 ∈ ℕ2
11. b : nameset(I)
12. (f b) = 0 ∈ ℕ2
13. ¬(a = b ∈ nameset(I))
14. ¬(∃v∈box. (¬(dimension(v) = b ∈ Cname)) ∧ (¬(dimension(v) = a ∈ Cname)) ∧ (direction(v) = (f dimension(v)) ∈ ℕ2))
15. (∀j∈J.(j = a ∈ Cname) ∨ (j = b ∈ Cname))
16. (a ∈ J)
17. (b ∈ J)
18. ¬(x = a ∈ Cname)
19. ¬(x = b ∈ Cname)
20. ¬((f x) = i ∈ ℕ2)
21. eq-cname(a;b) ~ ff
22. eq-cname(b;a) ~ eq-cname(a;b)
23. (flip(f;x) a) = 0 ∈ ℕ2
24. (flip(f;b) a) = 0 ∈ ℕ2
25. (flip(f;x) b) = 0 ∈ ℕ2
26. (flip(f;a) b) = 0 ∈ ℕ2
27. (flip(flip(f;x);b) a) = 0 ∈ ℕ2
28. (flip(flip(f;x);a) b) = 0 ∈ ℕ2
⊢ (∃i:cat-arrow(cat(G)) nerve_box_label(box;f) nerve_box_label(box;flip(f;x))
∃j:cat-arrow(cat(G)) nerve_box_label(box;flip(f;b)) nerve_box_label(box;flip(flip(f;x);b))
∃k:cat-arrow(cat(G)) nerve_box_label(box;flip(flip(f;a);b)) nerve_box_label(box;flip(flip(flip(f;x);a);b))
∃l:cat-arrow(cat(G)) nerve_box_label(box;flip(f;a)) nerve_box_label(box;flip(flip(f;x);a))
(nerve_box_edge(box;f;b) o j = i o nerve_box_edge(box;flip(f;x);b)
∧ nerve_box_edge(box;flip(f;b);a) o k = j o nerve_box_edge(box;flip(flip(f;x);b);a)
∧ l o nerve_box_edge(box;flip(flip(f;x);a);b) = nerve_box_edge(box;flip(f;a);b) o k
∧ i o nerve_box_edge(box;flip(f;x);a) = nerve_box_edge(box;f;a) o l))
∨ (∃i:cat-arrow(cat(G)) nerve_box_label(box;flip(f;x)) nerve_box_label(box;f)
∃j:cat-arrow(cat(G)) nerve_box_label(box;flip(flip(f;x);b)) nerve_box_label(box;flip(f;b))
∃k:cat-arrow(cat(G)) nerve_box_label(box;flip(flip(flip(f;x);a);b)) nerve_box_label(box;flip(flip(f;a);b))
∃l:cat-arrow(cat(G)) nerve_box_label(box;flip(flip(f;x);a)) nerve_box_label(box;flip(f;a))
(nerve_box_edge(box;flip(f;x);b) o j = i o nerve_box_edge(box;f;b)
∧ nerve_box_edge(box;flip(flip(f;x);b);a) o k = j o nerve_box_edge(box;flip(f;b);a)
∧ nerve_box_edge(box;flip(flip(f;x);a);b) o k = l o nerve_box_edge(box;flip(f;a);b)
∧ i o nerve_box_edge(box;f;a) = nerve_box_edge(box;flip(f;x);a) o l))
2
1. G : Groupoid
2. I : Cname List
3. J : nameset(I) List
4. x : nameset(I)
5. i : ℕ2
6. box : open_box(cubical-nerve(fst(G));I;J;x;i)
7. (∃j1∈J. (∃j2∈J. ¬(j1 = j2 ∈ Cname)))
8. f : name-morph(I;[])
9. a : nameset(I)
10. (f a) = 0 ∈ ℕ2
11. b : nameset(I)
12. (f b) = 0 ∈ ℕ2
13. ¬(a = b ∈ nameset(I))
14. ¬(∃v∈box. (¬(dimension(v) = b ∈ Cname)) ∧ (¬(dimension(v) = a ∈ Cname)) ∧ (direction(v) = (f dimension(v)) ∈ ℕ2))
15. (∀j∈J.(j = a ∈ Cname) ∨ (j = b ∈ Cname))
16. (a ∈ J)
17. (b ∈ J)
18. ¬(x = a ∈ Cname)
19. ¬(x = b ∈ Cname)
20. ¬((f x) = i ∈ ℕ2)
21. eq-cname(a;b) ~ ff
22. eq-cname(b;a) ~ eq-cname(a;b)
23. (flip(f;x) a) = 0 ∈ ℕ2
24. (flip(f;b) a) = 0 ∈ ℕ2
25. (flip(f;x) b) = 0 ∈ ℕ2
26. (flip(f;a) b) = 0 ∈ ℕ2
27. (flip(flip(f;x);b) a) = 0 ∈ ℕ2
28. (flip(flip(f;x);a) b) = 0 ∈ ℕ2
29. uiff(nerve_box_edge(box;flip(f;x);b) o nerve_box_edge(box;flip(flip(f;x);b);a)
= nerve_box_edge(box;flip(f;x);a) o nerve_box_edge(box;flip(flip(f;x);a);b);nerve_box_edge(box;f;b) o ...
= nerve_box_edge(box;f;a) o ...)
⊢ (cat-comp(fst(G)) 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(fst(G)) 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(fst(G)) nerve_box_label(box;f) nerve_box_label(box;flip(flip(f;a);b)))
Latex:
Latex:
1. G : Groupoid
2. I : Cname List
3. J : nameset(I) List
4. x : nameset(I)
5. i : \mBbbN{}2
6. box : open\_box(cubical-nerve(fst(G));I;J;x;i)
7. (\mexists{}j1\mmember{}J. (\mexists{}j2\mmember{}J. \mneg{}(j1 = j2)))
8. f : name-morph(I;[])
9. a : nameset(I)
10. (f a) = 0
11. b : nameset(I)
12. (f b) = 0
13. \mneg{}(a = b)
14. \mneg{}(\mexists{}v\mmember{}box. (\mneg{}(dimension(v) = b)) \mwedge{} (\mneg{}(dimension(v) = a)) \mwedge{} (direction(v) = (f dimension(v))))
15. (\mforall{}j\mmember{}J.(j = a) \mvee{} (j = b))
16. (a \mmember{} J) \mwedge{} (b \mmember{} J) \mwedge{} (\mneg{}(x = a)) \mwedge{} (\mneg{}(x = b))
17. \mneg{}((f x) = i)
18. eq-cname(a;b) \msim{} ff
19. eq-cname(b;a) \msim{} eq-cname(a;b)
20. (((flip(f;x) a) = 0) \mwedge{} ((flip(f;b) a) = 0))
\mwedge{} (((flip(f;x) b) = 0) \mwedge{} ((flip(f;a) b) = 0))
\mwedge{} ((flip(flip(f;x);b) a) = 0)
\mwedge{} ((flip(flip(f;x);a) b) = 0)
\mvdash{} (cat-comp(fst(G)) 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(fst(G)) 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:
(ExRepD
THEN (InstLemma `groupoid-cube-lemma2`
[\mkleeneopen{}G\mkleeneclose{}
;\mkleeneopen{}nerve\_box\_label(box;f)\mkleeneclose{}
; \mkleeneopen{}nerve\_box\_label(box;flip(f;a))\mkleeneclose{}
; \mkleeneopen{}nerve\_box\_label(box;flip(f;b))\mkleeneclose{}
; \mkleeneopen{}nerve\_box\_label(box;flip(flip(f;a);b))\mkleeneclose{}
; \mkleeneopen{}nerve\_box\_label(box;flip(f;x))\mkleeneclose{}
; \mkleeneopen{}nerve\_box\_label(box;flip(flip(f;x);a))\mkleeneclose{}
; \mkleeneopen{}nerve\_box\_label(box;flip(flip(f;x);b))\mkleeneclose{}
; \mkleeneopen{}nerve\_box\_label(box;flip(flip(flip(f;x);a);b))\mkleeneclose{}
; \mkleeneopen{}nerve\_box\_edge(box;flip(f;x);b)\mkleeneclose{}
; \mkleeneopen{}nerve\_box\_edge(box;flip(flip(f;x);b);a)\mkleeneclose{}
; \mkleeneopen{}nerve\_box\_edge(box;flip(f;x);a)\mkleeneclose{}
; \mkleeneopen{}nerve\_box\_edge(box;flip(flip(f;x);a);b)\mkleeneclose{}
; \mkleeneopen{}nerve\_box\_edge(box;f;b)\mkleeneclose{}
; \mkleeneopen{}nerve\_box\_edge(box;flip(f;b);a)\mkleeneclose{}
; \mkleeneopen{}nerve\_box\_edge(box;f;a)\mkleeneclose{}
; \mkleeneopen{}nerve\_box\_edge(box;flip(f;a);b)\mkleeneclose{}
]\mcdot{}
THENA (Auto THEN Try ((DoSubsume THEN Try (BLemma `subtype\_rel-equal`) THEN Auto)))
)
)
Home
Index