# In what sense do universes solve the problem of not having type $\Pi_{A:\text{Type}}B(A)$?

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?

$$\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).
$$\prod_{a:U}\mathrm{El}(a) → \mathrm{El}(a)$$