I expect you're right that if the only primitive rules for universes are "closure" ones such as

$$\frac{\vdash A:U_i \qquad x:A \vdash B[x] : U_i}{\vdash \prod(x:A). B[x] : U_i}$$

then there should be a metatheorem that whenever $\prod(x:A). B[x] : U_i$ it must have been derived by this rule so that we have $A:U_i$ and $x:A \vdash B[x] : U_i$ as well. (Such metatheorems are generally quite a lot of work to actually prove, so I hesitate to assert that there *is* such a theorem, but it seems plausible to me.)

However, there are type theories containing primitive rules allowing types in smaller universes to be built out of types in bigger ones. Probably the most well-known of these is asking for a small universe such as $U_0$ to be "impredicative" in the sense that it is closed under products of arbitrarily sized domain:

$$\frac{\vdash A:U_i \qquad x:A \vdash B[x] : U_0}{\vdash \prod(x:A). B[x] : U_0}$$

For instance, in the Predicative Calculus of Inductive Constructions that underlies the Coq proof assistant, the universe `Prop`

is impredicative in this sense. The *im*predicative Calculus of Inductive Constructions, which can be turned on by the option `--impredicative-set`

, also includes another impredicative universe `Set`

, although these are "parallel" rather than "sequential" (that is, we have `Prop : Type1`

and `Set : Type1`

but not `Prop : Set`

) --- I believe it is known to be inconsistent to have one impredicative universe containing another impredicative universe, although two "parallel" impredicative universes are known to be consistent (relative to standard set theory).

Vladimir Voevodsky suggested another class of "bigger into smaller" universe rules that he called "resizing rules", and which can be described generally by "adding extra useless junk to a type shouldn't raise its universe level". For instance, one such rule is that if $A:U_i$ and $B : U_j$ for $j>i$, while $A\simeq B$ (an equivalence/isomorphism of types), then $B:U_i$. Another is that if $A:U_i$ and $A$ is a subsingleton (i.e. $\prod(x:A)(y:A). x=y$), then $A:U_0$. As far as I know, none of these rules are known to be consistent.

A general framework for describing and studying type theories containing families of "universes" (not necessarily sequentially ordered) with arbitrarily chosen universe-assignments for the types in the $\prod$-formation rule is pure type systems. A PTS is specified by a set of *sorts* (the universes), a set of *axioms* of the form $s_1:s_2$ for sorts $s_1,s_2$ (specifying which universes belong to which others), and a set of *rules* of the form $(s_1,s_2,s_3)$ each specifying a way to assign universes to the types in $\prod$-formation:

$$\frac{\vdash A:s_1 \qquad x:A \vdash B[x] : s_2}{\vdash \prod(x:A). B[x] : s_3}$$

PTS's are very general and include even the inconsistent theory $U:U$.

definitionallyidentical to "the empty type", so we cannot automatically conclude from this that it belongs to $U_i$. $\endgroup$