(F G : object (C -> D)) (T : F = G) : NaturalTransformation F G. Proof. refine (Build_NaturalTransformation' F G (fun x => idtoiso _ (ap10 (ap object_of T) x)) _ _); intros; case T; simpl; [ exact (left_identity _ _ _ _ @ (right_identity _ _ _ _)^) | exact (right_identity _ _ _ _ @ (left_identity _ _ _ _)^) ]. Defined.
Require Import Category.Core Functor.Core NaturalTransformation.Paths FunctorCategory.Core Category.Morphisms NaturalTransformation.Core. Require Import Basics.Tactics.