Proof of Nuprl Lemma : groupoid-edges-commute1

Step * 1 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(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)))
BY
{ ((BoolCase ⌜(f x =_z i)⌝⋅ THENA Auto) THEN (BoolCase ⌜(flip(f;a) x =_z i)⌝⋅ THENA Auto)) }

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
15. (f x) = i ∈ ℤ
16. (flip(f;a) x) = 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);j))
   nerve_box_edge(box;f;a)
   nerve_box_edge(box;flip(f;a);j))
= (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))
   nerve_box_edge(box;f;j)
   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. flip(f;a) x ≠ i
13. ¬(a = j ∈ Cname)
14. (f a) = 0 ∈ ℕ2
15. (f j) = 0 ∈ ℕ2
16. (f x) = 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);j))
   nerve_box_edge(box;f;a)
   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(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))
   nerve_box_edge(box;f;j)
   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)))

3
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. f x ≠ i
12. a : nameset(I)
13. ¬(a = j ∈ Cname)
14. (f a) = 0 ∈ ℕ2
15. (f j) = 0 ∈ ℕ2
16. (flip(f;a) x) = 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);j))
   nerve_box_edge(box;f;a)
   nerve_box_edge(box;flip(f;a);j))
= (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 (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)))

4
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. f x ≠ i
12. a : nameset(I)
13. flip(f;a) x ≠ i
14. ¬(a = j ∈ Cname)
15. (f a) = 0 ∈ ℕ2
16. (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 (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(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 (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);

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(cat(G));I;J;x;i) 10. f : name-morph(I;[]) 11. a : nameset(I) 12. \mneg{}(a = j) 13. (f a) = 0 14. (f j) = 0 \mvdash{} (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 =\msubz{} i) then nerve\_box\_edge(box;flip(f;a);j) if (i =\msubz{} 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 =\msubz{} i) then nerve\_box\_edge(box;f;j) if (i =\msubz{} 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)) By Latex: ((BoolCase \mkleeneopen{}(f x =\msubz{} i)\mkleeneclose{}\mcdot{} THENA Auto) THEN (BoolCase \mkleeneopen{}(flip(f;a) x =\msubz{} i)\mkleeneclose{}\mcdot{} THENA Auto)) Home Index