proposition: Corollary curry_unfork {x y z w : C} (f : x × y ~> z) (g : x × y ~> w) : curry f △ curry g ≈ to exp_prod_r ∘ curry (f △ g).
proof: Proof. rewrite curry_fork. rewrite comp_assoc. rewrite iso_to_from; cat. Qed.
imports: Category.Lib Category.Theory.Category Category.Theory.Isomorphism Category.Structure.Terminal Category.Structure.Cartesian Category.Instance.Sets