From 8f860cc1be37057a87daf53788b34aec1068c5d6 Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Sun, 27 Feb 2022 02:19:22 +0100
Subject: [PATCH] an agda file that is kinda like how datatypes would be
 encoded in quox

---
 quox-nat.agda | 44 ++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 44 insertions(+)
 create mode 100644 quox-nat.agda

diff --git a/quox-nat.agda b/quox-nat.agda
new file mode 100644
index 0000000..a8a9cd7
--- /dev/null
+++ b/quox-nat.agda
@@ -0,0 +1,44 @@
+open import Axiom.Extensionality.Propositional
+
+module _ (ext : ∀ {a b} → Extensionality a b) where
+
+open import Prelude hiding (zero; suc)
+open import Data.W
+open import Data.Container
+open import Data.Container.Relation.Unary.All ; open □
+
+variable ℓ : Level
+
+
+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)
+
+elim : (P : Nat → Set ℓ) →
+       (Z : P zero) →
+       (S : ∀ n → P n → P (suc n)) →
+       (n : Nat) → P n
+elim P Z S = induction P λ {(tag , 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)) body