fact: Definition whisker_r_commutes s d (m : morphism C s d) : T (G d) o (F o G) _1 m = (F' o G) _1 m o T (G s) := commutes T _ _ _.
imports: Category.Core Functor.Core Functor.Composition.Core NaturalTransformation.Core