module Chapter6.Desc.FreeMonad where

open import Level hiding (zero ; suc)

open import Data.Unit
open import Data.Nat hiding (_*_)
open import Data.Fin hiding (lift)
open import Data.Vec
open import Data.Product

open import Chapter4.Desc
open import Chapter4.Desc.Tagged
open import Chapter4.Desc.Fixpoint

infix  _*_
infix  _*D_


_*D_ : ∀{ℓ} → tagDesc ℓ → Set ℓ → tagDesc ℓ
(cs , ds) *D X = suc cs , 
                (`Σ X λ _ → `1) ∷
                ds 

_*_ : ∀{ℓ} → tagDesc ℓ → Set ℓ → Set ℓ
D * X = μ (toDesc (D *D X))

`v : ∀{ℓ D}{X : Set ℓ} → X → D * X
`v x = ⟨ lift zero , x , lift tt  ⟩

`comp : ∀{ℓ D}{X : Set ℓ} → ⟦ toDesc D ⟧ (D * X) → D * X
`comp (lift k , xs) = ⟨ lift (suc k) , xs ⟩