open import Level

open import Chapter5.IDesc

open import Chapter8.Ornament

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

Cases : ∀{I : Set ℓ}(D : func ℓ I I) → (∀{i} → μ D i → Set ℓ) → Set ℓ
Cases {I} D P = {i : I}(xs : ⟦ D ⟧func (μ D) i) → P ⟨ xs ⟩ 

CasesLift : ∀{T} → Cases D (λ _ → ⟦ T ⟧Type) → FunctionOrn T → Set ℓ
CasesLift α T⁺ = Cases reornD 
                       (λ {ix} xs → Patch (induction D _ (λ {i}{xs} ih → α {i} xs) 
                                          (proj₂ ix)) T⁺)

liftCase : {i : I}{i⁺ : u ⁻¹ i}
           {T : Type ℓ}{T⁺ : FunctionOrn T}
           (α : Cases D (λ _ → ⟦ T ⟧Type))
           (β : CasesLift α T⁺)  →
    Patch (induction D (λ _ → ⟦ T ⟧Type) (λ {i}{xs} _ → α xs)) (μ⁺ o [ i⁺ ]→ T⁺)
liftCase {i⁺ = inv i⁺} α β = 
  λ x x⁺⁺ → induction reornD _ (λ {ix}{xs} _ → β {ix} xs) x⁺⁺