---

Step * of Lemma cat-comp-assoc

No Annotations
∀[C:SmallCategory]
  ∀x,y,z,w:cat-ob(C). ∀f:cat-arrow(C) x y. ∀g:cat-arrow(C) y z. ∀h:cat-arrow(C) z w.
    ((cat-comp(C) x z w (cat-comp(C) x y z f g) h) = (cat-comp(C) x y w f (cat-comp(C) y z w g h)) ∈ (cat-arrow(C) x w))
BY
{ TACTIC:(Auto
          THEN D -8
          THEN RepeatFor 3 (D -9)
          THEN All
          (RepUR ``cat-comp cat-arrow cat-ob``)⋅
          THEN All Reduce
          THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[C:SmallCategory]
    \mforall{}x,y,z,w:cat-ob(C).  \mforall{}f:cat-arrow(C)  x  y.  \mforall{}g:cat-arrow(C)  y  z.  \mforall{}h:cat-arrow(C)  z  w.
        ((cat-comp(C)  x  z  w  (cat-comp(C)  x  y  z  f  g)  h)  =  (cat-comp(C)  x  y  w  f  (cat-comp(C)  y  z  w  g  h)))


By

---

Latex:
TACTIC:(Auto
                THEN  D  -8
                THEN  RepeatFor  3  (D  -9)
                THEN  All
                (RepUR  ``cat-comp  cat-arrow  cat-ob``)\mcdot{}
                THEN  All  Reduce
                THEN  Auto)

---

Home Index