---

Step * of Lemma cat-comp-assoc

∀[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
{ (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:
\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:
(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