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.Algebra {ℓ : Level} {I K : Set ℓ} {D : func ℓ K K} {u : I → K} (o : orn D u u) where open import Chapter8.Reornament o open import Chapter8.Ornament.Algebra {u = forgetIdx} reorn reornAlgebra : ⟦ reornD ⟧func (μ ⟦ o ⟧orn ∘ forgetIdx) ⇒ μ ⟦ o ⟧orn ∘ forgetIdx reornAlgebra {i} = ornAlgebra {i} forgetReornament : μ reornD ⇒ μ ⟦ o ⟧orn ∘ forgetIdx forgetReornament {i} xs = fold reornD (λ {i} → reornAlgebra {i}) {i} xs