fact: Definition NaturalIsomorphism `{Funext} (C D : PreCategory) F G := @Isomorphic (C -> D) F G.
imports: Category.Core Functor.Core NaturalTransformation.Paths FunctorCategory.Core Category.Morphisms NaturalTransformation.Core Basics.Tactics