open import Level open import Function open import Data.Unit open import Data.Product open import Data.Nat hiding (fold) open import Data.Fin hiding (fold) open import Chapter2.Logic open import Chapter5.IDesc open import Chapter5.IDesc.Fixpoint open import Chapter5.IDesc.InitialAlgebra open import Chapter8.Ornament module Chapter8.Ornament.Algebra {ℓ k : Level} {I K : Set k} {D : func ℓ K K} {u : I → K} (o : orn D u u) where open import Chapter8.Ornament.CartesianMorphism o ornAlgebra : Alg ⟦ o ⟧orn (μ D ∘ u) ornAlgebra xs = ⟨ forgetNat xs ⟩ forgetOrnament : {i : I} → μ ⟦ o ⟧orn i → μ D (u i) forgetOrnament = fold ⟦ o ⟧orn ornAlgebra