s d (m : morphism (C1 * C2 -> D) s d) : forall c, morphism (C2 -> D) ((inverse_object_of s) c) ((inverse_object_of d) c). Proof. intro c. refine (Build_NaturalTransformation ((inverse_object_of s) c) ((inverse_object_of d) c) (fun c' => m (c, c')) _). abstract do_exponential4_inverse. Defined.
Require Import Category.Core Category.Prod FunctorCategory.Core Functor.Core NaturalTransformation.Core NaturalTransformation.Paths. Require Import Basics.Tactics.