(c : Functor (C1 + C2) D) : 1 o c o inl C1 C2 + 1 o c o inr C1 C2 = c. Proof. path_functor. (exists (path_forall _ _ (@helper2_helper c))). abstract exp_laws_t. 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.