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