coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Why is [Prop] not in [Set]?

From: Jason Gross <jasongross9 AT gmail.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] Why is [Prop] not in [Set]?
Date: Wed, 25 Jul 2012 14:37:08 -0400

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

[Coq-Club] Why is [Prop] not in [Set]?, Jason Gross, 07/25/2012
- Re: [Coq-Club] Why is [Prop] not in [Set]?, Ryan Wisnesky, 07/25/2012
- Re: [Coq-Club] Why is [Prop] not in [Set]?, Arnaud Spiwack, 07/27/2012