When is cumulative type universes useful?

AFAIK, a hierarchy of type universe(Type^0: Type^1: Type^2: ...) was introduced to avoid inconsistency caused by Type: Type.

But some functional language(e.g. Idris) also allows subtyping of these type universes(x: Type^n then also x: Type^n+1). From my understanding, this is not mandatory to solve the inconsistency. So it leads me to guess there should be some advantages from this redundant subtyping rule.

When is cumulative type universes useful?

Without cummulative universes, if you have $A : \mathsf{Type}_3$ then you do not have $A : \mathsf{Type}_7$. Instead, we also have to introduce lifting functions $\iota_{i,j} : \mathsf{Type}_i \to \mathsf{Type}_j$ for all $i \leq j$ and write $\iota_{3,7}(A)$ to port $A$ from the third universe to the seventh one. But this is not all, we also want to know whether $\iota_{3,5}(\iota_{5,7}(A)) = \iota_{3,7}(A)$, i.e., can we lift in several steps? So we need to add a bunch of equations $\iota_{i,j}(\iota_{j,k}(A)) = \iota_{i,k}(A)$ for $i \leq j \leq k$. And this is not all, we also need things like $\iota_{i,i}(A) = A$ and $\iota_{i,j}(\Pi(x : A), B(x)) = \Pi (x : A) \iota_{i,j}(B(x))$, and on and on. It's all very annoying.

With cummulative universes we can just drop all the lifting functions $\iota_{i,j}$.

So why would anyone reject cummulative universes? There are several reasons. An important one is that with cummulative universe it is not true that every expression has at most one type, since a type is an element of many universes. This complicates various algorithms for inferring and checking types. Another reason is semantic: there are interesting models of type theory in which universes are not cummulative.

StackExchange Computer Science Q#120421, answer score: 7