fact: Definition compose : NaturalTransformation F F'' := Build_NaturalTransformation' F F'' (fun c => CO c) compose_commutes compose_commutes_sym.
imports: Category.Core Functor.Core Functor.Composition.Core NaturalTransformation.Core