open import Axiom.Extensionality.Propositional module _ (ext : βˆ€ {a b} β†’ Extensionality a b) where open import Prelude hiding (zero; suc) open import Data.W renaming (induction to inductionβ€²) open import Data.Container open import Data.Container.Relation.Unary.All ; open β–‘ variable 𝓀 β„“ : Level A B : Set 𝓀 P Q : A β†’ Set β„“ C : Container 𝓀 β„“ data Tag : Set where `zero `suc : Tag Body : Tag β†’ Set Body t = case t of Ξ» {`zero β†’ βŠ₯ ; `suc β†’ ⊀} Repr : Container lzero lzero Repr = Tag β–· Body Nat : Set Nat = W Repr Natβ€² : Set Natβ€² = ⟦ Repr ⟧ Nat zero : Nat zero = sup (`zero , Ξ» ()) suc : Nat β†’ Nat suc n = sup (`suc , const n) induction : (P : W C β†’ Set β„“) β†’ (IH : (t : ⟦ C ⟧ (W C)) β†’ β–‘ C P t β†’ P (sup t)) β†’ (w : W C) β†’ P w induction P IH = inductionβ€² P (Ξ» {t} β†’ IH t) elim : (P : Nat β†’ Set β„“) β†’ (Z : P zero) β†’ (S : βˆ€ n β†’ P n β†’ P (suc n)) β†’ (n : Nat) β†’ P n elim P Z S = induction _ Ξ» (tag , body) β†’ body |> (case tag return (Ξ» t β†’ (nβ€² : Body t β†’ Nat) β†’ β–‘ Repr P (t , nβ€²) β†’ P (sup (t , nβ€²))) of Ξ» where `zero β†’ Ξ» nβ€² _ β†’ ≑.subst (Ξ» nβ€² β†’ P (sup (`zero , nβ€²))) (ext Ξ» ()) Z `suc β†’ Ξ» nβ€² IH β†’ S (nβ€² tt) (IH .proof tt)) pred : Nat β†’ Nat pred = induction _ Ξ» n@(tag , body) _ β†’ body |> (case tag return (Ξ» t β†’ (Body t β†’ Nat) β†’ Nat) of Ξ» where `zero _ β†’ zero `suc n β†’ n tt) Subterms : (A : Set 𝓀) (P : A β†’ Set β„“) β†’ Set _ Subterms A P = Ξ£[ x ∈ A ] (P x β†’ W (A β–· P)) subterms : W (A β–· P) β†’ Subterms A P subterms = induction _ Ξ» t IH β†’ t natSub : Nat β†’ List Nat natSub n = case subterms n of Ξ» where (`zero , body) β†’ [] (`suc , body) β†’ [ body tt ] where open List