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

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


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