The biggest syntactic difference in the given two languages is that universe levels do not have an eliminator as natural numbers do. For instance, you can pattern match over a natural number, and you have decidable equality on natural numbers (say, we can define decEq : (a b : Nat) -> (a = b) \/ (a = b -> ⊥)), while these are all absent from universe levels.

This is also why Level in Agda and levels in Lean are not first-class types (they're built-in types instead). For instance, in Agda Level does not live in a regular universe.

The biggest syntactic difference in the given two languages is that universe levels do not have an eliminator as natural numbers do. For instance, you can pattern match over a natural number, and you have equality decider function on natural numbers (say, we can define decEq : (a b : Nat) -> (a = b) \/ (a = b -> ⊥)), while these are all absent from universe levels.

This is also why Level in Agda and levels in Lean are not first-class types (they're built-in types instead). For instance, in Agda Level does not live in a regular universe.