4
$\begingroup$

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

$\endgroup$
  • 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$ – Dave Clarke May 11 '14 at 7:17
  • 2
    $\begingroup$ I'll let Konstantin expand "UTT". $\endgroup$ – Andrej Bauer May 11 '14 at 8:24
  • $\begingroup$ @DaveClarke What is PS? $\endgroup$ – Konstantin Solomatov May 11 '14 at 15:57
  • $\begingroup$ PS is P.S. without the does. $\endgroup$ – Dave Clarke May 11 '14 at 16:01
  • $\begingroup$ @DaveClarke Ok. I will try to formulate question better the next time. $\endgroup$ – Konstantin Solomatov May 11 '14 at 20:44
7
$\begingroup$

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.

$\endgroup$
  • 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$ – Konstantin Solomatov May 11 '14 at 15:48
  • $\begingroup$ May I ask why you're learning this stuff? $\endgroup$ – Andrej Bauer May 11 '14 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$ – Konstantin Solomatov May 11 '14 at 19:13

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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