---

Step * 1 3 of Lemma same-face-edge-arrows-commute0

.....subterm..... T:t
3:n
1. C : SmallCategory
2. I : Cname List
3. J : nameset(I) List
4. x : nameset(I)
5. i : ℕ2
6. box : open_box(cubical-nerve(C);I;J;x;i)
7. f : name-morph(I;[])
8. a : nameset(I)
9. b : nameset(I)
10. ((∃j1∈J. ¬(j1 = a ∈ Cname)) ∧ (∃j2∈J. ¬(j2 = b ∈ Cname)))
∨ ((¬↑null(J)) ∧ ((f x) = i ∈ ℤ) ∧ ((flip(f;a) x) = i ∈ ℤ) ∧ ((flip(f;b) x) = i ∈ ℕ2))
11. v : I-face(cubical-nerve(C);I)
12. (f a) = 0 ∈ ℕ2
13. direction(v) = (f dimension(v)) ∈ ℕ2
14. (f b) = 0 ∈ ℕ2
15. ¬(a = b ∈ nameset(I))
16. ¬(dimension(v) = a ∈ Cname)
17. ¬(dimension(v) = b ∈ Cname)
18. (v ∈ box)
19. ¬↑null(J)
20. ((ob(cube(v)) flip(flip(f;a);b)) = nerve_box_label(box;flip(flip(f;a);b)) ∈ cat-ob(C))
∧ ((ob(cube(v)) f) = nerve_box_label(box;f) ∈ cat-ob(C))
∧ ((ob(cube(v)) flip(f;a)) = nerve_box_label(box;flip(f;a)) ∈ cat-ob(C))
∧ ((ob(cube(v)) flip(f;b)) = nerve_box_label(box;flip(f;b)) ∈ cat-ob(C))
∧ ((ob(cube(v)) flip(flip(f;b);a)) = nerve_box_label(box;flip(flip(f;b);a)) ∈ cat-ob(C))
21. (cat-comp(C) (ob(cube(v)) f) (ob(cube(v)) flip(f;a)) (ob(cube(v)) flip(flip(f;a);b)) 
     (arrow(cube(v)) f flip(f;a) (λx.Ax)) 
     (arrow(cube(v)) flip(f;a) flip(flip(f;a);b) (λx.Ax)))
= (cat-comp(C) (ob(cube(v)) f) (ob(cube(v)) flip(f;b)) (ob(cube(v)) flip(flip(f;b);a)) 
   (arrow(cube(v)) f flip(f;b) (λx.Ax)) 
   (arrow(cube(v)) flip(f;b) flip(flip(f;b);a) (λx.Ax)))
∈ (cat-arrow(C) (ob(cube(v)) f) (ob(cube(v)) flip(flip(f;a);b)))
⊢ (cat-comp(C) (ob(cube(v)) f) (ob(cube(v)) flip(f;b)) (ob(cube(v)) flip(flip(f;b);a)) 
   (arrow(cube(v)) f flip(f;b) (λx.Ax)) 
   (arrow(cube(v)) flip(f;b) flip(flip(f;b);a) (λx.Ax)))
= (cat-comp(C) 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(C) (ob(cube(v)) f) (ob(cube(v)) flip(flip(f;a);b)))
BY
{ (SubsumeC ⌜cat-arrow(C) (ob(cube(v)) f) (ob(cube(v)) flip(flip(f;b);a))⌝⋅
   THEN Try ((BLemma `subtype_rel-equal` THEN Auto))
   THEN SplitAndHyps
   THEN Repeat (EqCD)
   THEN Try (Trivial)) }

1
.....subterm..... T:t
2:n
1. C : SmallCategory
2. I : Cname List
3. J : nameset(I) List
4. x : nameset(I)
5. i : ℕ2
6. box : open_box(cubical-nerve(C);I;J;x;i)
7. f : name-morph(I;[])
8. a : nameset(I)
9. b : nameset(I)
10. ((∃j1∈J. ¬(j1 = a ∈ Cname)) ∧ (∃j2∈J. ¬(j2 = b ∈ Cname)))
∨ ((¬↑null(J)) ∧ ((f x) = i ∈ ℤ) ∧ ((flip(f;a) x) = i ∈ ℤ) ∧ ((flip(f;b) x) = i ∈ ℕ2))
11. v : I-face(cubical-nerve(C);I)
12. (f a) = 0 ∈ ℕ2
13. direction(v) = (f dimension(v)) ∈ ℕ2
14. (f b) = 0 ∈ ℕ2
15. ¬(a = b ∈ nameset(I))
16. ¬(dimension(v) = a ∈ Cname)
17. ¬(dimension(v) = b ∈ Cname)
18. (v ∈ box)
19. ¬↑null(J)
20. (ob(cube(v)) flip(flip(f;a);b)) = nerve_box_label(box;flip(flip(f;a);b)) ∈ cat-ob(C)
21. (ob(cube(v)) f) = nerve_box_label(box;f) ∈ cat-ob(C)
22. (ob(cube(v)) flip(f;a)) = nerve_box_label(box;flip(f;a)) ∈ cat-ob(C)
23. (ob(cube(v)) flip(f;b)) = nerve_box_label(box;flip(f;b)) ∈ cat-ob(C)
24. (ob(cube(v)) flip(flip(f;b);a)) = nerve_box_label(box;flip(flip(f;b);a)) ∈ cat-ob(C)
25. (cat-comp(C) (ob(cube(v)) f) (ob(cube(v)) flip(f;a)) (ob(cube(v)) flip(flip(f;a);b)) 
     (arrow(cube(v)) f flip(f;a) (λx.Ax)) 
     (arrow(cube(v)) flip(f;a) flip(flip(f;a);b) (λx.Ax)))
= (cat-comp(C) (ob(cube(v)) f) (ob(cube(v)) flip(f;b)) (ob(cube(v)) flip(flip(f;b);a)) 
   (arrow(cube(v)) f flip(f;b) (λx.Ax)) 
   (arrow(cube(v)) flip(f;b) flip(flip(f;b);a) (λx.Ax)))
∈ (cat-arrow(C) (ob(cube(v)) f) (ob(cube(v)) flip(flip(f;a);b)))
⊢ (arrow(cube(v)) f flip(f;b) (λx.Ax))
= nerve_box_edge(box;f;b)
∈ (cat-arrow(C) (ob(cube(v)) f) (ob(cube(v)) flip(f;b)))

2
.....subterm..... T:t
2:n
1. C : SmallCategory
2. I : Cname List
3. J : nameset(I) List
4. x : nameset(I)
5. i : ℕ2
6. box : open_box(cubical-nerve(C);I;J;x;i)
7. f : name-morph(I;[])
8. a : nameset(I)
9. b : nameset(I)
10. ((∃j1∈J. ¬(j1 = a ∈ Cname)) ∧ (∃j2∈J. ¬(j2 = b ∈ Cname)))
∨ ((¬↑null(J)) ∧ ((f x) = i ∈ ℤ) ∧ ((flip(f;a) x) = i ∈ ℤ) ∧ ((flip(f;b) x) = i ∈ ℕ2))
11. v : I-face(cubical-nerve(C);I)
12. (f a) = 0 ∈ ℕ2
13. direction(v) = (f dimension(v)) ∈ ℕ2
14. (f b) = 0 ∈ ℕ2
15. ¬(a = b ∈ nameset(I))
16. ¬(dimension(v) = a ∈ Cname)
17. ¬(dimension(v) = b ∈ Cname)
18. (v ∈ box)
19. ¬↑null(J)
20. (ob(cube(v)) flip(flip(f;a);b)) = nerve_box_label(box;flip(flip(f;a);b)) ∈ cat-ob(C)
21. (ob(cube(v)) f) = nerve_box_label(box;f) ∈ cat-ob(C)
22. (ob(cube(v)) flip(f;a)) = nerve_box_label(box;flip(f;a)) ∈ cat-ob(C)
23. (ob(cube(v)) flip(f;b)) = nerve_box_label(box;flip(f;b)) ∈ cat-ob(C)
24. (ob(cube(v)) flip(flip(f;b);a)) = nerve_box_label(box;flip(flip(f;b);a)) ∈ cat-ob(C)
25. (cat-comp(C) (ob(cube(v)) f) (ob(cube(v)) flip(f;a)) (ob(cube(v)) flip(flip(f;a);b)) 
     (arrow(cube(v)) f flip(f;a) (λx.Ax)) 
     (arrow(cube(v)) flip(f;a) flip(flip(f;a);b) (λx.Ax)))
= (cat-comp(C) (ob(cube(v)) f) (ob(cube(v)) flip(f;b)) (ob(cube(v)) flip(flip(f;b);a)) 
   (arrow(cube(v)) f flip(f;b) (λx.Ax)) 
   (arrow(cube(v)) flip(f;b) flip(flip(f;b);a) (λx.Ax)))
∈ (cat-arrow(C) (ob(cube(v)) f) (ob(cube(v)) flip(flip(f;a);b)))
⊢ (arrow(cube(v)) flip(f;b) flip(flip(f;b);a) (λx.Ax))
= nerve_box_edge(box;flip(f;b);a)
∈ (cat-arrow(C) (ob(cube(v)) flip(f;b)) (ob(cube(v)) flip(flip(f;b);a)))

---

Latex:

---

Latex:
.....subterm.....  T:t
3:n
1.  C  :  SmallCategory
2.  I  :  Cname  List
3.  J  :  nameset(I)  List
4.  x  :  nameset(I)
5.  i  :  \mBbbN{}2
6.  box  :  open\_box(cubical-nerve(C);I;J;x;i)
7.  f  :  name-morph(I;[])
8.  a  :  nameset(I)
9.  b  :  nameset(I)
10.  ((\mexists{}j1\mmember{}J.  \mneg{}(j1  =  a))  \mwedge{}  (\mexists{}j2\mmember{}J.  \mneg{}(j2  =  b)))
\mvee{}  ((\mneg{}\muparrow{}null(J))  \mwedge{}  ((f  x)  =  i)  \mwedge{}  ((flip(f;a)  x)  =  i)  \mwedge{}  ((flip(f;b)  x)  =  i))
11.  v  :  I-face(cubical-nerve(C);I)
12.  (f  a)  =  0
13.  direction(v)  =  (f  dimension(v))
14.  (f  b)  =  0
15.  \mneg{}(a  =  b)
16.  \mneg{}(dimension(v)  =  a)
17.  \mneg{}(dimension(v)  =  b)
18.  (v  \mmember{}  box)
19.  \mneg{}\muparrow{}null(J)
20.  ((ob(cube(v))  flip(flip(f;a);b))  =  nerve\_box\_label(box;flip(flip(f;a);b)))
\mwedge{}  ((ob(cube(v))  f)  =  nerve\_box\_label(box;f))
\mwedge{}  ((ob(cube(v))  flip(f;a))  =  nerve\_box\_label(box;flip(f;a)))
\mwedge{}  ((ob(cube(v))  flip(f;b))  =  nerve\_box\_label(box;flip(f;b)))
\mwedge{}  ((ob(cube(v))  flip(flip(f;b);a))  =  nerve\_box\_label(box;flip(flip(f;b);a)))
21.  (cat-comp(C)  (ob(cube(v))  f)  (ob(cube(v))  flip(f;a))  (ob(cube(v))  flip(flip(f;a);b)) 
          (arrow(cube(v))  f  flip(f;a)  (\mlambda{}x.Ax)) 
          (arrow(cube(v))  flip(f;a)  flip(flip(f;a);b)  (\mlambda{}x.Ax)))
=  (cat-comp(C)  (ob(cube(v))  f)  (ob(cube(v))  flip(f;b))  (ob(cube(v))  flip(flip(f;b);a)) 
      (arrow(cube(v))  f  flip(f;b)  (\mlambda{}x.Ax)) 
      (arrow(cube(v))  flip(f;b)  flip(flip(f;b);a)  (\mlambda{}x.Ax)))
\mvdash{}  (cat-comp(C)  (ob(cube(v))  f)  (ob(cube(v))  flip(f;b))  (ob(cube(v))  flip(flip(f;b);a)) 
      (arrow(cube(v))  f  flip(f;b)  (\mlambda{}x.Ax)) 
      (arrow(cube(v))  flip(f;b)  flip(flip(f;b);a)  (\mlambda{}x.Ax)))
=  (cat-comp(C)  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:
(SubsumeC  \mkleeneopen{}cat-arrow(C)  (ob(cube(v))  f)  (ob(cube(v))  flip(flip(f;b);a))\mkleeneclose{}\mcdot{}
  THEN  Try  ((BLemma  `subtype\_rel-equal`  THEN  Auto))
  THEN  SplitAndHyps
  THEN  Repeat  (EqCD)
  THEN  Try  (Trivial))

---

Home Index