module Chapter9.Patch 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.Reornament

open import Chapter9.Functions
open import Chapter9.FunOrnament



Patch : ∀{ℓ}{T : Type ℓ} → ⟦ T ⟧Type → FunctionOrn T → Set ℓ
Patch {T = μ D [ ._ ]→ T} f (μ⁺ o [ inv i⁺ ]→ T⁺) = 
      (x : μ D _) → 
         μ (reornD o) (i⁺ , x) → Patch (f x) T⁺
Patch {T = μ D [ ._ ]× T} (x , t) (μ⁺ o [ inv i⁺ ]× T⁺) =
      μ (reornD o) (i⁺ , x) × Patch t T⁺
Patch {T = `⊤} (lift tt) `⊤ = Lift ⊤