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