Step * of Lemma functor-arrow-comp

No Annotations
[C,D:SmallCategory]. ∀[F:Functor(C;D)]. ∀[x,y,z:cat-ob(C)]. ∀[f:cat-arrow(C) y]. ∀[g:cat-arrow(C) z].
  ((F (cat-comp(C) g)) (cat-comp(D) (F x) (F y) (F z) (F f) (F g)) ∈ (cat-arrow(D) (F x) (F z)))
BY
((Intros THEN Unhide) THEN OnVar `F' DFunctor THEN Reduce THEN BackThruSomeHyp) }


Latex:


Latex:
No  Annotations
\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].
    ((F  x  z  (cat-comp(C)  x  y  z  f  g))  =  (cat-comp(D)  (F  x)  (F  y)  (F  z)  (F  x  y  f)  (F  y  z  g)))


By


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




Home Index