Functor (C1 + C2 -> D) ((C1 -> D) * (C2 -> D)) := pointwise (inl C1 C2) 1 * pointwise (inr C1 C2) 1.
Require Import Functor.Core FunctorCategory.Core Functor.Identity NaturalTransformation.Core Category.Sum Category.Prod Functor.Sum Functor.Prod.Core NaturalTransformation.Sum Functor.Pointwise.Core NaturalTransformation.Paths.