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)