module Chapter9.Patch.Apply where

open import Level

open import Data.Unit
open import Data.Product

open import Chapter2.Logic

open import Chapter5.IDesc.Fixpoint

open import Chapter8.Ornament
open import Chapter8.Ornament.Algebra 
open import Chapter8.Reornament
open import Chapter8.Reornament.Make
open import Chapter8.Reornament.Algebra

open import Chapter9.Functions
open import Chapter9.FunOrnament
open import Chapter9.Patch


patch : ∀{ℓ}{T : Type ℓ} → (fo : FunctionOrn T)(f : ⟦ T ⟧Type) → 
        Patch f fo → ⟦ fo ⟧FunctionOrn
patch (μ⁺ o [ inv i⁺ ]→ T⁺) f p = 
  λ x → patch T⁺ (f (forgetOrnament o x)) 
                 (p (forgetOrnament o x)
                    (makeAlg o x))
patch (μ⁺ o [ inv i⁺ ]× T⁺) (x , xs) (x⁺⁺ , p) =
  forgetReornament o x⁺⁺ , patch T⁺ xs p
patch `⊤ (lift tt) (lift tt) = lift tt