<p>Just because you can always embed a lower-order type into the higher-order universe doesn't imply that the reverse is true.  </p>

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

CC BY-SA 3.0
2011-06-04T22:40:27.207Z
Ok, I see. It does mean Boolean is of type Type₁, Type₂, etc. and that we have dependent types because of this?
Anthony
CC BY-SA 3.0
2011-06-05T01:35:34.803Z
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
CC BY-SA 3.0
2011-06-05T01:38:09.980Z
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
CC BY-SA 3.0
2011-06-04T22:35:29.333Z
2011-06-04T22:35:29.333Z
Marc Hamann
<p>Please help me understand some type theory research.</p>

<p>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.</p>

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

<p>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?</p>

<p>How does this differ from a predicative type theory where Type : Type?</p>

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

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

<p>where the types of α, β and the resulting formation are (implicitely) required to be equivalent, right?</p>

<lo.logic><type-theory><functional-programming><type-inference><dependent-type>
Implications of the rule of cumulativity in the Calculus of Constructions
Anthony
# Implications of the rule of cumulativity in the Calculus of Constructions

(Asked by: username_0 on 2011-06-04)

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?

**Tags:** lo.logic, type-theory, functional-programming, type-inference, dependent-type

---

## 1 answers

### Answer by username_1 on 2011-06-04. Score: 8 | Accepted answer

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.

> **Comments:**
> **username_0**: Ok, I see. It does mean Boolean is of type Type₁, Type₂, etc. and that we have dependent types because of this?  
> **username_1**: 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.)  
> **username_1**: 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.  

---

