open import Level

open import Chapter5.IDesc

open import Chapter8.Ornament

module Chapter9.Lift.Constructor
         {ℓ : 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.Fixpoint
open import Chapter5.IDesc.Induction

open import Chapter7.Case

open import Chapter8.Reornament o

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

Extra : {i : I}{i⁺ : u ⁻¹ i}
         (x : ⟦ D ⟧func (μ D) i) → Set ℓ
Extra {i⁺ = inv i⁺} x = Extension (orn.out o i⁺) x

Args : {i : I}{i⁺ : u ⁻¹ i}
       (x : ⟦ D ⟧func (μ D) i)
       (e : Extra {i⁺ = i⁺} x) → Set ℓ
Args {i⁺ = inv i⁺} x e = 
  ⟦ ⟦ Structure (orn.out o i⁺) x e ⟧Orn ⟧ (μ reornD)

liftConstructor : {i : I}{i⁺ : u ⁻¹ i}
                  {T : Type ℓ}{T⁺ : FunctionOrn T}
                  {t : ⟦ T ⟧Type} →
                  {x : ⟦ D ⟧func (μ D) i}
                  (e : Extra {i⁺ = i⁺} x) → Args {i⁺ = i⁺} x e → Patch t T⁺ →
                  Patch (⟨ x ⟩ , t) (μ⁺ o [ i⁺ ]× T⁺)
liftConstructor {i⁺ = inv i⁺} e a p = ⟨ e , a ⟩ , p