Definition. Natural Numbers [hca/H007.lagda]

open import Cubical.Foundations.Prelude hiding (_∨_) public

We define the natural numbers as follows.

data ℕ : Type where
  zero : ℕ
  suc : ℕ → ℕ

This is indeed enough and we do not need to worry about them being cyclic, since for any n : ℕ, suc n wont be judgementally equal to zero, unless we define it to be.