proposition: Lemma curry_fork {x y z w : C} (f : x × y ~> z) (g : x × y ~> w) : curry (f △ g) ≈ from exp_prod_r ∘ curry f △ curry g.
proof: Proof. simpl. apply uncurry_inj; cat. rewrite uncurry_comp; cat. unfold first. rewrite <- fork_comp. apply fork_inv; split; rewrite <- eval_curry; rewrite curry_uncurry; rewrite comp_assoc; cat. Qed.
imports: Category.Lib Category.Theory.Category Category.Theory.Isomorphism Category.Structure.Terminal Category.Structure.Cartesian Category.Instance.Sets