[neel_k]

I haven't used Lean, but looking at its documentation, it supports universe polymorphism, very much like Agda. This means that there are countably many named universe levels, with each numbered universe containing the universe below it.

All of these numbered universes live inside of a top-most universe which contains all the types and universes. You can't quantify over the topmost universe, for exactly the same reason you can't form the set of all sets in ordinary set theory.

If you do pencil-and-paper mathematics particularly pedantically, when you define something like id, you will say you are working in Tarski-Grothendieck set theory, and then be careful to call it a "definition schema", rather than a "definition", because you are "really" giving a family of definitions, once for each Grothendieck universe. Distinguishing schemas and definitions is a little inconvenient on a computer -- the naive implementation forces you to implement everything twice -- and so one extra top universe is introduced as a home for all of the smaller universes. (Though Mizar apparently chooses to support universe-generic definitions, and to explain them to users as schemas.)

IME, these issues are generally ignorable, both on paper and on computers. Harper and Pollack gave an algorithm for inferring universe levels in the early 90s, and apparently it worked so well that they were worried their implementation was wrong (ie, would always say OK). So they carefully coded up various set-theoretic paradoxes in type theory and were relieved to discover their implementation rejected them.

[pron]

OK, so `id` is basically syntax (or access to the meta-language) for a schema. Thanks for explaining that! In Lean you can certainly feel this sometimes, as you can't even write the proposition `id = id` or `id id = id`. I guess there is no escaping such mechanisms in consistent formalisms, but I've found myself running against such subtleties much more often in Lean than in TLA+, and certainly far sooner (giving me a persistent feeling that I don't really get it). For example, the entire universe hierarchy is something to be aware of from the start (even though Prop is exempted from it), and is completely accidental complexity (necessitated by the chosen formalism, but still) from the perspective of someone just interested in specifying and verifying programs. I think that in most, though not all, cases, TLA+ has a somewhat better story in that regard. For example, definitions parameterized over the domain of the entire universe are syntactically distinct from functions (even in the use-site), and access to the meta-language, required in order to universally quantify over formulas when writing theorems/axioms that serve as inference rules (e.g. well-founded induction), is done in a way that's syntactically distinct from formulas.

When playing with Lean (and I guess the feeling may go away if I ever invest enough time to become proficient in it) I feel like fighting the formalism, which works hard to maintain consistency while having formulas represent "intensional" objects (meaning objects other than true/false), which is a feature that may be very interesting to logicians, but as a practitioner, it feels like paying a high price for something I absolutely don't need. HOL should be simpler, but the Isabelle/HOL tutorials are seriously lacking, and the whole quoting system there is a lot of accidental complexity that I didn't want to bother with.