C D (F G : Functor C D) (T : NaturalTransformation F G) `{forall x, IsIsomorphism (T x)} : NaturalTransformation G F. Proof. exists (fun x => (T x)^-1); abstract ( intros; iso_move_inverse; first [ apply commutes | symmetry; apply commutes ] ). Defined.
Require Import Category.Core Functor.Core NaturalTransformation.Paths FunctorCategory.Core Category.Morphisms NaturalTransformation.Core. Require Import Basics.Tactics.