fact: Definition whisker_l := Build_NaturalTransformation' (F o G) (F o G') (fun c => CO c) whisker_l_commutes whisker_l_commutes_sym.
imports: Category.Core Functor.Core Functor.Composition.Core NaturalTransformation.Core