fact: Definition generalized_identity : NaturalTransformation F G := Build_NaturalTransformation' F G (fun c => CO c) generalized_identity_commutes generalized_identity_commutes_sym.
imports: Category.Core Functor.Core NaturalTransformation.Core