data Nat : Set where
  zero : Nat
  suc  : Nat @$\rightarrow$@ Nat