open import Function

open import Data.Unit
open import Data.Product

open import Relation.Binary.PropositionalEquality

open import Logic.Logic

open import IDesc.IDesc
open import IDesc.Fixpoint
open import IDesc.InitialAlgebra

open import Orn.Ornament

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

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

-- Paper: Remark 4.32
make : ∀{k}
(x : μ  o ⟧orn k)  μ  o ⌉D (k , fold  o ⟧orn forgetAlg x)
make {k}  xs  =  help (orn.out o k ) xs
where help : ∀{D' : IDesc I}  (O : Orn u D')
(xs :   O ⟧Orn  (μ  o ⟧orn))
Reorn O (forgetOrnNT O (Fold.hyps  o ⟧orn forgetAlg  O ⟧Orn xs)) ⟧Orn  (μ  o ⌉D)
help (insert S D⁺) (s , xs) = s , help (D⁺ s) xs
help (`var (inv i))  xs  =  help (orn.out o i) xs
help `1 xs = tt
help (O₁  O₂) (xs₁ , xs₂) = help O₁ xs₁ , help O₂ xs₂
help ( T⁺) (k , xs) = help (T⁺ k) xs
help ( T⁺) (s , xs) = help (T⁺ s) xs
help ( T⁺) xs s = help (T⁺ s) (xs s)
help (deleteΣ s O) xs = refl , help O xs
help (deleteσ k O) xs = refl , help O xs