fact: Definition compose_commutes_sym s d (m : morphism C s d) : F'' _1 m o CO s = CO d o F _1 m := (associativity_sym _ _ _ _ _ _ _ _) @ ap (fun x => x o _) (commutes_sym T' _ _ m) @ (associativity _ _ _ _ _ _ _ _) @ ap (fun x => _ o x) (commutes_sym T _ _ m) @ (associativity_sym _ _ _ _ _ _ _ _).
imports: Category.Core Functor.Core Functor.Composition.Core NaturalTransformation.Core