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