open import Level 

open import Chapter5.IDesc

open import Chapter8.Ornament

module Chapter9.Lift.Fold 
         {ℓ : Level}
         {I I⁺ : Set ℓ}
         {D : func ℓ I I}
         {u : I⁺ → I}
         (o : orn D u u)
       where

open import Data.Product

open import Chapter2.Logic 

open import Chapter5.IDesc.InitialAlgebra

open import Chapter8.Reornament o

open import Chapter9.Functions
open import Chapter9.FunOrnament
open import Chapter9.Patch

AlgLift : ∀{T} → Alg D (λ _ → ⟦ T ⟧Type) → FunctionOrn T → Set ℓ
AlgLift α T⁺ = Alg reornD (λ ix → Patch (fold D α (proj₂ ix)) T⁺)


liftAlg : {i : I}{i⁺ : u ⁻¹ i}
          {T : Type ℓ}{T⁺ : FunctionOrn T}
          (α : Alg D (λ _ → ⟦ T ⟧Type))
          (β : AlgLift α T⁺) →
    Patch (fold D α) (μ⁺ o [ i⁺ ]→ T⁺)
liftAlg {i⁺ = inv i⁺} α β = 
  λ x x⁺⁺ → fold reornD (λ {ix} ih → β {ix} ih) x⁺⁺