# Adding type constructors to universes

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?

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.