coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Why do we have "Prop < Set" ? Why not just "Prop ≤ Set" ?

From: Jacques-Henri Jourdan <jacques-henri.jourdan AT normalesup.org>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Why do we have "Prop < Set" ? Why not just "Prop ≤ Set" ?
Date: Thu, 19 Jan 2017 15:54:02 +0100
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jacques-henri.jourdan AT normalesup.org; spf=Neutral smtp.mailfrom=jacques-henri.jourdan AT normalesup.org; spf=None smtp.helo=postmaster AT ulminfo.fr
Ironport-phdr: 9a23:dRhVRBCrLOa3/wMooS17UyQJP3N1i/DPJgcQr6AfoPdwSP3yocbcNUDSrc9gkEXOFd2CrakV16yK6uu+ACRAuc/H6y9SNsQUFlcssoY/oU8JOIa9E0r1LfrnPWQRPf9pcxtbxUy9KlVfA83kZlff8TWY5D8WHQjjZ0IufrymUt2as8Pi3OervpbXfg9ghTynYLo0Ig/lgx/Ws5w0iIB7N6sqjzvEpGFJM8ZR2HlkLFTbyxT17d6t8YUm8ylWofNn9cldS6nzeYw+SqZdBTArKH0tosrxuk+QHkO0+nIAXzBOwVJzCA/f4USiUw==

Yes, that is what I mean : if you remove -noinit, you cannot access
these definitions, but you can still create them again.

Le 19/01/2017 à 15:09, Dominique Larchey-Wendling a écrit :
> Le 19/01/2017 à 14:07, Jacques-Henri Jourdan a écrit :
>
>> The thing is that Prop and Set DO HAVE inhabitants, and some of the ones
>> of Set are not in Prop. Always. Even when using -noinit, because you can
>> always redefine the standard library logical connectives using
>> inductives, which are primitive in the logic.
> Well actually, "exists", /\, \/, True and False are inductively defined
> in the standard library ...

Attachment: signature.asc
Description: OpenPGP digital signature

Re: [Coq-Club] Why do we have "Prop < Set" ? Why not just "Prop ≤ Set" ?, (continued)