Implications of the rule of cumulativity in the Calculus of Constructions Please help me understand some type theory research.

As suggested in "Type Checking with Universes" by Robert Harper and Robert Pollack, we can add the following rule to our otherwise standard COC or PTS type inference rules.

$$
\frac{\Gamma \vdash M : \text{Type}_{i}}{\Gamma \vdash M : \text{Type}_{i+1}} \text{(Cumulativity)}
$$

Doesn't that mean that if I declare Boolean : Type₀ that Boolean is implicitly of type Type₁, Type₂, and so on? And doesn't that mean that Typeᵢ ≡ Type₍ᵢ₊₁₎ and furthmore that ∀ i, j . Typeᵢ ≡ Typeⱼ by equational reasoning?

How does this differ from a predicative type theory where Type : Type?

Furthermore, this allows us to have dependent types even if our Π-formation rule is written as follows

$$
\frac{\Gamma \vdash \alpha : s \hspace{3em} \Gamma,x :a \vdash \beta : s}{\Gamma \vdash (\Pi x : \alpha . \beta) : s} \text{(}\Pi\text{-formation)}
$$

where the types of α, β and the resulting formation are (implicitely) required to be equivalent, right?
Just because you can always embed a lower-order type into the higher-order universe doesn't imply that the reverse is true.  

The higher-order universe is always strictly larger than the lower-order one, so there is no problem with respect to predicativity.