proposition: Theorem curry_id {x y z : C} (f : x ~> y) : curry (@id _ (y × z)) ∘ f ≈ curry (first f).
proof: Proof. intros. rewrite curry_comp_l. apply uncurry_inj; cat. Qed.
imports: Category.Lib Category.Theory.Category Category.Theory.Isomorphism Category.Structure.Terminal Category.Structure.Cartesian Category.Instance.Sets