1
$\begingroup$

One motivation for introducing universes, as I see it, is that without universes, we cannot construct types like $\Pi_{A:\text{Type}}B(A)$ because they would require us to have $\Gamma.\text{Type}\vdash B \text{ type}$, which would require $\Gamma.\text{Type}$ to be a valid context, but it's not a valid context because $\Gamma \vdash \text{Type} \text{ type}$ is not derivable, unless we make this declaration, and such a declaration corresponds to the introduction of a universe $\text{Type}$ (which I will call $U$ below).

This is in contrast to the type $\Pi_{x:A}B(x)$ that can be constructed: if $\Gamma\vdash A \text{ type}$, then $\Gamma.A$ is a valid context, so we can cansider $\Gamma.A\vdash B$ and hence we can construct the type $\Pi_{x:A}B(x)$.

But still I see one problem. Suppose we have a universe $U$:

$$\frac{}{\Gamma \vdash U \text{ type}} \quad \frac{\Gamma \vdash a:U}{\Gamma \vdash \text{El}(a) \text{ type}} $$

Now this rule is provable:

$$\frac{\Gamma \vdash U \text{ type}\quad \Gamma.U\vdash B\text{ type}}{\Gamma\vdash \Pi_{c:U}B(c) \text{ type}}$$

But I don't see how this solves the problem of being able to have type $\Pi_{A:\text{Type}}B(A)$. The above rule only lets us form $\Pi$-types with codes that populate the universe, not with the actual types that correspond to those codes. My question is whether it is possible to formalize "$\Pi_{A:\text{Type}}B(A)$" with universes, and if not, then the motivation for universes that I provided at the beginning turns out to be incorrect, correct?

$\endgroup$

1 Answer 1

1
$\begingroup$

$\mathrm{El}$ is how you get the type corresponding to a code. So, wherever you would imagine $A$ occurring in $B$, instead $\mathrm{El}(a)$ occurs. This makes $B$ into a family over the universe instead of a family 'over types' (which don't exist in Martin-löf type theory).

For instance, a polymorphic identity function would have type:

$$\prod_{a:U}\mathrm{El}(a) → \mathrm{El}(a)$$

$\endgroup$

Your Answer

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

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