module Chapter9.Lift.Examples.Append
         {A : Set}
       where

open import Level hiding (zero ; suc)

open import Data.Unit
open import Data.Product
open import Data.Fin hiding (_+_ ; fold ; lift)

open import Chapter2.Logic

open import Chapter5.IDesc.Fixpoint
open import Chapter5.IDesc.Induction
open import Chapter5.IDesc.Examples.Nat
open import Chapter5.IDesc.Examples.Bool

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

open import Chapter8.Reornament.Examples.List

open import Chapter9.Functions.Examples.Plus
open import Chapter9.FunOrnament.Examples.Append
open import Chapter9.Patch.Examples.Append

open import Chapter9.Functions
open import Chapter9.FunOrnament
open import Chapter9.Patch
open import Chapter9.Lift.Induction
open import Chapter9.Lift.Constructor

αL : (m : Nat) 
     μ (reornD (ListO A)) (tt , m) 
     DAlgLift (ListO A)
               {i}{xs}  α m {i}{xs}) 
              (μ⁺ ListO A [ inv tt  `⊤)
αL m xs {tt ,  zero , lift tt } {lift tt , lift tt} (lift tt) = xs , lift tt
αL m xs {tt ,  suc zero , n , lift tt } {(a , lift tt , lift tt) , ys , lift tt} ((ih , lift tt) , lift tt) =
     liftConstructor (ListO A) {i⁺ = inv tt} {T = `⊤} {T⁺ = `⊤} 
                     (a , (lift tt , lift tt)) 
                     (ih , lift tt) (lift tt)
αL m xs {tt ,  suc (suc ()) , _ } _

vappend :  Patch _+_ (typeAppend A)
vappend m xs n ys = liftInd (ListO A) {tt} {inv tt}
                            {T = μ NatD [ tt  `⊤} 
                            {T⁺ = μ⁺ ListO A [ inv tt  `⊤ }
                             {i}{hs}  α m {i}{hs}) 
                             {i}{hs}  αL m xs {i}{hs}) n ys

open import Chapter9.Patch.Apply

append :  typeAppend A ⟧FunctionOrn
append = patch (typeAppend A) _+_ vappend