fact: Definition commutes_T_Fp 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.Core.associativity_sym _ _ _ _ _ _ _ _) @ ap10 (ap _ (commutes _ _ _ _)) _ @ (Category.Core.associativity _ _ _ _ _ _ _ _))%path.
imports: Category.Core Functor.Core