`{Funext} `{@IsIsomorphism (C -> D) F G T} x : IsIsomorphism (T x). Proof. exists (T^-1 x). - exact (apD10 (ap components_of left_inverse) x). - exact (apD10 (ap components_of right_inverse) x). Defined.
Require Import Category.Core Functor.Core NaturalTransformation.Paths FunctorCategory.Core Category.Morphisms NaturalTransformation.Core. Require Import Basics.Tactics.