Adding type constructors to universes

Question

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?

Answer 1

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.
2. • 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.