(F G : object (C -> D)) (T : F = G) : Category.Morphisms.idtoiso _ T = idtoiso T. Proof. case T. expand; f_ap. exact (center _). Qed.
Require Import Category.Core Functor.Core NaturalTransformation.Paths FunctorCategory.Core Category.Morphisms NaturalTransformation.Core. Require Import Basics.Tactics.