Step
*
1
of Lemma
groupoid-edges-commute1
1. G : Groupoid
2. I : Cname List
3. J : nameset(I) List
4. j : nameset(I)
5. (j ∈ J)
6. (∀j'∈J.j' = j ∈ Cname)
7. x : nameset(I)
8. i : ℕ2
9. box : open_box(cubical-nerve(fst(G));I;J;x;i)
10. f : name-morph(I;[])
11. a : nameset(I)
12. (f a) = 0 ∈ ℕ2
13. b : nameset(I)
14. (f b) = 0 ∈ ℕ2
15. ¬(a = b ∈ nameset(I))
⊢ (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_edge1(G;box;x;i;j;f;a)
nerve_box_edge1(G;box;x;i;j;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_edge1(G;box;x;i;j;f;b)
nerve_box_edge1(G;box;x;i;j;flip(f;b);a))
∈ (cat-arrow(fst(G)) nerve_box_label(box;f) nerve_box_label(box;flip(flip(f;a);b)))
BY
{ ((Unfold `nerve_box_edge1` 0
THEN (BoolCase ⌜eq-cname(a;j)⌝⋅ THENA Auto)
THEN (BoolCase ⌜eq-cname(b;j)⌝⋅ THENA Auto)
THEN Try ((D -3 THEN HypSubst' (-2) 0 THEN HypSubst' (-1) 0 THEN Fold `member` 0 THEN Auto))
THEN (RWW "bor-btrue bor-bfalse" 0 THENA Auto)
THEN (Reduce 0 THEN All (Fold `groupoid-cat`))
THEN Try ((MoveToConcl (-3)
THEN HypSubst' (-1) 0
THEN ThinVar `b'
THEN RenameVar `%a' (-2)
THEN RenameVar `%b' (-1)
THEN (D 0 THENA Auto)))
THEN Try ((MoveToConcl(-6)
THEN HypSubst' (-1) 0
THEN ThinVar `a'
THEN RenameVar `%a' (-2)
THEN RenameVar `%b' (-1)
THEN (D 0 THENA Auto)
THEN RenameTo `a' `b'
THEN Symmetry
THEN SubsumeC ⌜cat-arrow(cat(G)) nerve_box_label(box;f) nerve_box_label(box;flip(flip(f;a);j))⌝⋅
THEN Try ((BLemma `subtype_rel-equal` THEN Auto)))))
THEN Id
) }
1
1. G : Groupoid
2. I : Cname List
3. J : nameset(I) List
4. j : nameset(I)
5. (j ∈ J)
6. (∀j'∈J.j' = j ∈ Cname)
7. x : nameset(I)
8. i : ℕ2
9. box : open_box(cubical-nerve(cat(G));I;J;x;i)
10. f : name-morph(I;[])
11. a : nameset(I)
12. ¬(a = j ∈ Cname)
13. (f a) = 0 ∈ ℕ2
14. (f j) = 0 ∈ ℕ2
⊢ (cat-comp(cat(G)) nerve_box_label(box;f) nerve_box_label(box;flip(f;a)) nerve_box_label(box;flip(flip(f;a);j))
nerve_box_edge(box;f;a)
if (flip(f;a) x =z i) then nerve_box_edge(box;flip(f;a);j)
if (i =z 0)
then groupoid-square1(G;nerve_box_label(box;flip(flip(f;a);x));nerve_box_label(box;flip(flip(flip(f;a);x);j));
nerve_box_label(box;flip(f;a));nerve_box_label(box;flip(flip(f;a);j));nerve_box_edge(box;flip(flip(f;a);x);j);
nerve_box_edge(box;flip(flip(flip(f;a);x);j);x);nerve_box_edge(box;flip(flip(f;a);x);x))
else groupoid-square2(G;nerve_box_label(box;flip(f;a));nerve_box_label(box;flip(flip(f;a);j));
nerve_box_label(box;flip(flip(f;a);x));nerve_box_label(box;flip(flip(flip(f;a);j);x));
nerve_box_edge(box;flip(flip(f;a);j);x);nerve_box_edge(box;flip(f;a);x);nerve_box_edge(box;flip(flip(f;a);x);j))
fi )
= (cat-comp(cat(G)) nerve_box_label(box;f) nerve_box_label(box;flip(f;j)) nerve_box_label(box;flip(flip(f;j);a))
if (f x =z i) then nerve_box_edge(box;f;j)
if (i =z 0)
then groupoid-square1(G;nerve_box_label(box;flip(f;x));nerve_box_label(box;flip(flip(f;x);j));
nerve_box_label(box;f);nerve_box_label(box;flip(f;j));nerve_box_edge(box;flip(f;x);j);
nerve_box_edge(box;flip(flip(f;x);j);x);nerve_box_edge(box;flip(f;x);x))
else groupoid-square2(G;nerve_box_label(box;f);nerve_box_label(box;flip(f;j));
nerve_box_label(box;flip(f;x));nerve_box_label(box;flip(flip(f;j);x));nerve_box_edge(box;flip(f;j);x);
nerve_box_edge(box;f;x);nerve_box_edge(box;flip(f;x);j))
fi
nerve_box_edge(box;flip(f;j);a))
∈ (cat-arrow(cat(G)) nerve_box_label(box;f) nerve_box_label(box;flip(flip(f;a);j)))
2
1. G : Groupoid
2. I : Cname List
3. J : nameset(I) List
4. j : nameset(I)
5. (j ∈ J)
6. (∀j'∈J.j' = j ∈ Cname)
7. x : nameset(I)
8. i : ℕ2
9. box : open_box(cubical-nerve(cat(G));I;J;x;i)
10. f : name-morph(I;[])
11. a : nameset(I)
12. ¬(a = j ∈ Cname)
13. (f a) = 0 ∈ ℕ2
14. b : nameset(I)
15. ¬(b = j ∈ Cname)
16. (f b) = 0 ∈ ℕ2
17. ¬(a = b ∈ nameset(I))
⊢ (cat-comp(cat(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(cat(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(cat(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. j : nameset(I)
5. (j \mmember{} J)
6. (\mforall{}j'\mmember{}J.j' = j)
7. x : nameset(I)
8. i : \mBbbN{}2
9. box : open\_box(cubical-nerve(fst(G));I;J;x;i)
10. f : name-morph(I;[])
11. a : nameset(I)
12. (f a) = 0
13. b : nameset(I)
14. (f b) = 0
15. \mneg{}(a = b)
\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\_edge1(G;box;x;i;j;f;a)
nerve\_box\_edge1(G;box;x;i;j;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\_edge1(G;box;x;i;j;f;b)
nerve\_box\_edge1(G;box;x;i;j;flip(f;b);a))
By
Latex:
((Unfold `nerve\_box\_edge1` 0
THEN (BoolCase \mkleeneopen{}eq-cname(a;j)\mkleeneclose{}\mcdot{} THENA Auto)
THEN (BoolCase \mkleeneopen{}eq-cname(b;j)\mkleeneclose{}\mcdot{} THENA Auto)
THEN Try ((D -3 THEN HypSubst' (-2) 0 THEN HypSubst' (-1) 0 THEN Fold `member` 0 THEN Auto))
THEN (RWW "bor-btrue bor-bfalse" 0 THENA Auto)
THEN (Reduce 0 THEN All (Fold `groupoid-cat`))
THEN Try ((MoveToConcl (-3)
THEN HypSubst' (-1) 0
THEN ThinVar `b'
THEN RenameVar `\%a' (-2)
THEN RenameVar `\%b' (-1)
THEN (D 0 THENA Auto)))
THEN Try ((MoveToConcl(-6)
THEN HypSubst' (-1) 0
THEN ThinVar `a'
THEN RenameVar `\%a' (-2)
THEN RenameVar `\%b' (-1)
THEN (D 0 THENA Auto)
THEN RenameTo `a' `b'
THEN Symmetry
THEN SubsumeC \mkleeneopen{}cat-arrow(cat(G)) nerve\_box\_label(box;f)
nerve\_box\_label(box;flip(flip(f;a);j))\mkleeneclose{}\mcdot{}
THEN Try ((BLemma `subtype\_rel-equal` THEN Auto)))))
THEN Id
)
Home
Index