(F G : object (C -> D)) (T : F = G) : F <~=~> G. Proof. exists (idtoiso_natural_transformation T). exists (idtoiso_natural_transformation (T^)%path); abstract (path_natural_transformation; case T; simpl; auto with morphism). Defined.
Require Import Category.Core Functor.Core NaturalTransformation.Paths FunctorCategory.Core Category.Morphisms NaturalTransformation.Core. Require Import Basics.Tactics.