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