Functor ((D -> C1) * (D -> C2)) (D -> C1 * C2) := Functor.
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.