module FunOrn.Patch.Coherence where
open import Data.Unit
open import Data.Product
open import Logic.Logic
open import Logic.IProp
open import IDesc.Fixpoint
open import Orn.Ornament
open import Orn.Ornament.Algebra
open import Orn.Reornament
open import Orn.Reornament.Make
open import Orn.Reornament.Algebra
open import Orn.Reornament.Coherence
open import FunOrn.Functions
open import FunOrn.FunOrnament
open import FunOrn.Patch
open import FunOrn.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 (forget o x))
(f⁺ (forget o x)
(make o x))
⊢Coherence (μ⁺ o [ inv i⁺ ]× T⁺) (x , xs) (x⁺ , xs⁺) =
coherentOrn o x⁺ , ⊢Coherence T⁺ xs xs⁺
⊢Coherence `⊤ tt tt = tt