open import Level
open import Function

open import Data.Product

open import Chapter2.Logic

open import Chapter5.IDesc
open import Chapter5.IDesc.Fixpoint
open import Chapter5.IDesc.InitialAlgebra

open import Chapter8.Ornament

module Chapter8.Reornament.Make
         { : Level}
         {K I : Set }
         {D : func  I I}
         {u : K  I}
         (o : orn D u u) 
       where

open import Chapter8.Reornament o
open import Chapter8.Ornament.Algebra o

postulate 
  makeAlg : ∀{k} 
            (x : μ  o ⟧orn k)  μ reornD (k , fold  o ⟧orn ornAlgebra x)