A type universe is a type of small types that is closed under the basic type formation operations (dependent product, sum, coproduct etc.), that is to say for example that from


* $A \colon U\_i$ and
* $x \colon A \vdash B[x] \colon U\_i$


derive $\prod(x\colon A).B[x] \colon U\_i$.


I haven't yet found anything in my reading that discusses the effects of having


* $\prod(x\colon A).B[x] \colon U\_i$,
* $A \colon U\_{i+1}$ and
* $x \colon A \vdash B[x] \colon U\_{i+1}$


derivable, but $A \colon U\_i$ and $x \colon A \vdash B[x] \colon U\_i$ not derivable.


Does anything interesting arise if we require the converse of type formation rules to hold, and add in "type formation conditions" stating e.g. "from $\prod(x\colon A).B[x] \colon U\_i$ derive $A \colon U\_i$" (or similar things for other types)?


N.B. I've been thinking about this in the setting of Russell-style universes, and am equally unsure what happens in Tarski-style universes.


**Edit** --- I have just realized that my question is somewhat silly in the usual context, where typing judgments are made in the presence of type contexts for variables, which *requires one to derive* $A \colon U\_i$ etc. before being able to derive $\prod(x\colon A).B[x] \colon U\_i$. I am however currently working in a different formulation which needs a bit more explaining, and so I'll add more information soon.



Can a type in a lower universe be formed from types in higher universes?
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](https://coq.inria.fr) 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](https://ncatlab.org/nlab/show/pure+type+system). 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$.


