open import Level
open import Function

open import Data.Unit
open import Data.Product

open import Chapter2.Logic

open import Chapter5.IDesc
open import Chapter5.IDesc.Fixpoint
open import Chapter5.IDesc.Lifting


module Chapter5.IDesc.Induction
          {ℓ k : Level}
          {I : Set k}
          (D : func ℓ I I)
          (P : {i : I} → μ D i → Set (k ⊔ ℓ))
       where

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

module Induction (α : DAlg) where

  mutual
    induction : {i : I}(x : μ D i) → P x
    induction ⟨ xs ⟩ = α (hyps (func.out D _) xs)
  
    hyps : (D' : IDesc ℓ I)(xs : ⟦ D' ⟧ (μ D)) → [ D' ]^h P xs
    hyps `1 (lift tt) = (lift tt)
    hyps (`var i) xs = induction xs
    hyps (T `× T') (t , t') = hyps T t , hyps T' t'
    hyps (`σ n T) (k , xs) = hyps (T k) xs
    hyps (`Σ S T) (s , xs) = hyps (T s) xs
    hyps (`Π S T) f = λ s → hyps (T s) (f s)

induction : DAlg → {i : I}(x : μ D i) → P x
induction = Induction.induction