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