In Ulf Norell's PhD thesis, which is considered the standard reference of the Agda 2 language, the universes are cumulative, say,
Set i is not just an instance of
Set (suc i), but also a subtype of it.
However, in the implementation of Agda, this is not true. We only have the "instance of" relation, not the subtype relation, until recently (
IMO, it is good to have more flexibility, but why would Agda developers delete this in the beginning? What inconveniences or problems did cumulative universes bring to us?