open import Function

open import Data.Product

open import Logic.Logic

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

open import Orn.Ornament

module Orn.Reornament.Algebra 
           {I K : Set }
           {D : func  K K}
           {u : I  K}
           (o : orn D u u) where

open import Orn.Reornament
open import Orn.Ornament.Algebra {u = forgetIdx} ( o )

reornAlgebra :   o ⌉D ⟧func (μ  o ⟧orn  forgetIdx)  μ  o ⟧orn  forgetIdx
reornAlgebra {i} = forgetAlg {i} 

forgetReornament : μ  o ⌉D  μ  o ⟧orn  forgetIdx
forgetReornament {i} xs = fold  o ⌉D  {i}  reornAlgebra {i}) {i} xs