The Coq mailing list

[Ryan Wisnesky <ryan AT cs.harvard.edu>]

I think Coq's choice is one of many - for example, some Coq developments 
avoid [Prop] altogether, as in homotopy type theory or using impredicative 
sets as props.  I'm not sure why Coq settled on this particular choice, 
however.

On Jul 25, 2012, at 2:37 PM, Jason Gross wrote:

> Hi,
> I've been wondering for a little while now why [Prop] is not in [Set], but 
> in [Type (* (Set)+1 *)].  My intuition says that any proof about why 
> propositions (which can quantify over [Set]s, [Type]s, etc.) do not form a 
> set should also say that the type of all propositions which can quantify 
> over Type(i) (and lower) is not a Type(i).
> 
> Thanks!
> 
> -JAson