Curry.agda

module Curry where

record _×_ (A B : Set) : Set where
  constructor _,_
  field
    andL : A
    andR : B

curry : {A B C : Set} → (A × B → C) → (A → B → C)
curry f = λ {x y → f (x , y)}

uncurry : {A B C : Set} → (A → B → C) → (A × B → C)
uncurry f = λ {(x , y) → f x y}