proposition: Corollary unmerge_uncurry {x y z w : C} (f : x ~> y^z) (g : w ~> y^z) : uncurry f ▽ uncurry g ≈ uncurry (f ▽ g) ∘ from prod_coprod_l.
proof: Proof. rewrite uncurry_merge. rewrite <- comp_assoc. rewrite iso_to_from; 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