Functor (D -> C1 * C2) ((D -> C1) * (D -> C2)) := Build_Functor (D -> C1 * C2) ((D -> C1) * (D -> C2)) (fun H => (fst o H, snd o H)%core) (fun s d m => (fst oL m, snd oL m)%core) (fun _ _ _ _ _ => path_prod' (composition_of_whisker_l _ _ _) (composition_of_whisker_l _ _ _)) (fun _ => path_prod' (whisker_l_right_identity _ _) (whisker_l_right_identity _ _)).
Require Import Category.Core Functor.Core FunctorCategory.Core Category.Prod. Require Import Functor.Prod Functor.Composition.Core NaturalTransformation.Composition.Laws NaturalTransformation.Composition.Core. Require Import Types.Prod.