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