(c : Functor D C1 * Functor D C2) : ((fst o (Basics.Overture.fst c * Basics.Overture.snd c))%functor, (snd o (Basics.Overture.fst c * Basics.Overture.snd c))%functor)%core = c. Proof. apply path_prod; [ apply compose_fst_prod | apply compose_snd_prod ]. Defined.
Require Import Category.Core Functor.Core. Require Import Functor.Prod. Require Import Functor.Paths. Require Import Functor.Identity Functor.Composition.Core. Require Import ExponentialLaws.Law3.Functors. Require Import Types.Prod ExponentialLaws.Tactics.