On Wednesday, 1 May 2019 17:55:50 UTC+1, Michael Shulman wrote
Yes, this is a good point in favor of Agda-style non-cumulative
Russell universes over Coq-style cumulative Russell universes.
But isn't there a middle ground with Tarski universes?
It would be nice to have such a middle ground, particularly because formulating universe assumptions in each single definition and theorem is unfamiliar in mathematical practice, and so "typical ambiguity" (pretending there is only one universe) is potentially a good idea for many (or even most) examples. But not in the paper I advertised in this thread.
Here I post an example when Giraud did precisely that, namely to assume two arbitrary universes U and V, explaining why this is needed in that level of generality after the formulation of a theorem and its proof, given to me by Thierry Coquand:
https://www.cs.bham.ac.uk/~mhe/giraud-universes.pdf (photo of one page of a book).
The book is “Cohmologie non abelienne” (1971, https://www.springer.com/gp/book/9783540053071).
Suppose we
have explicit lifting operators Lift : U_i -> U_{i+1}, so that as in
Agda we have unique small polymorphic level assignments. But then
suppose we have *definitional* equalities El(Lift(A)) == El(A). Then
on the (rare) occasions when we do have to explicitly lift types from
one universe to another,
I can confirm from a 26k line Agda development (with comments and repeated blank lines removed in this counting of the number of lines) that not once did I need to embed a universe into a larger universe, except when I wanted to state the theorem that any universe is a retract of any larger universe if one assumes the propositional resizing axiom (any proposition in a universe U has an equivalent copy in any universe V). So I would say that such situations are *extremely rare* in practice.
we would get stronger cumulativity behavior.
(And I could imagine a proof assistant that implements this and sugars
away the El to look like Russell universes to the user.)
At the moment we can choose cumulativity (Coq) or non-cumulativity (Agda), and there is no system that combines the virtues of Coq and Agda regarding universe handling. (And I fear that such a system would potentially multiply the vices of both. :-) )
M.