It seems that universe levels are just a type generated by a zero constant and a successor constructor (like in Agda), so why don't we adapt natural numbers as universe levels?
In Lean, it is also similar: one can find the maximum of two levels, add a level variable with a constant (which is just a sugared version of applying successors), and constants.
One of the things that make universe levels “just work”, to some extent, is that they satisfy the idempotent commutative monoid laws judgementally. This means that any elimination form of a universe level would also have to satisfy those laws judgementally. However, this would be basically unusable because there are no other idempotent commutative monoids in standard type theories for it to eliminate into (this contrasts to judgemental monoids and categories, which exist thanks to simple functions equipped with β- and η-laws). In particular, I don't see how such a type could be proven isomorphic to the ordinary zero-suc-based natural numbers, and as such it wouldn't make sense to call them the “natural numbers”.
Modularity.
Clearly, universe levels must form a semi-lattice with a successor. But there is no need to force it to be the set of natural numbers. Doing so would actually result in spurious constraints between unrelated universes, artificially constrained to collapse to some linearly ordered value. By taking a system of free relations, unrelated constraints cannot interfere with one another.
This is as if definitions were forced numbered instead of being given user names. Clearly, it does not endanger the formal expressivity, but it would make the system virtually unusable. (Remember the good old days of BASIC line numbering?)
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.
At some point in history, Agda's universe levels were just an inductive type like the naturals, but with different accompanying BUILTIN declarations so that they could have extra judgmental equalities (mentioned in other answers). So, you could do 'weirder' things than you can do now, like define families that depended on the level, rather than being parametric in the level.
I suspect this doesn't cause any foundational problems. Set theorists don't have any issues indexing their universes by ordinals whose fine structure is observable. Also, I don't think it's impossible to have judgmental associativity/commutativity/idempotence of ⊔ on the naturals, as Agda already has some support for adding additional judgmental equalities like that, and I think they're hoping to extend it further.
However, at the time, it made people uneasy to be able to do the 'weird' stuff mentioned above, it wasn't the intended purpose of the first-class universe levels, and the judgmental equality stuff was not really conceived of. So it definitely made sense at the time to make it a bit less like the natural numbers. And it still probably makes sense, for some of these, and other mentioned reasons.
