Peano axioms in Agda

PeanoAxioms.agda

-- http://en.wikipedia.org/wiki/Peano_axioms

module PeanoAxioms where

data ⊥ : Set where -- empty

data ℕ : Set where
  -- [1] 0 is a natural number.
  zero : ℕ
  -- [6] For every natural number n, S(n) is a natural number.
  suc : ℕ → ℕ

-- [5] Natural numbers are closed under equality.
data _≣_ (n : ℕ) : ℕ → Set where
  -- [2] Equality is reflexive.
  refl : n ≣ n

infix 4 _≣_

-- [3] Equality is symmetric.
sym : {m n : ℕ} → m ≣ n → n ≣ m
sym refl = refl

-- [4] Equality is transitive.
trans : {a b c : ℕ} → a ≣ b → b ≣ c → a ≣ c
trans refl refl = refl

-- [7] There is no natural number n where S(n) = 0.
zero-init : {n : ℕ} → suc n ≣ zero → ⊥
zero-init ()

-- [8] S is an injection.
suc-inj : {m n : ℕ} → suc m ≣ suc n → m ≣ n
suc-inj refl = refl

-- [9] Induction! Yay!
ind : (P : ℕ → Set)
    → ((m : ℕ) → P m → P (suc m))
    → P zero
    → (n : ℕ) → P n
ind P f z zero    = z
ind P f z (suc n) = f n (ind P f z n)