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