Functor (C -> D) (C -> D'). Proof. refine (Build_Functor (C -> D) (C -> D') (fun x => pointwise_whiskerL_object_of x) pointwise_whiskerL_morphism_of _ _); abstract (intros; simpl; path_natural_transformation; auto with functor). Defined.
Require Import Category.Core Functor.Core FunctorCategory.Core NaturalTransformation.Paths Functor.Composition.Core NaturalTransformation.Composition.Core.