{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Data.Vec.NAry where
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Univalence
open import Cubical.Data.Nat
open import Cubical.Data.Vec.Base
private
variable
ℓ ℓ' : Level
A : Type ℓ
B : Type ℓ'
nAryLevel : Level → Level → ℕ → Level
nAryLevel ℓ₁ ℓ₂ zero = ℓ₂
nAryLevel ℓ₁ ℓ₂ (suc n) = ℓ-max ℓ₁ (nAryLevel ℓ₁ ℓ₂ n)
nAryOp : (n : ℕ) → Type ℓ → Type ℓ' → Type (nAryLevel ℓ ℓ' n)
nAryOp zero A B = B
nAryOp (suc n) A B = A → nAryOp n A B
_$ⁿ_ : ∀ {n} → nAryOp n A B → (Vec A n → B)
f $ⁿ [] = f
f $ⁿ (x ∷ xs) = f x $ⁿ xs
curryⁿ : ∀ {n} → (Vec A n → B) → nAryOp n A B
curryⁿ {n = zero} f = f []
curryⁿ {n = suc n} f x = curryⁿ (λ xs → f (x ∷ xs))
$ⁿ-curryⁿ : ∀ {n} (f : Vec A n → B) → _$ⁿ_ (curryⁿ f) ≡ f
$ⁿ-curryⁿ {n = zero} f = funExt λ { [] → refl }
$ⁿ-curryⁿ {n = suc n} f = funExt λ { (x ∷ xs) i → $ⁿ-curryⁿ {n = n} (λ ys → f (x ∷ ys)) i xs}
curryⁿ-$ⁿ : ∀ {n} (f : nAryOp {ℓ = ℓ} {ℓ' = ℓ'} n A B) → curryⁿ {A = A} {B = B} (_$ⁿ_ f) ≡ f
curryⁿ-$ⁿ {n = zero} f = refl
curryⁿ-$ⁿ {n = suc n} f = funExt λ x → curryⁿ-$ⁿ {n = n} (f x)
nAryOp≃VecFun : ∀ {n} → nAryOp n A B ≃ (Vec A n → B)
nAryOp≃VecFun {n = n} = isoToEquiv f
where
f : Iso (nAryOp n A B) (Vec A n → B)
Iso.fun f = _$ⁿ_
Iso.inv f = curryⁿ
Iso.rightInv f = $ⁿ-curryⁿ
Iso.leftInv f = curryⁿ-$ⁿ {n = n}