\begin{code}
{-# OPTIONS --without-K #-}
module Naturals where
open import SetsAndFunctions
open import CurryHoward
open import Equality
open import DiscreteAndSeparated
data ℕ : Set where
zero : ℕ
succ : ℕ → ℕ
{-# BUILTIN NATURAL ℕ #-}
{-# BUILTIN ZERO zero #-}
{-# BUILTIN SUC succ #-}
induction : {A : ℕ → Prp} →
A 0 → (∀(k : ℕ) → A k → A(succ k)) → ∀(n : ℕ) → A n
induction base step 0 = base
induction base step (succ n) = step n (induction base step n)
a-peano-axiom : ∀{n : ℕ} → succ n ≠ 0
a-peano-axiom ()
pred : ℕ → ℕ
pred 0 = 0
pred (succ n) = n
succ-injective : ∀{i j : ℕ} → succ i ≡ succ j → i ≡ j
succ-injective = cong pred
ℕ-discrete : discrete ℕ
ℕ-discrete 0 0 = ∨-intro₀ refl
ℕ-discrete 0 (succ n) = ∨-intro₁ (λ())
ℕ-discrete (succ m) 0 = ∨-intro₁ (λ())
ℕ-discrete (succ m) (succ n) = step(ℕ-discrete m n)
where
step : m ≡ n ∨ (m ≠ n) → succ m ≡ succ n ∨ (succ m ≠ succ n)
step (in₀ r) = in₀(cong succ r)
step (in₁ f) = in₁(λ s → f(succ-injective s))
\end{code}
\begin{code}
open import Two
number : ₂ → ℕ
number ₀ = 0
number ₁ = 1
\end{code}