[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
There are several reasons to be interested in universe hierarchies, among which (1) the question of the ordinal strength of the resulting type theory, (2) the ability to reflect a fragment of the type theory of interest into itself to study it internally, and (3) usability questions arising from the inconvenience, in practice, of predicative universes. Erik's answer gives a lot of information on (1) and (2), but I have a comment on (3). If I understand correctly, Agda today has a finite hierarchy of universes that are types, and a Set-omega sort (that is not a type) to classify universe-polymorphic declarations. It is natural to think of extending this hierarchy with sorts (omega+n) (making Set-omega a type), and then one would extend quantification on universe levels to something of the form (forall (i < l)) for an ordinal level l. However, my intuition would be that this does not deliver much usability benefits in practice. We use universe-polymorphic definitions to get genericity (from a programming point of view, we think of it as SystemF-style impredicative quantification), and then sometimes we find that we cannot compose two generic things as it would require going above Set-omega. But in practice with a transfinite hierarchy you would likely run into the same trouble: if two independent generic definitions quantify in the strongest possible way, they clash, and otherwise one can be used under the other but not conversely. When you develop in the large, you would still need to synchronize universe constraints among the various libraries to compose them in the way you intend; in fact, it is likely that in practice you could (given a coherent policy for universe numbering among the libraries of your development) lift that back to finite universes equipped with finite bounded quantification. For this reason, I have generally considered that extending the ordinal hierarchy you have access to isn't actually so important. If you don't ask for ordinals that are very strong (say, if you are happy with the m*omega+k, or below epsilon0), my understanding is that the metatheory would not be harder than it is today with finite universes and universe quantification, but the usability of the resulting system also wouldn't be very different. On Tue, Jul 10, 2018 at 11:00 PM Stefan Monnier <monn...@iro.umontreal.ca> wrote: > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list > ] > > > Most type theory-based tools nowadays are based on a calculus with an > infinite hierarchy of predicative universes. Some of them, such as > Agda, also allow abstraction over those levels, so we end up with a PTS > along the lines of: > > ℓ ::= z | s ℓ | ℓ₁ ∪ ℓ₂ | l (where `l` is a level variable) > > S = { Type ℓ, Type ω, SortLevel } > A = { Type ℓ : Type (ℓ + 1), TypeLevel : SortLevel } > R = { (Type ℓ₁, Type ℓ₂, Type (ℓ₁ ∪ ℓ₂)), > (SortLevel, Type ℓ, Type ω), > (SortLevel, Type ω, Type ω) } > > I was wondering if there's been work to push this to larger ordinals, to > allow maybe rules like > > (Type ω, Type ω, Type (ω·ω)) > > I.e. "deep universe polymorphism" > > > Stefan >