fact: Definition eval {x y} : (x ⇒ y) ⨂ x ~> y := uncurry id.
imports: Category.Lib Category.Theory.Category Category.Theory.Isomorphism Category.Theory.Functor Category.Structure.Monoidal.Cartesian Category.Instance.Sets