s d (m : morphism (C1 * C2 -> D) s d) : morphism (C1 -> (C2 -> D)) (inverse_object_of s) (inverse_object_of d). Proof. refine (Build_NaturalTransformation (inverse_object_of s) (inverse_object_of d) (inverse_morphism_of_components_of m) _). 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.