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)