Martin Escardo 2011.

\begin{code}

{-# OPTIONS --without-K --exact-split --safe #-}

module Naturals where

open import SpartanMLTT
open import DiscreteAndSeparated

data  : Set where 
  zero :               
  succ :          

{-# BUILTIN NATURAL  #-}

rec : {X : U}  X  (X  X)  (  X)
rec x f zero = x
rec x f (succ n) = f(rec x f n)

induction : {A :   U}  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 = ap pred

ℕ-discrete : discrete  
ℕ-discrete 0 0 = inl refl 
ℕ-discrete 0 (succ n) = inr (λ())
ℕ-discrete (succ m) 0 = inr (λ())
ℕ-discrete (succ m) (succ n) =  step(ℕ-discrete m n)
  where 
   step : m  n + (m  n)  succ m  succ n + (succ m  succ n) 
   step (inl r) = inl(ap succ r)
   step (inr f) = inr s  f(succ-injective s)) 

open import Two
open import DecidableAndDetachable

≡-indicator :  (m : )  Σ \(p :   𝟚)  (n : )  (p n    m  n) × (p n    m  n)
≡-indicator m = co-characteristic-function (ℕ-discrete m)

χ≡ :     𝟚
χ≡ m = pr₁ (≡-indicator m)

χ≡-spec : (m n : )  (χ≡ m n    m  n) × (χ≡ m n    m  n)
χ≡-spec m = pr₂ (≡-indicator m)

_≡[ℕ]_ :     U
m ≡[ℕ] n = (χ≡ m n  )

infix  30 _≡[ℕ]_

≡-agrees-with-≡[ℕ] : (m n : )  m  n  m ≡[ℕ] n
≡-agrees-with-≡[ℕ] m n =  r  Lemma[b≢₀→b≡₁]  s  pr₁(χ≡-spec m n) s r)) , pr₂(χ≡-spec m n)

-- We don't need the following anymore:

≢-indicator :  (m : )  Σ \(p :   𝟚)  (n : )  (p n    m  n) × (p n    m  n)
≢-indicator m = indicator(ℕ-discrete m)

χ≢ :     𝟚
χ≢ m = pr₁ (≢-indicator m)

χ≢-spec : (m n : )  (χ≢ m n    m  n) × (χ≢ m n    m  n)
χ≢-spec m = pr₂ (≢-indicator m)

_≠_ :     U
m  n = (χ≢ m n  )

infix  30 _≠_

≠-agrees-with-≢ : (m n : )  m  n  m  n
≠-agrees-with-≢ m n = pr₂(χ≢-spec m n) ,  d  Lemma[b≢₀→b≡₁] (contra-positive(pr₁(χ≢-spec m n)) d))

-- up to here. But I will keep it anyway.

\end{code}

Sometimes the following injection is useful:

\begin{code}

open import Two

number : 𝟚  
number  = 0
number  = 1

\end{code}