(c : Functor C1 D * Functor C2 D) : ((1 o (Basics.Overture.fst c + Basics.Overture.snd c) o inl C1 C2)%functor, (1 o (Basics.Overture.fst c + Basics.Overture.snd c) o inr C1 C2)%functor)%core = c. Proof. apply path_prod; simpl; path_functor. Defined.
Require Import Functor.Core. Require Import Category.Sum Functor.Sum. Require Import Functor.Paths. Require Import Functor.Identity Functor.Composition.Core. Require Import Types.Prod ExponentialLaws.Tactics. Require Import ExponentialLaws.Law2.Functors.