module Chapter4.Desc.Fixpoint where open import Chapter4.Desc data μ {ℓ}(D : Desc ℓ) : Set ℓ where ⟨_⟩ : ⟦ D ⟧ (μ D) → μ D