<p>Say that a universe $U$ is <em>impredicative</em> 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$.</p>

<p>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.</p>

<p>Of course, we recognize that the case $U = \{\emptyset, \{\emptyset\}\}$ is just the case when $U$ is the set of <em>truth values</em>, 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.</p>

<p>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$.</p>

<p>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 <em>two</em> impredicative universes such that one is a member of the other, because one can then cook up a Burali-Forti paradox.</p>

CC BY-SA 3.0
2014-05-11T15:48:24.707Z
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).
Konstantin Solomatov
CC BY-SA 3.0
2014-05-11T16:18:08.337Z
May I ask why you're learning this stuff?
Andrej Bauer
CC BY-SA 3.0
2014-05-11T19:13:23.447Z
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.
Konstantin Solomatov
CC BY-SA 3.0
2014-05-11T07:39:46.700Z
2014-05-11T15:48:12.973Z
2014-05-11T15:48:12.973Z
Andrej Bauer
<p>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.</p>

<p>Why it was done in this way? Will anything bad happen in such a case? </p>

<p>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>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.P.P.S. UTT is described in Luo's PhD thesis and book here: <a href="http://www.cs.rhul.ac.uk/home/zhaohui/books.html" rel="nofollow">http://www.cs.rhul.ac.uk/home/zhaohui/books.html</a></p>

CC BY-SA 3.0
2014-05-11T07:17:34.973Z
Question would be more readable if you expanded some of the acronyms. Also, a well-formulated question should not require several PSs.
Dave Clarke
CC BY-SA 3.0
2014-05-11T08:24:56.803Z
I'll let Konstantin expand "UTT".
Andrej Bauer
CC BY-SA 3.0
2014-05-11T15:57:33.840Z
@DaveClarke What is PS?
Konstantin Solomatov
CC BY-SA 3.0
2014-05-11T16:01:02.163Z
PS is P.S. without the does.
Dave Clarke
CC BY-SA 3.0
2014-05-11T20:44:42.360Z
@DaveClarke Ok. I will try to formulate question better the next time.
Konstantin Solomatov
CC BY-SA 4.0
2019-06-18T07:49:05.910Z
FWIW, I doubt that Agda and Idris use UTT, as they are completely predicative, and based on MLTT with countably many universes.
Blaisorblade
<lo.logic><type-theory><dependent-type>
Rules about Prop and Set in UTT
Konstantin Solomatov
# Rules about Prop and Set in UTT

(Asked by: username_0 on 2014-05-11)

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>

**Tags:** lo.logic, type-theory, dependent-type
> **Comments:**
> **username_1**: Question would be more readable if you expanded some of the acronyms. Also, a well-formulated question should not require several PSs.  
> **username_2**: I'll let Konstantin expand "UTT".  
> **username_0**: @DaveClarke What is PS?  
> **username_1**: PS is P.S. without the does.  
> **username_0**: @DaveClarke Ok. I will try to formulate question better the next time.  
> **username_3**: FWIW, I doubt that Agda and Idris use UTT, as they are completely predicative, and based on MLTT with countably many universes.  

---

## 1 answers

### Answer by username_2 on 2014-05-11. Score: 8 | Accepted answer

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.

> **Comments:**
> **username_0**: 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).  
> **username_2**: May I ask why you're learning this stuff?  
> **username_0**: 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.  

---

