open import Level

open import Data.Product

open import Relation.Binary.PropositionalEquality

open import Chapter5.IDesc
open import Chapter5.IDesc.Fixpoint

open import Chapter8.Ornament

module Chapter8.Reornament.Coherence
         {ℓ : Level}
         {K I : Set ℓ}
         {D : func ℓ I I}
         {u : K → I}
         (o : orn D u u) 
       where

open import Chapter8.Reornament o
open import Chapter8.Ornament.Algebra o
open import Chapter8.Reornament.Algebra o

postulate
  coherentOrn : ∀{k t} → 
                (t⁺ : μ reornD (k , t)) → 
                t ≡ forgetOrnament (forgetReornament t⁺)