fact: Definition whisker_l_commutes s d (m : morphism C s d) : F _1 (T d) o (F o G) _1 m = (F o G') _1 m o F _1 (T s) := ((composition_of F _ _ _ _ _)^) @ (ap (fun m => F _1 m) (commutes T _ _ _)) @ (composition_of F _ _ _ _ _).
imports: Category.Core Functor.Core Functor.Composition.Core NaturalTransformation.Core