In Agda, the levels themselves form a type; this simplifies some things, and makes other things more complicated; on the other hand, Bezem, Coquand, Dybjer, and Escardó have proposed a stratified system in which levels can be abstracted but are not organised into an actual type. The main comment I would like to make here is that the formulation of universe heirarchies that I have described above will work regardless of whether levels form a type. The main syntactical challenge is to implement the smallness and inequality judgements, but is easily done in the style of Allais, Mc Bride, and Boutillier as recently reformulated by Corbyn et al.. Put in terms of the latter, the type of universe levels is the free semilattice with successor on the presheaf of neutral terms of level type; and it is easy to decide equality in free semilattices with successor.
A semantic challenge for Agda-style levels is that the semilattice laws are very strict, and so an interpretation into a higher-topos model might be a problem; for example, we cannot rely on the natural numbers being strict in every model of HoTT, which means that the semilattice laws might not hold definitionally. But we can stratify things in such a way that the type of levels is not small for any universe; then the universe levels could be interpreted as the “exo-naturals” in the extensional outer-layer of two-level type theory, which is conservative over HoTT.