Indeed, homotopy type theory employs a stratified approach to this question. That is, what I've written "U" would more formally be written "U_0". We then have

Indeed, homotopy type theory employs a stratified approach to this question. That is, what I've written "U" would more formally be written "U_0". We then have U_0 : U_1, U_1 : U_2, and so on. All the base types are inhabitans of U_0, that is we have Int : U_0, String : U_0, and so on. In functional programming parlance, we'd have U_0 = Type, U_1 = Kind, U_2 = Sort. There's a thing called "typical ambiguity" which allows us to drop the index in most cases (and let it be automatically inferred).