---

Step * 1 1 1 2 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)))
11. ∀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)))
12. (f a) = 0 ∈ ℕ2
13. (f b) = 0 ∈ ℕ2
14. ¬(a = b ∈ nameset(I))
15. ¬(j = a ∈ Cname)
16. ¬(j = b ∈ Cname)
17. ∀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))))
18. f ∈ name-morph(I-[j];[])
19. flip(f;a) ∈ name-morph(I-[j];[])
20. flip(f;b) ∈ name-morph(I-[j];[])
21. flip(flip(f;a);b) ∈ name-morph(I-[j];[])
22. flip(flip(f;b);a) ∈ name-morph(I-[j];[])
23. i : nameset(I-[j])
⊢ (flip(f;a) i) ≤ (flip(flip(f;a);b) i)
BY
{ ((Assert (flip(f;a) b) = 0 ∈ ℤ BY
          (RepUR ``name-morph-flip`` 0
           THEN AutoSplit
           THEN OnMaybeHyp 14 (\h. (D h THEN HypSubst' (-1) 0 THEN Complete (Auto)))))
   THEN MoveToConcl (-1)
   THEN GenConcl ⌜flip(f;a) = h ∈ name-morph(I;[])⌝⋅
   THEN Auto
   THEN (RepUR ``name-morph-flip`` 0 THEN AutoSplit THEN HypSubst' (-1) 0 THEN SubstFor ⌜h b⌝  0⋅ THEN Auto)) }

---

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)))
11.  \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)))
12.  (f  a)  =  0
13.  (f  b)  =  0
14.  \mneg{}(a  =  b)
15.  \mneg{}(j  =  a)
16.  \mneg{}(j  =  b)
17.  \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)))))
18.  f  \mmember{}  name-morph(I-[j];[])
19.  flip(f;a)  \mmember{}  name-morph(I-[j];[])
20.  flip(f;b)  \mmember{}  name-morph(I-[j];[])
21.  flip(flip(f;a);b)  \mmember{}  name-morph(I-[j];[])
22.  flip(flip(f;b);a)  \mmember{}  name-morph(I-[j];[])
23.  i  :  nameset(I-[j])
\mvdash{}  (flip(f;a)  i)  \mleq{}  (flip(flip(f;a);b)  i)


By

---

Latex:
((Assert  (flip(f;a)  b)  =  0  BY
                (RepUR  ``name-morph-flip``  0
                  THEN  AutoSplit
                  THEN  OnMaybeHyp  14  (\mbackslash{}h.  (D  h  THEN  HypSubst'  (-1)  0  THEN  Complete  (Auto)))))
  THEN  MoveToConcl  (-1)
  THEN  GenConcl  \mkleeneopen{}flip(f;a)  =  h\mkleeneclose{}\mcdot{}
  THEN  Auto
  THEN  (RepUR  ``name-morph-flip``  0
              THEN  AutoSplit
              THEN  HypSubst'  (-1)  0
              THEN  SubstFor  \mkleeneopen{}h  b\mkleeneclose{}    0\mcdot{}
              THEN  Auto))

---

Home Index