C D (F G : Functor C D) (T : NaturalTransformation F G) s d d' (m : morphism C s d) (m' : morphism D d' _) : T d o (F _1 m o m') = G _1 m o (T s o m') := ((Category.
Require Import Category.Core Functor.Core.