    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Code for converting Vec A n → B to and from n-ary functions
    ------------------------------------------------------------------------

    {-# OPTIONS --cubical-compatible --safe #-}

    module Data.Vec.N-ary where

    open import Axiom.Extensionality.Propositional using (Extensionality)
    open import Function.Bundles using (_↔_; Inverse; mk↔ₛ′)
    open import Data.Nat.Base hiding (_⊔_)
    open import Data.Product.Base as Product using (∃; _,_)
    open import Data.Vec.Base using (Vec; []; _∷_; head; tail)
    open import Function.Base using (_∘_; id; flip; constᵣ)
    open import Function.Bundles using (_⇔_; mk⇔)
    open import Level using (Level; _⊔_)
    open import Relation.Binary.Core using (REL)
    open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong)

    private
      variable
        a b c ℓ ℓ₁ ℓ₂ : Level
        A : Set a
        B : Set b
        C : Set c

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

    N-ary-level : Level → Level → ℕ → Level
    N-ary-level ℓ₁ ℓ₂ zero    = ℓ₂
    N-ary-level ℓ₁ ℓ₂ (suc n) = ℓ₁ ⊔ N-ary-level ℓ₁ ℓ₂ n

    N-ary : ∀ (n : ℕ) → Set ℓ₁ → Set ℓ₂ → Set (N-ary-level ℓ₁ ℓ₂ n)
    N-ary zero    A B = B
    N-ary (suc n) A B = A → N-ary n A B

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

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

    infix -1 _$ⁿ_

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

    ------------------------------------------------------------------------
    -- Quantifiers

    module _ {A : Set a} where

      -- Universal quantifier.

      ∀ⁿ : ∀ n → N-ary n A (Set ℓ) → Set (N-ary-level a ℓ n)
      ∀ⁿ zero    P = P
      ∀ⁿ (suc n) P = ∀ x → ∀ⁿ n (P x)

      -- Universal quantifier with implicit (hidden) arguments.

      ∀ⁿʰ : ∀ n → N-ary n A (Set ℓ) → Set (N-ary-level a ℓ n)
      ∀ⁿʰ zero    P = P
      ∀ⁿʰ (suc n) P = ∀ {x} → ∀ⁿʰ n (P x)

      -- Existential quantifier.

      ∃ⁿ : ∀ n → N-ary n A (Set ℓ) → Set (N-ary-level a ℓ n)
      ∃ⁿ zero    P = P
      ∃ⁿ (suc n) P = ∃ λ x → ∃ⁿ n (P x)

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

    Eq : ∀ {A : Set a} {B : Set b} {C : Set c} n →
         REL B C ℓ → REL (N-ary n A B) (N-ary n A C) (N-ary-level a ℓ n)
    Eq n _∼_ f g = ∀ⁿ n (curryⁿ {n = n} λ xs → (f $ⁿ xs) ∼ (g $ⁿ xs))

    -- A variant where all the arguments are implicit (hidden).

    Eqʰ : ∀ {A : Set a} {B : Set b} {C : Set c} n →
          REL B C ℓ → REL (N-ary n A B) (N-ary n A C) (N-ary-level a ℓ n)
    Eqʰ n _∼_ f g = ∀ⁿʰ n (curryⁿ {n = n} λ xs → (f $ⁿ xs) ∼ (g $ⁿ xs))

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

    -- The functions curryⁿ and _$ⁿ_ are inverses.

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

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

    -- ∀ⁿ can be expressed in an "uncurried" way.

    uncurry-∀ⁿ : ∀ n {P : N-ary n A (Set ℓ)} →
                 ∀ⁿ n P ⇔ (∀ (xs : Vec A n) → P $ⁿ xs)
    uncurry-∀ⁿ {a} {A} {ℓ} n = mk⇔ (⇒ n) (⇐ n)
      where
      ⇒ : ∀ n {P : N-ary n A (Set ℓ)} →
          ∀ⁿ n P → (∀ (xs : Vec A n) → P $ⁿ xs)
      ⇒ zero    p []       = p
      ⇒ (suc n) p (x ∷ xs) = ⇒ n (p x) xs

      ⇐ : ∀ n {P : N-ary n A (Set ℓ)} →
          (∀ (xs : Vec A n) → P $ⁿ xs) → ∀ⁿ n P
      ⇐ zero    p = p []
      ⇐ (suc n) p = λ x → ⇐ n (p ∘ _∷_ x)

    -- ∃ⁿ can be expressed in an "uncurried" way.

    uncurry-∃ⁿ : ∀ n {P : N-ary n A (Set ℓ)} →
                 ∃ⁿ n P ⇔ (∃ λ (xs : Vec A n) → P $ⁿ xs)
    uncurry-∃ⁿ {a} {A} {ℓ} n = mk⇔ (⇒ n) (⇐ n)
      where
      ⇒ : ∀ n {P : N-ary n A (Set ℓ)} →
          ∃ⁿ n P → (∃ λ (xs : Vec A n) → P $ⁿ xs)
      ⇒ zero    p       = ([] , p)
      ⇒ (suc n) (x , p) = Product.map (_∷_ x) id (⇒ n p)

      ⇐ : ∀ n {P : N-ary n A (Set ℓ)} →
          (∃ λ (xs : Vec A n) → P $ⁿ xs) → ∃ⁿ n P
      ⇐ zero    ([] , p)     = p
      ⇐ (suc n) (x ∷ xs , p) = (x , ⇐ n (xs , p))

    -- Conversion preserves equality.

    module _ (_∼_ : REL B C ℓ) where

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

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

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

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

    -- Eq and Eqʰ are equivalent.

    Eq-to-Eqʰ : ∀ n (_∼_ : REL B C ℓ) {f : N-ary n A B} {g : N-ary n A C} →
                Eq n _∼_ f g → Eqʰ n _∼_ f g
    Eq-to-Eqʰ zero    _∼_ eq = eq
    Eq-to-Eqʰ (suc n) _∼_ eq = Eq-to-Eqʰ n _∼_ (eq _)

    Eqʰ-to-Eq : ∀ n (_∼_ : REL B C ℓ) {f : N-ary n A B} {g : N-ary n A C} →
                Eqʰ n _∼_ f g → Eq n _∼_ f g
    Eqʰ-to-Eq zero    _∼_ eq = eq
    Eqʰ-to-Eq (suc n) _∼_ eq = λ _ → Eqʰ-to-Eq n _∼_ eq

    module _ (ext : ∀ {a b} → Extensionality a b) where

      Vec↔N-ary : ∀ n → (Vec A n → B) ↔ N-ary n A B
      Vec↔N-ary zero = mk↔ₛ′ (λ vxs → vxs []) (flip constᵣ) (λ _ → refl)
        (λ vxs → ext λ where [] → refl)
      Vec↔N-ary (suc n) = let open Inverse (Vec↔N-ary n) in
        mk↔ₛ′ (λ vxs x → to λ xs → vxs (x ∷ xs))
        (λ any xs → from (any (head xs)) (tail xs))
        (λ any → ext λ x → strictlyInverseˡ _)
        (λ vxs → ext λ where (x ∷ xs) → cong (λ f → f xs) (strictlyInverseʳ (λ ys → vxs (x ∷ ys))))