open import Level

open import Chapter5.IDesc

open import Chapter8.Ornament

module Chapter9.Lift.Induction
         { : 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.Induction

open import Chapter8.Reornament o

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


DAlgLift : {T : Type }  DAlg D  _   T ⟧Type)  FunctionOrn T  Set 
DAlgLift α T⁺ = DAlg reornD ((λ {ix} _  Patch (induction D _ α (proj₂ ix)) T⁺))

liftInd : {i : I}{i⁺ : u ⁻¹ i}
          {T : Type }{T⁺ : FunctionOrn T}
          (α : DAlg D  _   T ⟧Type))
          (β : DAlgLift α T⁺) 
    Patch (induction D  _   T ⟧Type) α)
          (μ⁺ o [ i⁺ ]→ T⁺)
liftInd {i⁺ = inv i⁺} α β = 
  λ x x⁺⁺  induction reornD _  {ix}  β {ix}) x⁺⁺