Natural numbers

\begin{code}

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

module NaturalNumbers where

open import Universes

data  : Set where
  zero : 
  succ :   

{-# BUILTIN NATURAL  #-}

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

_^_ : {X : 𝓤 ̇ }  (X  X)    (X  X)
(f ^ n) x = rec x f n

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)

\end{code}