open import Function
open import Level

open import Data.Unit
open import Data.Sum
open import Data.Product

open import Chapter2.Logic

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


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

DAlg : Set (ℓ ⊔ k)
DAlg = {xs : ⟦ D ⟧ (μ D)} → 
           [_]^ {k = k} D P xs → 
           P ⟨ xs ⟩

module Induction (α : DAlg) where

  mutual
    induction : (x : μ D) → P x
    induction ⟨ xs ⟩ = α (hyps D xs)

    hyps : (D' : Desc ℓ)(xs : ⟦ D' ⟧ (μ D)) → [ D' ]^ P xs
    hyps `1 (lift tt) = lift tt
    hyps `var xs = induction xs
    hyps (T `× T') (t , t') = hyps T t , hyps T' t'
    hyps (T `+ T') (inj₁ t) = hyps T t
    hyps (T `+ T') (inj₂ t') = hyps T' t'
    hyps (`Σ S T) (s , xs) = hyps (T s) xs
    hyps (`Π S T) f = λ s → hyps (T s) (f s)

induction : DAlg → (x : μ D) → P x
induction = Induction.induction