7
$\begingroup$

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?

Improve this question
$\endgroup$

1 Answer 1

Reset to default
8
$\begingroup$

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.

Improve this answer
$\endgroup$
3
  • $\begingroup$ Ok, I see. It does mean Boolean is of type Type₁, Type₂, etc. and that we have dependent types because of this? $\endgroup$
    – Anthony
    Jun 4, 2011 at 22:40
  • 1
    $\begingroup$ 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.) $\endgroup$
    – Marc Hamann
    Jun 5, 2011 at 1:35
  • 1
    $\begingroup$ 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. $\endgroup$
    – Marc Hamann
    Jun 5, 2011 at 1:38

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.