proposition: Corollary curry_comp_l {x y z w : C} (f : y × z ~> w) (g : x ~> y) : curry f ∘ g ≈ curry (f ∘ first g).
proof: Proof. apply uncurry_inj; cat. rewrite <- (ump_exponents (uncurry (curry f ∘ g))). rewrite curry_uncurry. unfold first in *. rewrite <- comp_assoc. rewrite eval_curry. reflexivity. Qed.
imports: Category.Lib Category.Theory.Category Category.Theory.Isomorphism Category.Structure.Terminal Category.Structure.Cartesian Category.Instance.Sets