---

Step * of Lemma functor-arrow-comp

∀[C,D:SmallCategory]. ∀[F:Functor(C;D)]. ∀[x,y,z:cat-ob(C)]. ∀[f:cat-arrow(C) x y]. ∀[g:cat-arrow(C) y z].
  ((functor-arrow(F) x z (cat-comp(C) x y z f g))
  = (cat-comp(D) (functor-ob(F) x) (functor-ob(F) y) (functor-ob(F) z) (functor-arrow(F) x y f) 
     (functor-arrow(F) y z g))
  ∈ (cat-arrow(D) (functor-ob(F) x) (functor-ob(F) z)))
BY
{ (Auto THEN OnVar `F' DFunctor THEN Reduce 0 THEN BackThruSomeHyp) }

---

Latex:

---

Latex:
\mforall{}[C,D:SmallCategory].  \mforall{}[F:Functor(C;D)].  \mforall{}[x,y,z:cat-ob(C)].  \mforall{}[f:cat-arrow(C)  x  y].
\mforall{}[g:cat-arrow(C)  y  z].
    ((functor-arrow(F)  x  z  (cat-comp(C)  x  y  z  f  g))
    =  (cat-comp(D)  (functor-ob(F)  x)  (functor-ob(F)  y)  (functor-ob(F)  z)  (functor-arrow(F)  x  y  f) 
          (functor-arrow(F)  y  z  g)))


By

---

Latex:
(Auto  THEN  OnVar  `F'  DFunctor  THEN  Reduce  0  THEN  BackThruSomeHyp)

---

Home Index