open import Function
open import Data.Unit hiding (_≟_)
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
{K I : Set }
{D : func I I}
{u : K → I}
where
forgetIdx : Σ K (μ D ∘ u) → K
forgetIdx = proj₁
Reorn : ∀{D'} → (O : Orn u D') → ⟦ D' ⟧ (μ D) → Orn forgetIdx ⟦ O ⟧Orn
Reorn `1 tt = `1
Reorn (O₁ `× O₂) (xs₁ , xs₂) = Reorn O₁ xs₁ `× Reorn O₂ xs₂
Reorn (`σ T⁺) (k , xs) = deleteσ k (Reorn (T⁺ k) xs)
Reorn (`Σ T⁺) (s , xs) = deleteΣ s (Reorn (T⁺ s) xs)
Reorn (`Π T⁺) f = `Π λ s → Reorn (T⁺ s) (f s)
Reorn (`var (inv k)) xs = `var (inv (k , xs))
Reorn (insert S D⁺) xs = `Σ λ s → Reorn (D⁺ s) xs
Reorn (deleteΣ {T = T} s o) (s' , xs) = insert (s' ≡ s) λ q → Reorn o (subst (λ s → ⟦ T s ⟧ (μ D)) q xs)
Reorn (deleteσ {T = T} k o) (k' , xs) = insert (k' ≡ k) λ { q → Reorn o (subst (λ k → ⟦ T k ⟧ (μ D)) q xs) }
⌈_⌉ : (o : orn D u u) → orn ⟦ o ⟧orn forgetIdx forgetIdx
⌈ o ⌉ = orn.mk (λ { (k , ⟨ xs ⟩) → Reorn (orn.out o k) xs })
⌈_⌉D : orn D u u → func (Σ K (μ D ∘ u)) (Σ K (μ D ∘ u))
⌈ o ⌉D = ⟦ ⌈ o ⌉ ⟧orn