Functor (C1 * C2 -> D) (C1 -> (C2 -> D)). Proof. refine (Build_Functor (C1 * C2 -> D) (C1 -> (C2 -> D)) inverse_object_of inverse_morphism_of _ _); abstract by path_natural_transformation. Defined.
Require Import Category.Core Category.Prod FunctorCategory.Core Functor.Core NaturalTransformation.Core NaturalTransformation.Paths. Require Import Basics.Tactics.