---

Step * 1 1 1 1 3 1 1 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 : I-face(cubical-nerve(cat(G));I) List
10. adjacent-compatible(cubical-nerve(cat(G));I;box)
11. ¬(x ∈ J)
12. l_subset(Cname;J;I)
13. ∀y:nameset(J). ∀c:ℕ2.  (∃f∈box. face-name(f) = <y, c> ∈ (nameset(I) × ℕ2))
14. (∃f∈box. face-name(f) = <x, i> ∈ (nameset(I) × ℕ2))
15. (∀f∈box.¬(face-name(f) = <x, 1 - i> ∈ (nameset(I) × ℕ2)))
16. (∀f∈box.(fst(f) ∈ [x / J]))
17. (∀f1,f2∈box.  ¬(face-name(f1) = face-name(f2) ∈ (nameset(I) × ℕ2)))
18. f : name-morph(I;[])
19. a : nameset(I)
20. ¬(a = j ∈ Cname)
21. (f a) = 0 ∈ ℕ2
22. (f j) = 0 ∈ ℕ2
23. (f x) = i ∈ ℤ
24. (flip(f;a) x) = i ∈ ℤ
25. ∀[v:I-face(cubical-nerve(cat(G));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)))) supposing 
         ((v ∈ box) and 
         (¬(dimension(v) = j ∈ Cname)) and 
         (¬(dimension(v) = a ∈ Cname)) and 
         (¬(a = j ∈ nameset(I))) and 
         ((f j) = 0 ∈ ℕ2) and 
         (((f a) = 0 ∈ ℕ2) ∧ (direction(v) = (f dimension(v)) ∈ ℕ2)))
26. get_face(x;i;box) ∈ I-face(cubical-nerve(cat(G));I)
27. (get_face(x;i;box) ∈ box)
28. x1 : nameset(I)
29. v2 : ℕ2
30. v3 : cubical-nerve(cat(G))(I-[x1])
31. get_face(x;i;box) = <x1, v2, v3> ∈ I-face(cubical-nerve(cat(G));I)
32. x1 = x ∈ nameset(I)
33. v2 = i ∈ ℕ2
34. x = j ∈ Cname
⊢ False
BY
{ TACTIC:(Thin (-3) THEN Eliminate ⌜x⌝⋅ THEN Auto) }

---

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  :  I-face(cubical-nerve(cat(G));I)  List
10.  adjacent-compatible(cubical-nerve(cat(G));I;box)
11.  \mneg{}(x  \mmember{}  J)
12.  l\_subset(Cname;J;I)
13.  \mforall{}y:nameset(J).  \mforall{}c:\mBbbN{}2.    (\mexists{}f\mmember{}box.  face-name(f)  =  <y,  c>)
14.  (\mexists{}f\mmember{}box.  face-name(f)  =  <x,  i>)
15.  (\mforall{}f\mmember{}box.\mneg{}(face-name(f)  =  <x,  1  -  i>))
16.  (\mforall{}f\mmember{}box.(fst(f)  \mmember{}  [x  /  J]))
17.  (\mforall{}f1,f2\mmember{}box.    \mneg{}(face-name(f1)  =  face-name(f2)))
18.  f  :  name-morph(I;[])
19.  a  :  nameset(I)
20.  \mneg{}(a  =  j)
21.  (f  a)  =  0
22.  (f  j)  =  0
23.  (f  x)  =  i
24.  (flip(f;a)  x)  =  i
25.  \mforall{}[v:I-face(cubical-nerve(cat(G));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)))  supposing 
                  ((v  \mmember{}  box)  and 
                  (\mneg{}(dimension(v)  =  j))  and 
                  (\mneg{}(dimension(v)  =  a))  and 
                  (\mneg{}(a  =  j))  and 
                  ((f  j)  =  0)  and 
                  (((f  a)  =  0)  \mwedge{}  (direction(v)  =  (f  dimension(v)))))
26.  get\_face(x;i;box)  \mmember{}  I-face(cubical-nerve(cat(G));I)
27.  (get\_face(x;i;box)  \mmember{}  box)
28.  x1  :  nameset(I)
29.  v2  :  \mBbbN{}2
30.  v3  :  cubical-nerve(cat(G))(I-[x1])
31.  get\_face(x;i;box)  =  <x1,  v2,  v3>
32.  x1  =  x
33.  v2  =  i
34.  x  =  j
\mvdash{}  False


By

---

Latex:
TACTIC:(Thin  (-3)  THEN  Eliminate  \mkleeneopen{}x\mkleeneclose{}\mcdot{}  THEN  Auto)

---

Home Index