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