(F : Functor C D) (F' : Functor C D') : Functor C (D * D') := Build_Functor C (D * D') (fun c => (F c, F' c)) (fun s d m => (F _1 m, F' _1 m)) (fun _ _ _ _ _ => path_prod' (composition_of F _ _ _ _ _) (composition_of F' _ _ _ _ _)) (fun _ => path_prod' (identity_of F _) (identity_of F' _)).
Require Import Category.Core Functor.Core Category.Prod Functor.Composition.Core. Require Import Types.Prod.