module Chapter8.AlgebraicOrnament.Examples.Vec (A : Set) where open import Level hiding (zero ; suc) open import Function open import Data.Unit open import Data.Nat open import Data.Fin hiding (lift) open import Data.Product open import Relation.Binary.PropositionalEquality open import Chapter5.IDesc open import Chapter5.IDesc.Fixpoint open import Chapter5.IDesc.InitialAlgebra open import Chapter5.IDesc.Examples.Nat open import Chapter8.Ornament open import Chapter8.Ornament.Examples.List open import Chapter8.Ornament.Algebra (ListO A) import Chapter8.AlgebraicOrnament open Chapter8.AlgebraicOrnament.Func (⟦ ListO A ⟧orn) ornAlgebra Vec : Nat → Set Vec n = μ algOrnD (tt , n) vnil : Vec ze vnil = ⟨ (zero , lift tt) , refl , lift tt ⟩ vcons : ∀{n} → A → Vec n → Vec (su n) vcons {n} a xs = ⟨ (suc zero , a , n , lift tt) , refl , xs , lift tt ⟩