{-# OPTIONS --universe-polymorphism #-}
module Data.Product.N-ary where
open import Data.Nat
open import Data.Product
open import Data.Unit
open import Data.Vec
open import Function.Inverse
open import Level
open import Relation.Binary.PropositionalEquality as P using (_≡_)
infix 8 _^_
_^_ : ∀ {ℓ} → Set ℓ → ℕ → Set ℓ
A ^ 0 = Lift ⊤
A ^ 1 = A
A ^ suc (suc n) = A × A ^ suc n
⇿Vec : ∀ {a} {A : Set a} n → A ^ n ⇿ Vec A n
⇿Vec n = record
{ to = P.→-to-⟶ (toVec n)
; from = P.→-to-⟶ fromVec
; inverse-of = record
{ left-inverse-of = fromVec∘toVec n
; right-inverse-of = toVec∘fromVec
}
}
where
toVec : ∀ {a} {A : Set a} n → A ^ n → Vec A n
toVec 0 (lift tt) = []
toVec 1 x = [ x ]
toVec (suc (suc n)) (x , xs) = x ∷ toVec _ xs
fromVec : ∀ {a} {A : Set a} {n} → Vec A n → A ^ n
fromVec [] = lift tt
fromVec (x ∷ []) = x
fromVec (x ∷ y ∷ xs) = (x , fromVec (y ∷ xs))
fromVec∘toVec : ∀ {a} {A : Set a} n (xs : A ^ n) →
fromVec (toVec n xs) ≡ xs
fromVec∘toVec 0 (lift tt) = P.refl
fromVec∘toVec 1 x = P.refl
fromVec∘toVec 2 (x , y) = P.refl
fromVec∘toVec (suc (suc (suc n))) (x , y , xs) =
P.cong (_,_ x) (fromVec∘toVec (suc (suc n)) (y , xs))
toVec∘fromVec : ∀ {a} {A : Set a} {n} (xs : Vec A n) →
toVec n (fromVec xs) ≡ xs
toVec∘fromVec [] = P.refl
toVec∘fromVec (x ∷ []) = P.refl
toVec∘fromVec (x ∷ y ∷ xs) = P.cong (_∷_ x) (toVec∘fromVec (y ∷ xs))