Natural numbers

\begin{code}

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

module MLTT.NaturalNumbers where

open import MLTT.Universes
open import MLTT.Natural-Numbers-Type public

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}
