Martin Escardo 2011.

\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}

Sometimes the following injection is useful:

\begin{code}

open import Two

number : ₂ → ℕ
number ₀ = 0
number ₁ = 1

\end{code}