data @$\mathbb{N}$@ : Set where
  zero : @$\mathbb{N}$@
  suc  : @$\mathbb{N}$@ @$\rightarrow$@ @$\mathbb{N}$@