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?