\begin{code} {-# OPTIONS --without-K --exact-split --safe --no-sized-types --no-guardedness --auto-inline #-} module MLTT.Natural-Numbers-Type where data ℕ : Set₀ where zero : ℕ succ : ℕ → ℕ {-# BUILTIN NATURAL ℕ #-} \end{code}