Functor (C * D) D := Build_Functor (C * D) D (@ _ _) (fun _ _ => @ _ _) (fun _ _ _ _ _ => idpath) (fun _ => idpath).
Require Import Category.Core Functor.Core Category.Prod Functor.Composition.Core. Require Import Types.Prod.