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