Level universe

[fredrik-bakke]

Currently, the library is blocked from enabling the --level-universe option globally due to a single definition, namely telescope. Although telescope is a very useful construction, having --level-universe enabled is also advantageous, for instance in modal type theory, where we currently have to distinguish between crisp and cohesive universe levels. Something which doesn't really make sense and leads to trouble.

One route that reconciles having both telescope and --level-universe is to enable the --cumulativity option. This gives small-telescope the same expressivity as telescope has currently, but comes with its own set of advantages and disadvantages:

• It allows us to completely disregard raise-... constructs, and perhaps we will be able to infer telescopes without using the instance resolution mechanism.

On the other hand

• As far as I have found, it is not established that HoTT with cumulative universes admits semantics in all $\infty$-topoi. In Shulman's original article, he expressively states that he does not consider cumulative universes. Andras Kovacs has an article developing some semantics for cumulative universe hierarchies, but it does not seem to get so far as to establish the result we want: Generalized Universe Hierarchies and First-Class Universe Levels. However, at the same time, the larger HoTT community seems to have embraced cumulativity, so I don't know if this is particularly controversial.
• Apparently, the universe-solving mechanisms of Agda are underdeveloped for cumulativity, hence perhaps this will hurt ergonomics or slow down type-checking times.

[EgbertRijke]

Perhaps we should be looking for a modification of the definition of telescopes. I would much prefer that over enabling universe cumulativity.