object ((C -> D) * (C -> D') -> (C -> D * D')) := Build_Functor ((C -> D) * (C -> D')) (C -> D * D') _ functor_morphism_of functor_composition_of functor_identity_of.
Require Import Category.Core Functor.Core Functor.Prod.Core FunctorCategory.Core Category.Prod NaturalTransformation.Prod NaturalTransformation.Composition.Core. Require Import NaturalTransformation.Paths.