proposition: Lemma helper2 (c : Functor (C1 + C2) D) : 1 o c o inl C1 C2 + 1 o c o inr C1 C2 = c.
proof: Proof. path_functor. (exists (path_forall _ _ (@helper2_helper c))). abstract exp_laws_t. Defined.
imports: Functor.Core Category.Sum Functor.Sum Functor.Paths Functor.Identity Functor.Composition.Core Types.Prod ExponentialLaws.Tactics ExponentialLaws.Law2.Functors