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