# Implications of the rule of cumulativity in the Calculus of Constructions

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?

• We get dependent types because a Set types can used as parameter to create another type. (That's what the $\Pi$-formation rule is saying.) – Marc Hamann Jun 5 '11 at 1:35
• And, yes, you can continue to use $Type_1$ values at the $Type_2$ level as though they were native to that level. This allows you to mix types from different lower levels together as parameters to a higher-level type. – Marc Hamann Jun 5 '11 at 1:38