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 ⊤