In various sources on intuitionistic type theory, the universe of types is taken to be cumulative, i.e. $A:\mathcal U _i$ implies $A:\mathcal U_j$ whenever $i\le j$.
The question is: why do we have to assume that? Is there any unavoidable difficulty if we do not use it (that way elements always have unique types)? And, what are the subtleties involved in each situation?
Thanks in advance!
It's done because it seems natural, and it avoids some tedium of having to explicitly
liftterms in one universe to a higher universe. It's essentially just a subtyping constraint, and instead of having implicit coercions, you can have explicit coercions, i.e. thelifts. I believe one of the reasons Agda doesn't have cumulativity is that it doesn't interact well with universe polymorphism (or rather its interactions were not well understood), but you should check that. Subtyping, in general, often leads to gnarly complexities.