diff --git a/quox-nat.agda b/quox-nat.agda deleted file mode 100644 index 4ae275e..0000000 --- a/quox-nat.agda +++ /dev/null @@ -1,78 +0,0 @@ -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