module Chapter4.Desc.Tagged where

open import Level

open import Data.Nat hiding (suc)
open import Data.Fin hiding (suc ; lift)
open import Data.Vec
open import Data.Product

open import Chapter4.Desc

tagDesc : (ℓ : Level) → Set (suc ℓ)
tagDesc ℓ = Σ[ n ∈ ℕ ] Vec (Desc ℓ) n

toDesc : ∀{ℓ} → tagDesc ℓ → Desc ℓ
toDesc (n , ds) = `Σ (Lift (Fin n)) (λ { (lift k) → lookup k ds })

toTagged : ∀{ℓ} → Desc ℓ → tagDesc ℓ
toTagged d = (  , d ∷ [])