generalized_identity' : NaturalTransformation F G. Proof. apply (generalized_identity F G (ap (@object_of C D) H)). case H. reflexivity. Defined.
Require Import Category.Core Functor.Core NaturalTransformation.Core.