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