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