Implications of the rule of cumulativity in the Calculus of Constructions
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.