Rules about Prop and Set in UTT

Question

In Luo's UTT (type theory which is used in Agda, Idris, and other dependently typed programming languages), there're are two rules for $\Pi$ types. One for $\mathsf{Prop}$ and one for $\mathsf{Set}$. In the one for $\mathsf{Prop}$ we have no constraints on the universe of a parameter. In the one for $\mathsf{Set}(i)$, we have.

Why it was done in this way? Will anything bad happen in such a case?

P.S. Basically I want to understand why $\mathsf{Prop}$ has special treatment in the theory. I.e. why we can't choose $\mathsf{Type}(0)$ for propositions, then removed the $\mathsf{Type}(i)$ condition in the $\Pi$ types' argument, and as a consequence have more uniform set of axioms.

P.P.S. In Luo's thesis I read that Calculus of inductive constructions (CIC) where this universe was introduce was created as a mix between Martin-Löf type theory (MLTT) and System F. Does $\mathsf{Prop}$ correspond to the union of all the existing universes?

P.P.P.S. UTT is described in Luo's PhD thesis and book here: http://www.cs.rhul.ac.uk/home/zhaohui/books.html

Answer 1

Say that a universe $U$ is impredicative if the product $\prod_{x : A} B(x)$ is in $U$ whenever $B(x)$ is in $U$ for all $x$, and $A$ is arbitrary, i.e., not necessarily in $U$.

Are there any impredicative universes? Let us think about what an impredicative universe would be for sets: a set $U$ such that for every family of sets $B : A \to U$, no matter how large $A$ is, $\prod_{x : A} B(x)$ is in $U$. That's only possible in two cases: when $U$ contains the singleton (or many copies of it) and when it contains the empty set and the singleton (or many copies of it). This is so because a product of sets which are all singletons or empty is again such a set. If $U$ contains a set $S$ with at least two elements then $S^U$ (which is a special case of a product) will fail to be contained in $U$ for cardinality reasons.

Of course, we recognize that the case $U = \{\emptyset, \{\emptyset\}\}$ is just the case when $U$ is the set of truth values, i.e., $\mathsf{Prop}$. This is one reason why $\mathsf{Prop}$ is treated differently: it is impredicative – not only in classical set theory but also more generally, because truth values are closed under $\forall$. Note that $\forall$ and $\prod$ coincide on families of sets that all contain at most one element.

In system $F$ we have impredicativity because types there are closed under $\forall$ ranging over the whole universe of types, and $\forall$ behaves like $\prod$.

One could hope that there are other models, where for instance $\mathsf{Type}_i$ is impredicative. Indeed, there are realizability models of (extensional) type theory that contain an impredicative universe of sets (as opposed to truth values). However, one cannot have two impredicative universes such that one is a member of the other, because one can then cook up a Burali-Forti paradox.