---

Step * of Lemma functor-comp-assoc

∀[A,B,C,D:SmallCategory]. ∀[F:Functor(A;B)]. ∀[G:Functor(B;C)]. ∀[H:Functor(C;D)].
  (functor-comp(F;functor-comp(G;H)) = functor-comp(functor-comp(F;G);H) ∈ Functor(A;D))
BY
{ (Auto THEN (BLemma `equal-functors` THENA Auto) THEN RepUR ``functor-comp`` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[A,B,C,D:SmallCategory].  \mforall{}[F:Functor(A;B)].  \mforall{}[G:Functor(B;C)].  \mforall{}[H:Functor(C;D)].
    (functor-comp(F;functor-comp(G;H))  =  functor-comp(functor-comp(F;G);H))


By

---

Latex:
(Auto  THEN  (BLemma  `equal-functors`  THENA  Auto)  THEN  RepUR  ``functor-comp``  0  THEN  Auto)

---

Home Index