fact: Definition inverse C D (F G : Functor C D) (T : NaturalTransformation F G) `{forall x, IsIsomorphism (T x)} : NaturalTransformation G F.
imports: Category.Core Functor.Core NaturalTransformation.Paths FunctorCategory.Core Category.Morphisms NaturalTransformation.Core Basics.Tactics