`{Funext} C D F G (T : NaturalTransformation F G) `{forall x, IsIsomorphism (T x)} : @IsIsomorphism (C -> D) F G T. Proof. exists (inverse _); abstract ( path_natural_transformation; first [ apply left_inverse | apply right_inverse ] ). Defined.
Require Import Category.Core Functor.Core NaturalTransformation.Paths FunctorCategory.Core Category.Morphisms NaturalTransformation.Core. Require Import Basics.Tactics.