proposition: Lemma uncurry_merge {x y z w : C} (f : x ~> y^z) (g : w ~> y^z) : uncurry (f ▽ g) ≈ uncurry f ▽ uncurry g ∘ to prod_coprod_l.
proof: Proof. simpl. apply curry_inj; cat. rewrite curry_comp; cat. rewrite <- merge_comp. apply merge_inv; split; rewrite <- curry_comp; cat. Qed.
imports: Category.Lib Category.Theory.Category Category.Theory.Isomorphism Category.Structure.Initial Category.Structure.Terminal Category.Structure.Cartesian Category.Structure.Cartesian.Closed Category.Structure.Cocartesian Category.Structure.Distributive