Currying using a Universe

Currying.agda

module Currying where

open import Level
open import Data.Product as P using (_×_ ; _,_)
open import Function

data Universe (ℓ : Level) : Set (suc ℓ) where
  set  : (A : Set ℓ) → Universe ℓ
  _**_ : (u₁ u₂ : Universe ℓ) → Universe ℓ

⟦_⟧ : {ℓ : Level} (u : Universe ℓ) → Set ℓ
⟦ set A    ⟧ = A
⟦ u₁ ** u₂ ⟧ = ⟦ u₁ ⟧ × ⟦ u₂ ⟧

⟦_⟧→_ : {ℓ : Level} (u : Universe ℓ) (R : Set ℓ) → Set ℓ
⟦ set A    ⟧→ R = A → R
⟦ u₁ ** u₂ ⟧→ R = ⟦ u₁ ⟧→ (⟦ u₂ ⟧→ R)

curry : {ℓ : Level} (u : Universe ℓ) {R : Set ℓ} (f : ⟦ u ⟧ → R) → ⟦ u ⟧→ R
curry (set A)     f = f
curry (u₁ ** u₂)  f = curry u₁ $ λ v₁ →
                      curry u₂ $ λ v₂ →
                      f (v₁ , v₂)

uncurry :  {ℓ : Level} (u : Universe ℓ) {R : Set ℓ} (f : ⟦ u ⟧→ R) → ⟦ u ⟧ → R
uncurry (set A)    f = f
uncurry (u₁ ** u₂) f = P.uncurry $ λ v₁ v₂ → uncurry u₂ (uncurry u₁ f v₁) v₂