NaturalTransformation F G := Build_NaturalTransformation' F G (fun c => CO c) generalized_identity_commutes generalized_identity_commutes_sym.
Require Import Category.Core Functor.Core NaturalTransformation.Core.