2
$\begingroup$

Suppse we have a Tarski-style universe $U$, which means, in particular, that the following rules are declared: $$\frac{}{\Gamma \vdash U \text{ type}} \quad \frac{\Gamma \vdash a:U}{\Gamma \vdash \text{El}(a) \text{ type}}$$

To introduce dependent product type into $U$, one uses, in particular, thse rules:

$$\frac{\Gamma\vdash a:U\quad \Gamma.\text{El}(a)\vdash b:U}{\Gamma\vdash p(a,b):U} \quad \frac{\Gamma\vdash a:U\quad \Gamma.\text{El}(a)\vdash b:U}{\Gamma\vdash \text{El}(p(a,b))=\Pi(\text{El}(a),\text{El}(b)) \text{ type}}$$

I have two related questions:

  1. The second judgement on the top of the rule $\cfrac{\Gamma\vdash a:U\quad \Gamma.\text{El}(a)\vdash b:U}{\Gamma\vdash p(a,b):U}$ presupposes that $\Gamma.\text{El}(a) $ is a valid context and that $\Gamma.\text{El}(a)\vdash U\text{ type}$. I can see why the former is true, but why is the latter presupposition true?
  2. Why can't we use instead of the rule $\cfrac{\Gamma\vdash a:U\quad \Gamma.\text{El}(a)\vdash b:U}{\Gamma\vdash p(a,b):U}$ the rule $\cfrac{\Gamma\vdash a:U\quad \Gamma.U \vdash b:U}{\Gamma\vdash p(a,b):U}$? $\Gamma.U$ is also a valid context, just like $\Gamma.\text{El}(a)$. Is it because the presupposition $\Gamma.U\vdash U \text{ type}$ cannot be proved? If so, how do I see that? If the reason is different, then what is it?
$\endgroup$

1 Answer 1

2
$\begingroup$
  1. $Γ.\mathrm{El}(a) ⊢ U\ \mathrm{type}$ is valid because $Γ ⊢ U\ \mathrm{type}$ is valid for all $Γ$. Just pick $Γ.\mathrm{El}(a)$ as the context.
    • For one, there is no reason to have the $a$ in that rule. $b$ is a $U$-indexed family of $U$-values. So it's unclear why the $a$ is involved at all.
    • For two, if you get rid of the $a$ and add the likely rule for $\mathrm{El}$, this makes $U$ an impredicative universe, because it is saying that $\prod_{a:U}b : U$. So $U$ contains products that quantify over itself. The usual rule says that $\prod_{x:a}b : U$. You can do this for $Π$, but only once (in a hierarchy). If you have two nested universes that are both impredicative, then that leads to inconsistency. And if you try to have an impredicative $Σ$, that is also inconsistent.
$\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.