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