```------------------------------------------------------------------------
-- Code for converting Vec₁ n A → B to and from n-ary functions
------------------------------------------------------------------------

-- I want universe polymorphism.

module Data.Vec.N-ary1 where

open import Data.Nat
open import Data.Vec1
open import Relation.Binary.PropositionalEquality1

------------------------------------------------------------------------
-- N-ary functions

N-ary : ℕ → Set1 → Set1 → Set1
N-ary zero    A B = B
N-ary (suc n) A B = A → N-ary n A B

------------------------------------------------------------------------
-- Conversion

curryⁿ : ∀ {n A B} → (Vec₁ A n → B) → N-ary n A B
curryⁿ {zero}  f = f []
curryⁿ {suc n} f = λ x → curryⁿ (λ xs → f (x ∷ xs))

_\$ⁿ_ : ∀ {n A B} → N-ary n A B → (Vec₁ A n → B)
f \$ⁿ []       = f
f \$ⁿ (x ∷ xs) = f x \$ⁿ xs

------------------------------------------------------------------------
-- N-ary function equality

Eq : ∀ {A B} n → (B → B → Set1) → (f g : N-ary n A B) → Set1
Eq zero    _∼_ f g = f ∼ g
Eq (suc n) _∼_ f g = ∀ x → Eq n _∼_ (f x) (g x)

------------------------------------------------------------------------
-- Some lemmas

-- The two functions are inverses.

left-inverse : ∀ {n A B} (f : Vec₁ A n → B) →
∀ xs → curryⁿ f \$ⁿ xs ≡₁ f xs
left-inverse f []       = refl
left-inverse f (x ∷ xs) = left-inverse (λ xs → f (x ∷ xs)) xs

data Lift {A : Set1} (R : A → A → Set) x y : Set1 where
lift : R x y → Lift R x y

right-inverse : ∀ {A B} n (f : N-ary n A B) →
Eq n (Lift _≡₁_) (curryⁿ (_\$ⁿ_ {n} f)) f
right-inverse zero    f = lift refl
right-inverse (suc n) f = λ x → right-inverse n (f x)

-- Conversion preserves equality.

curryⁿ-pres : ∀ {n A B _∼_} (f g : Vec₁ A n → B) →
(∀ xs → f xs ∼ g xs) →
Eq n _∼_ (curryⁿ f) (curryⁿ g)
curryⁿ-pres {zero}  f g hyp = hyp []
curryⁿ-pres {suc n} f g hyp = λ x →
curryⁿ-pres (λ xs → f (x ∷ xs)) (λ xs → g (x ∷ xs))
(λ xs → hyp (x ∷ xs))

curryⁿ-pres⁻¹ : ∀ {n A B _∼_} (f g : Vec₁ A n → B) →
Eq n _∼_ (curryⁿ f) (curryⁿ g) →
∀ xs → f xs ∼ g xs
curryⁿ-pres⁻¹ f g hyp []       = hyp
curryⁿ-pres⁻¹ f g hyp (x ∷ xs) =
curryⁿ-pres⁻¹ (λ xs → f (x ∷ xs)) (λ xs → g (x ∷ xs)) (hyp x) xs

appⁿ-pres : ∀ {n A B _∼_} (f g : N-ary n A B) →
Eq n _∼_ f g →
(xs : Vec₁ A n) → (f \$ⁿ xs) ∼ (g \$ⁿ xs)
appⁿ-pres f g hyp []       = hyp
appⁿ-pres f g hyp (x ∷ xs) = appⁿ-pres (f x) (g x) (hyp x) xs

appⁿ-pres⁻¹ : ∀ {n A B _∼_} (f g : N-ary n A B) →
((xs : Vec₁ A n) → (f \$ⁿ xs) ∼ (g \$ⁿ xs)) →
Eq n _∼_ f g
appⁿ-pres⁻¹ {zero}  f g hyp = hyp []
appⁿ-pres⁻¹ {suc n} f g hyp = λ x →
appⁿ-pres⁻¹ (f x) (g x) (λ xs → hyp (x ∷ xs))
```