@MartinEscardo
I had a question about univalent mathematics and I was told you'd be the one to ask. I hope you don't mind
Reading the HoTT book I noticed that they defined universes to be cumulative. This surprised me because in theorem provers such as Lean and allegedly Agda (I was told), this is not the case. In the book itself they mention a downside of having cumulative universes being that a term no longer has a unique type, but they don't mention any advantages of constructing them this way.
Therefore, my question is: what is the advantage of having cumulative type universes?
@mra Aaah, that must have been why I was suggested to talk with Martin Escardo then. Thanks for the link!
If I understood correctly from the page, the advantages are purely operational. Cumulative universes seem to be a relaxation to more easily allow the definition of certain functions, and for instance prevents having to implement a function twice, once for the value computation and once for the universe level computation.
So I guess it's used in the HoTT book since it leads to potentially cleaner definitions, but left out of theorem provers since terms having a unique type is desirable.
@ayhon yeah, this sounds about right. it doesn't really seem to meaningfully change the type theory at all. it's more or less a purely aesthetic choice, as far as i can see
(1) I don't generally have trouble with the lack of cumulativity, and personally find the non-cumulative system more natural, e.g. because of unique typing.
(2) As others said, there is an experimental cumulativity flag in Agda, but I haven't tried it.
@ayhon @MartinEscardo agda has optional cumulative universes (see: https://agda.readthedocs.io/en/stable/language/cumulativity.html). the page also explains some of the reasons that cumulative universes are desirable, at a skim