proposition: Theorem curry_adj : forall a, (fun b => a * b)%type ⊣ (fun b => a -> b).
proof: Proof. intros. unfold adjoint; intros. exists (fun k a b => k (b, a)). exists (fun k p => k (snd p) (fst p)). extensionalize. Qed.
imports: Hask.Ltac Hask.Prelude Hask.Control.Applicative Hask.Control.Monad Hask.Control.Monad.Cont Hask.Control.Monad.State Hask.Data.Functor.Contravariant Hask.Data.Functor.Identity Hask.Data.Functor.Kan Hask.Data.Functor.Yoneda Hask.Control.Lens Coq.Classes.Morphisms Coq.Setoids.Setoid Coq.Init.Datatypes Coq.Relations.Relation_Definitions FunctionalExtensionality