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⁺)