Functor ((C1 -> D) * (C2 -> D)) (C1 + C2 -> D). Proof. refine (Build_Functor ((C1 -> D) * (C2 -> D)) (C1 + C2 -> D) (fun FG => fst FG + snd FG)%functor (fun _ _ m => fst_type m + snd_type m)%natural_transformation _ _); simpl in *; abstract ( repeat (intros [?|?] || intros [? ?]); simpl in *; apply path_natural_transformation; intros [?|?]; reflexivity ). Defined.
Require Import Functor.Core FunctorCategory.Core Functor.Identity NaturalTransformation.Core Category.Sum Category.Prod Functor.Sum Functor.Prod.Core NaturalTransformation.Sum Functor.Pointwise.Core NaturalTransformation.Paths.