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⁺⁺