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}