(C1 -> (C2 -> D))%category. Proof. refine (Build_Functor C1 (C2 -> D) inverse_object_of_object_of inverse_object_of_morphism_of _ _); abstract (path_natural_transformation; do_exponential4_inverse). Defined.
Require Import Category.Core Category.Prod FunctorCategory.Core Functor.Core NaturalTransformation.Core NaturalTransformation.Paths. Require Import Basics.Tactics.