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