proposition: Corollary eval_curry {x y z w : C} (f : y × z ~> w) (g : x ~> y) (h : x ~> z) : eval ∘ ((curry f ∘ g) △ h) ≈ f ∘ g △ h.
proof: Proof. intros. rewrite <- (ump_exponents f) at 2. rewrite <- comp_assoc. unfold first. rewrite <- fork_comp; cat. rewrite <- comp_assoc; cat. Qed.
imports: Category.Lib Category.Theory.Category Category.Theory.Isomorphism Category.Structure.Terminal Category.Structure.Cartesian Category.Instance.Sets