Fuss-free universe hierarchies › So you want a coherent universe hierarchy… [01HY]

Someone who wishes to deploy modern elaboration technology to achieve an implicit source language, however, must think very carefully about the algebraic formulation of the core language to ensure that it has enough equations to maintain predictable behaviour under the implicit Russell-style notation. For example, if the level coercions are not coherent enough, it is easy to create unacceptable error messages that appear to the user like “Could not unify A -> B with A -> B.” Unfortunately, strong enough core languages are very laborious to specify and implement; for example, you will need the following (or some variation):

1. You need top-level type constructors for all type theoretic connectives.
2. For each universe level i, a type U[i] : Type and a dependent type el[i] : U[i] -> Type and codes closing U[i] under all type theoretic connectives, including codes for U[j] with j<i. The el[i] operation needs to commute strictly with the type constructor codes.
3. For universe levels i <= j, you need a lifting operation lift[i<=j]: U[i] -> U[j] that commutes with all type constructor codes and is, moreover, definitionally functorial in the level preorder.
4. You need el to commute with lift. (Thanks to Meven Lennon-Bertrand for catching this!)
5. You need both lift[i<=j] and el[i] to be definitionally injective.

There could be ways to refactor the above; for example, you could get rid of the top level of types altogether and just have universes. This is sometimes referred to as “universes à la Coquand”. Although admirable for its parsimony, I no longer like this approach because I agree with Per Martin-Löf that types and their elements are different concepts. And, for engineering purposes, although it seems at first easiest to have only universes, I think there are subtle ways in which that choice can make other aspects of the implementation more complicated. I think the importance of a separate top-level notion of type is argued for very well in the recent paper of Bezem, Coquand, Dybjer and Escardó.

Anyway, this is a lot to implement in the kernel of a proof assistant.