When should I use data types vs calculating types

When should I prefer creating data types vs calculating types?

Concrete example - given:

data Zero : Set where

record One : Set where

data Nat : Set where
  zero : Nat
  suc : Nat -> Nat

and wanting to define \lt, what are the advantages and disadvantages of each of these:

-- a new datatype
data _<_ : Nat -> Nat -> Set where
  ozero : {n : Nat} -> zero < suc n
  osuc : {n m : Nat} -> n < m -> suc n < suc m

vs

-- calculating
_<_ : Nat -> Nat -> Set
zero < zero = Zero
zero < suc m = One
suc n < zero = Zero
suc n < suc m = n < m

So far I've got these:

• I remember/have seen is that the second one makes it harder for agda to infer implicit arguments sometimes (?)
• the first one should use more memory (?)
• the second datatype is more useful when you want agda to be able to infer your less than proof as an implicit argument, e.g. when your its arguments are constants/inferrable