C1 -> (C2 -> D)%category. Proof. intro c1. refine (Build_Functor C2 D (fun c2 => F (c1, c2)) (fun s2 d2 m2 => F _1 ((identity c1, m2) : morphism (_ * _) (c1, s2) (c1, d2))) _ _); abstract do_exponential4_inverse. Defined.
Require Import Category.Core Category.Prod FunctorCategory.Core Functor.Core NaturalTransformation.Core NaturalTransformation.Paths. Require Import Basics.Tactics.