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)