---

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


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)
16. ∀x,y,z:name-morph(I-[j];[]).
      ((∀i:nameset(I-[j]). ((x i) ≤ (y i)))
      ⇒ (∀i:nameset(I-[j]). ((y i) ≤ (z i)))
      ⇒ ((H x z (λx.Ax))
         = (cat-comp(C) (F x) (F y) (F z) (H x y (λi.Ax)) (H y z (λi.Ax)))
         ∈ (cat-arrow(C) (F x) (F z))))
⊢ (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)))
BY
{ ((Assert f ∈ name-morph(I-[j];[]) BY
          Auto)
   THEN (Assert flip(f;a) ∈ name-morph(I-[j];[]) BY
               (SubsumeC ⌜name-morph(I;[])⌝⋅ THEN Auto))
   THEN (Assert flip(f;b) ∈ name-morph(I-[j];[]) BY
               (SubsumeC ⌜name-morph(I;[])⌝⋅ THEN Auto))
   THEN (Assert flip(flip(f;a);b) ∈ name-morph(I-[j];[]) BY
               (SubsumeC ⌜name-morph(I;[])⌝⋅ THEN Auto))
   THEN (Assert flip(flip(f;b);a) ∈ name-morph(I-[j];[]) BY
               (SubsumeC ⌜name-morph(I;[])⌝⋅ THEN Auto))) }

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)
16. ∀x,y,z:name-morph(I-[j];[]).
      ((∀i:nameset(I-[j]). ((x i) ≤ (y i)))
      ⇒ (∀i:nameset(I-[j]). ((y i) ≤ (z i)))
      ⇒ ((H x z (λx.Ax))
         = (cat-comp(C) (F x) (F y) (F z) (H x y (λi.Ax)) (H y z (λi.Ax)))
         ∈ (cat-arrow(C) (F x) (F z))))
17. f ∈ name-morph(I-[j];[])
18. flip(f;a) ∈ name-morph(I-[j];[])
19. flip(f;b) ∈ name-morph(I-[j];[])
20. flip(flip(f;a);b) ∈ name-morph(I-[j];[])
21. flip(flip(f;b);a) ∈ name-morph(I-[j];[])
⊢ (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:

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  :  \mBbbN{}2
8.  F  :  cat-ob(poset-cat(I-[j]))  {}\mrightarrow{}  cat-ob(C)
9.  H  :  x@0:cat-ob(poset-cat(I-[j]))
{}\mrightarrow{}  y:cat-ob(poset-cat(I-[j]))
{}\mrightarrow{}  (cat-arrow(poset-cat(I-[j]))  x@0  y)
{}\mrightarrow{}  (cat-arrow(C)  (F  x@0)  (F  y))
10.  (\mforall{}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))))
\mwedge{}  (\mforall{}x@0,y,z:cat-ob(poset-cat(I-[j])).  \mforall{}f:cat-arrow(poset-cat(I-[j]))  x@0  y.
      \mforall{}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))))
11.  (f  a)  =  0
12.  (f  b)  =  0
13.  \mneg{}(a  =  b)
14.  \mneg{}(j  =  a)
15.  \mneg{}(j  =  b)
16.  \mforall{}x,y,z:name-morph(I-[j];[]).
            ((\mforall{}i:nameset(I-[j]).  ((x  i)  \mleq{}  (y  i)))
            {}\mRightarrow{}  (\mforall{}i:nameset(I-[j]).  ((y  i)  \mleq{}  (z  i)))
            {}\mRightarrow{}  ((H  x  z  (\mlambda{}x.Ax))  =  (cat-comp(C)  (F  x)  (F  y)  (F  z)  (H  x  y  (\mlambda{}i.Ax))  (H  y  z  (\mlambda{}i.Ax)))))
\mvdash{}  (cat-comp(C)  (F  f)  (F  flip(f;a))  (F  flip(flip(f;a);b))  (H  f  flip(f;a)  (\mlambda{}x.Ax)) 
      (H  flip(f;a)  flip(flip(f;a);b)  (\mlambda{}x.Ax)))
=  (cat-comp(C)  (F  f)  (F  flip(f;b))  (F  flip(flip(f;b);a))  (H  f  flip(f;b)  (\mlambda{}x.Ax)) 
      (H  flip(f;b)  flip(flip(f;b);a)  (\mlambda{}x.Ax)))


By

---

Latex:
((Assert  f  \mmember{}  name-morph(I-[j];[])  BY
                Auto)
  THEN  (Assert  flip(f;a)  \mmember{}  name-morph(I-[j];[])  BY
                          (SubsumeC  \mkleeneopen{}name-morph(I;[])\mkleeneclose{}\mcdot{}  THEN  Auto))
  THEN  (Assert  flip(f;b)  \mmember{}  name-morph(I-[j];[])  BY
                          (SubsumeC  \mkleeneopen{}name-morph(I;[])\mkleeneclose{}\mcdot{}  THEN  Auto))
  THEN  (Assert  flip(flip(f;a);b)  \mmember{}  name-morph(I-[j];[])  BY
                          (SubsumeC  \mkleeneopen{}name-morph(I;[])\mkleeneclose{}\mcdot{}  THEN  Auto))
  THEN  (Assert  flip(flip(f;b);a)  \mmember{}  name-morph(I-[j];[])  BY
                          (SubsumeC  \mkleeneopen{}name-morph(I;[])\mkleeneclose{}\mcdot{}  THEN  Auto)))

---

Home Index