(d : D) : Functor C E. Proof. refine (Build_Functor C E (fun c => F (c, d)) (fun _ _ m => @morphism_of _ _ F (_, _) (_, _) (m, identity d)) _ _); abstract t. Defined.
Require Import Category.Core Functor.Core Category.Prod Functor.Composition.Core. Require Import Types.Prod.