@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?
@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
