```open import Function

open import Level

open import Data.Product
open import Data.Unit

open import Relation.Binary.PropositionalEquality

open import Logic.Logic
open import Logic.IProp
open Logic.IProp.Applicative {zero}

open import IDesc.IDesc
open import IDesc.Lifting
open import IDesc.Fixpoint
open import IDesc.Induction
open import IDesc.InitialAlgebra

open import Orn.Ornament

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

open import Logic.IProp

open import Orn.Reornament
open import Orn.Ornament.Algebra o
open import Orn.Ornament.CartesianMorphism
open import Orn.Reornament.Algebra o

-- Paper: Remark 4.32
coherentOrn : ∀{k t} →
(t⁺ : μ ⌈ o ⌉D (k , t)) →
⊢ t ≡ forget (forgetReornament t⁺)
coherentOrn {k}{t} = induction (⌈ o ⌉D) P
(λ {i}{xs} → step {i} {xs})

where P : {kx : Σ K (μ D ∘ u)} → μ ⌈ o ⌉D kx → Set
P {(k , x)} t⁺ = ⊢ x ≡ fold ⟦ o ⟧orn  forgetAlg (forgetReornament t⁺)

step' : (D' : IDesc I)
(i :  ⟦ D' ⟧ (μ D))
(o' : Orn u D') →
let reornD' : IDesc (Σ K (μ D ∘ u))
reornD' = ⟦ Reorn o' i ⟧Orn in
(xs : ⟦ reornD' ⟧ (μ ⌈ o ⌉D)) →
□h reornD' (λ {kx} t⁺ → ⊢ proj₂ kx ≡ fold ⟦ o ⟧orn forgetAlg (forgetReornament t⁺)) xs →
⊢ i ≡ forgetOrnNT o o'
(Fold.hyps ⟦ o ⟧orn forgetAlg ⟦ o' ⟧Orn
(forgetOrnNT ⌈ o ⌉ (Reorn o' i)
(Fold.hyps ⌈ o ⌉D (λ {i} → reornAlgebra {i}) reornD' xs)))
step' D i (insert S D⁺) (s , xs) ih = step' D i (D⁺ s) xs ih
step' .(`var (u k)) ⟨ i ⟩ (`var (inv k)) ⟨ xs ⟩ ih = ih
step' .`1 tt `1 xs ih = pf refl
step' .(D₁ `× D₂) (i₁ , i₂) (_`×_ {D₁}{D₂} O₁ O₂) (xs₁ , xs₂) (ih₁ , ih₂) =
cong₂ (λ x y → (x , y)) <\$>
step' D₁ i₁ O₁ xs₁ ih₁ ⊛
step' D₂ i₂ O₂ xs₂ ih₂
step' .(`σ n T) (k , i) (`σ {n} {T} T⁺) xs ih = cong⊢ (λ x → (k , x )) (step' (T k) i (T⁺ k) xs ih)
step' .(`Σ S T) (s , i) (`Σ {S} {T} T⁺) xs ih = cong⊢ (λ x → (s , x )) (step' (T s) i (T⁺ s) xs ih)
step' .(`Π S T) i (`Π {S} {T} T⁺) xs ih = extensionality (λ s → step' (T s) (i s) (T⁺ s) (xs s) (ih s))
step' .(`Σ S T) (s , i) (deleteΣ {S} {T} .s o') (refl , xs) ih = cong⊢ (λ x → (s , x)) (step' (T s) i  o' xs ih)
step' .(`σ n T) (k , i) (deleteσ {n} {T} .k o') (refl , xs) ih = cong⊢ (λ x → (k , x)) (step' (T k) i  o' xs ih)

step : DAlg (⌈ o ⌉D) P
step {(k , ⟨ xs ⟩)} {os} ps = cong⊢ ⟨_⟩ (step' (func.out D (u k)) xs (orn.out o k) os ps)
```