---

Step * of Lemma same-face-edge-arrows-commute

∀C:SmallCategory. ∀I:Cname List. ∀f:name-morph(I;[]). ∀a,b:nameset(I). ∀v:I-face(cubical-nerve(C);I).
  (((f a) = 0 ∈ ℕ2)
  ⇒ ((f b) = 0 ∈ ℕ2)
  ⇒ (¬(a = b ∈ nameset(I)))
  ⇒ (¬(dimension(v) = a ∈ Cname))
  ⇒ (¬(dimension(v) = b ∈ Cname))
  ⇒ ((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)))))
BY
{ (Auto
   THEN RepeatFor 2 (D -6)
   THEN RepUR ``face-cube`` 0
   THEN All (RepUR ``face-dimension``)
   THEN (RWO  "cubical-nerve-I-cube" (-6) THENA Auto)
   THEN D -6
   THEN D -7
   THEN RepUR ``functor-ob functor-arrow`` 0
   THEN All Reduce
   THEN RenameVar `j' 6
   THEN RenameVar `H' (-7)) }

1
1. C : SmallCategory
2. I : Cname List
3. f : name-morph(I;[])
4. a : nameset(I)
5. b : nameset(I)
6. j : nameset(I)
7. v2 : ℕ2
8. F : cat-ob(poset-cat(I-[j])) ⟶ cat-ob(C)
9. H : x@0:cat-ob(poset-cat(I-[j]))
⟶ y:cat-ob(poset-cat(I-[j]))
⟶ (cat-arrow(poset-cat(I-[j])) x@0 y)
⟶ (cat-arrow(C) (F x@0) (F y))
10. (∀x@0:cat-ob(poset-cat(I-[j]))
       ((H x@0 x@0 (cat-id(poset-cat(I-[j])) x@0)) = (cat-id(C) (F x@0)) ∈ (cat-arrow(C) (F x@0) (F x@0))))
∧ (∀x@0,y,z:cat-ob(poset-cat(I-[j])). ∀f:cat-arrow(poset-cat(I-[j])) x@0 y. ∀g:cat-arrow(poset-cat(I-[j])) y z.
     ((H x@0 z (cat-comp(poset-cat(I-[j])) x@0 y z f g))
     = (cat-comp(C) (F x@0) (F y) (F z) (H x@0 y f) (H y z g))
     ∈ (cat-arrow(C) (F x@0) (F z))))
11. (f a) = 0 ∈ ℕ2
12. (f b) = 0 ∈ ℕ2
13. ¬(a = b ∈ nameset(I))
14. ¬(j = a ∈ Cname)
15. ¬(j = b ∈ Cname)
⊢ (cat-comp(C) (F f) (F flip(f;a)) (F flip(flip(f;a);b)) (H f flip(f;a) (λx.Ax)) 
   (H flip(f;a) flip(flip(f;a);b) (λx.Ax)))
= (cat-comp(C) (F f) (F flip(f;b)) (F flip(flip(f;b);a)) (H f flip(f;b) (λx.Ax)) 
   (H flip(f;b) flip(flip(f;b);a) (λx.Ax)))
∈ (cat-arrow(C) (F f) (F flip(flip(f;a);b)))

---

Latex:

---

Latex:
\mforall{}C:SmallCategory.  \mforall{}I:Cname  List.  \mforall{}f:name-morph(I;[]).  \mforall{}a,b:nameset(I).
\mforall{}v:I-face(cubical-nerve(C);I).
    (((f  a)  =  0)
    {}\mRightarrow{}  ((f  b)  =  0)
    {}\mRightarrow{}  (\mneg{}(a  =  b))
    {}\mRightarrow{}  (\mneg{}(dimension(v)  =  a))
    {}\mRightarrow{}  (\mneg{}(dimension(v)  =  b))
    {}\mRightarrow{}  ((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)))))


By

---

Latex:
(Auto
  THEN  RepeatFor  2  (D  -6)
  THEN  RepUR  ``face-cube``  0
  THEN  All  (RepUR  ``face-dimension``)
  THEN  (RWO    "cubical-nerve-I-cube"  (-6)  THENA  Auto)
  THEN  D  -6
  THEN  D  -7
  THEN  RepUR  ``functor-ob  functor-arrow``  0
  THEN  All  Reduce
  THEN  RenameVar  `j'  6
  THEN  RenameVar  `H'  (-7))

---

Home Index