open import Level module Chapter5.IDesc.Fixpoint {ℓ k : Level} {I : Set k} where open import Chapter5.IDesc data μ (D : func ℓ I I)(i : I) : Set ℓ where ⟨_⟩ : ⟦ D ⟧func (μ D) i → μ D i