coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
- [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
Archive powered by MHonArc 2.6.18.