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 40 _*_ infix 40 _*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 ⟩