module Chapter9.FunOrnament.Examples.Append where

open import Data.Unit

open import Chapter2.Logic

open import Chapter5.IDesc.Examples.Nat

open import Chapter8.Ornament
open import Chapter8.Ornament.Examples.List

open import Chapter9.Functions.Examples.Plus

open import Chapter9.FunOrnament

typeAppend : (A : Set) → FunctionOrn type+
typeAppend A = μ⁺ ListO A [ inv tt ]→ 
               μ⁺ ListO A [ inv tt ]→ 
               μ⁺ ListO A [ inv tt ]× `⊤