module Chapter4.Desc.Fixpoint where

open import Chapter4.Desc

data μ {ℓ}(D : Desc ℓ) : Set ℓ where
  ⟨_⟩ : ⟦ D ⟧ (μ D) → μ D