Proof of Nuprl Lemma : groupoid-edges-commute

Step * 2 2 1 1 1 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)
17. (b ∈ J)
18. ¬(x = a ∈ Cname)
19. ¬(x = b ∈ Cname)
20. ¬((f x) = i ∈ ℕ2)
21. (flip(f;x) a) = 0 ∈ ℕ2
22. (flip(f;b) a) = 0 ∈ ℕ2
23. (flip(f;x) b) = 0 ∈ ℕ2
24. (flip(f;a) b) = 0 ∈ ℕ2
25. (flip(flip(f;x);b) a) = 0 ∈ ℕ2
26. (flip(flip(f;x);a) b) = 0 ∈ ℕ2
27. (i = 1 ∈ ℕ2) ∧ ((f x) = 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)
BY
{ (D -1
   THEN (Assert eq-cname(x;a) ~ ff BY
               (BoolCase ⌜eq-cname(x;a)⌝⋅ THEN Auto))
   THEN (Assert eq-cname(x;b) ~ ff BY
               (BoolCase ⌜eq-cname(x;b)⌝⋅ THEN Auto))
   THEN (Assert ((flip(f;a) x) = 0 ∈ ℕ2)
               ∧ ((flip(f;b) x) = 0 ∈ ℕ2)
               ∧ ((flip(flip(f;a);b) x) = 0 ∈ ℕ2)
               ∧ ((flip(flip(f;b);a) x) = 0 ∈ ℕ2) BY
               (SplitAndConcl
                THEN RepUR ``name-morph-flip`` 0
                THEN Try (HypSubst' (-2) 0)
                THEN Try (HypSubst' (-1) 0)
                THEN Reduce 0
                THEN Try (HypSubst' (-3) 0)
                THEN Try ((Fold `member` 0 THEN Auto))))) }

1
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))

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) 17. (b \mmember{} J) 18. \mneg{}(x = a) 19. \mneg{}(x = b) 20. \mneg{}((f x) = i) 21. (flip(f;x) a) = 0 22. (flip(f;b) a) = 0 23. (flip(f;x) b) = 0 24. (flip(f;a) b) = 0 25. (flip(flip(f;x);b) a) = 0 26. (flip(flip(f;x);a) b) = 0 27. (i = 1) \mwedge{} ((f x) = 0) \mvdash{} \mexists{}i:cat-arrow(cat(G)) nerve\_box\_label(box;f) nerve\_box\_label(box;flip(f;x)) \mexists{}j:cat-arrow(cat(G)) nerve\_box\_label(box;flip(f;b)) nerve\_box\_label(box;flip(flip(f;x);b)) \mexists{}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)) \mexists{}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) \mwedge{} nerve\_box\_edge(box;flip(f;b);a) o k = j o nerve\_box\_edge(box;flip(flip(f;x);b);a) \mwedge{} l o nerve\_box\_edge(box;flip(flip(f;x);a);b) = nerve\_box\_edge(box;flip(f;a);b) o k \mwedge{} i o nerve\_box\_edge(box;flip(f;x);a) = nerve\_box\_edge(box;f;a) o l) By Latex: (D -1 THEN (Assert eq-cname(x;a) \msim{} ff BY (BoolCase \mkleeneopen{}eq-cname(x;a)\mkleeneclose{}\mcdot{} THEN Auto)) THEN (Assert eq-cname(x;b) \msim{} ff BY (BoolCase \mkleeneopen{}eq-cname(x;b)\mkleeneclose{}\mcdot{} THEN Auto)) THEN (Assert ((flip(f;a) x) = 0) \mwedge{} ((flip(f;b) x) = 0) \mwedge{} ((flip(flip(f;a);b) x) = 0) \mwedge{} ((flip(flip(f;b);a) x) = 0) BY (SplitAndConcl THEN RepUR ``name-morph-flip`` 0 THEN Try (HypSubst' (-2) 0) THEN Try (HypSubst' (-1) 0) THEN Reduce 0 THEN Try (HypSubst' (-3) 0) THEN Try ((Fold `member` 0 THEN Auto))))) Home Index