(C1 -> (C2 -> D))%category -> (C1 * C2 -> D)%category. Proof. intro F; hnf in F |- *. refine (Build_Functor (C1 * C2) D (fun c1c2 => F (fst c1c2) (snd c1c2)) (fun s d m => F (fst d) _1 (snd m) o (F _1 (fst m)) (snd s)) _ _); abstract do_exponential4. Defined.
Require Import Category.Core Category.Prod FunctorCategory.Core Functor.Core NaturalTransformation.Core NaturalTransformation.Paths. Require Import Basics.Tactics.