Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Why is [Prop] not in [Set]?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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


Chronological Thread 
  • From: Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>
  • To: Jason Gross <jasongross9 AT gmail.com>
  • Cc: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Why is [Prop] not in [Set]?
  • Date: Fri, 27 Jul 2012 10:53:00 +0200

Historically, Set was an impredicative sort (e.g. forall A:Set.A->A had type Set). You can summon back this behaviour by giving the flag -impredicative-set to coqtop. Anyway, if Set and Prop are impredicative and Prop:Set, then we have at least system U, which is notoriously inconsistent. So we couldn't have that, then. Nowadays, without the -impredicative-set flag, there is nothing distinguishing Set from a particular Type(i). So there is no particular reason not to consider Prop:Set. I don't why it hasn't been done, maybe to stay compatible with the impredicative Set. Those with the relevant knowledge happen to be on holidays or otherwise away presently.

On a side note, related to homotopy type theory, it has been considered to reintroduce a difference between Set and Type(i): we could have K relative to Set (that is, something like: forall (A:Set) (x y:A) (p q: x=y), p=q). But I'm pretty sure Prop:Set is consistent with this particular axiom.


Arnaud

On 25 July 2012 20:37, Jason Gross <jasongross9 AT gmail.com> 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




Archive powered by MHonArc 2.6.18.

Top of Page