proposition: Corollary fmap_eval {x y : C} : fmap (@eval C _ _ x y) ≈ uncurry (curry eval ∘ exp_out) ∘ prod_out.
proof: Proof. intros. unfold eval, eval'. rewrite fmap_uncurry; cat. Qed.
imports: Category.Lib Category.Theory.Category Category.Theory.Isomorphism Category.Theory.Functor Category.Structure.Cartesian Category.Structure.Cartesian.Closed Category.Functor.Structure.Cartesian