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

  • 4
    $\begingroup$ Question would be more readable if you expanded some of the acronyms. Also, a well-formulated question should not require several PSs. $\endgroup$ Commented May 11, 2014 at 7:17
  • 2
    $\begingroup$ I'll let Konstantin expand "UTT". $\endgroup$ Commented May 11, 2014 at 8:24
  • $\begingroup$ @DaveClarke What is PS? $\endgroup$ Commented May 11, 2014 at 15:57
  • $\begingroup$ PS is P.S. without the does. $\endgroup$ Commented May 11, 2014 at 16:01
  • $\begingroup$ @DaveClarke Ok. I will try to formulate question better the next time. $\endgroup$ Commented May 11, 2014 at 20:44

1 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.

  • 1
    $\begingroup$ Thank you very much! I can't imagine how I would find this out without your answer (and learn dep types without your other answers here). $\endgroup$ Commented May 11, 2014 at 15:48
  • $\begingroup$ May I ask why you're learning this stuff? $\endgroup$ Commented May 11, 2014 at 16:18
  • 1
    $\begingroup$ Basically, I want to understand tradeoffs which we have when we design dependently typed language, to implement one myself (I already implemented a language which is similar to what you implemented in your blog but with inductive types). I am doing this, since I want to apply projectional editors, the thing which I am working at JetBrains, to dependent types and I feel that it's the area where they are currently most useful. Since the length of the comment is limited I will write you email, where I explain this in more detail. $\endgroup$ Commented May 11, 2014 at 19:13

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.