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 ⟩