The Coq mailing list

[Talia Ringer <tringer AT cs.washington.edu>]

Hi all,

Does anyone have a good resource to read about why Prop is impredicative, and why this is desirable? So far, I've found Adam Chlipala's Universes post and some answers to a stackexchange question. I'd like something a little more formal. For example, in the stackexchange post, Cody Roux notes:

> The expressiveness gained by impredicativity is "reassuring" in the sense 99% of "reasonable"
> mathematics can be formalized with it, and it is known to be consistent relative to set theory. This
> makes it likely they won't weaken it to something like Agda, which only has predicative universes.

I want to know more about that expressiveness. Why is it "reassuring," and what is "reasonable"? (I couldn't find a working email address for Cody Roux, or I'd try him as well.) Is it essential, or does it just make some things easier?

Similarly, Adam Chlipala's post has a few interesting examples of things we can do with impredicative Prop, but I'm interested in something broader and more formal. A research paper or talk would be great, if such a thing exists.

Thanks!

Talia

University of Washington