open import Level

open import Chapter4.Desc
open import Chapter4.Desc.Fixpoint
open import Chapter4.Desc.Lifting
open import Chapter4.Desc.Induction

module Chapter7.Case 
         {ℓ k : Level}
         (D : Desc ℓ)
         (P : μ D → Set (ℓ ⊔ k))
       where

case : ((xs : ⟦ D ⟧ (μ D)) → P ⟨ xs ⟩) → (x : μ D) → P x
case cases = induction {k = k} D P (λ {xs} _ → cases xs)