module Naturals where

open import Logic

data ℕ : Set where
     O : ℕ              -- Zero (capital letter Oh).
     succ : ℕ → ℕ       -- Successor.


{-# BUILTIN NATURAL ℕ #-}
{-# BUILTIN ZERO O #-}
{-# BUILTIN SUC succ #-}


induction : {A : ℕ → Ω} →
---------
            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)


head : {A : ℕ → Ω} →
----
       (∀(n : ℕ) → A n) → A 0

head α = α 0


tail : {A : ℕ → Ω} →
----
       (∀(n : ℕ) → A n) → ∀(n : ℕ) → A(succ n)

tail α n = α(succ n)


cons : {A : ℕ → Ω} →
----
       A 0 ∧ (∀(n : ℕ) → A(succ n)) → ∀(n : ℕ) → A n

cons (∧-intro a α) 0 = a
cons (∧-intro a α) (succ n) = α n


prefix : {R : Ω} {A : ℕ → Ω} →
------
          A 0 → ((∀(n : ℕ) → A n) → R) → (∀(n : ℕ) → A(succ n)) → R


prefix α₀ p α' = p(cons (∧-intro α₀ α'))


eq-cases : {X : ℕ → Set} → (i j : ℕ) → X i → X j → X j
eq-cases 0 0 x y = x
eq-cases 0 (succ j) x y = y
eq-cases (succ i) 0 x y = y
eq-cases {X} (succ i) (succ j) x y = eq-cases {λ n → X(succ n)} i j x y


mapsto : {X : ℕ → Set} →
  (i : ℕ) → X i → ((j : ℕ) → X j) → (j : ℕ) → X j
mapsto {X} i x α j = eq-cases {X} i j x (α j)