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: Dominique Larchey-Wendling <dominique.larchey-wendling AT loria.fr>
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:09:26 +0100
Organization: LORIA

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 ...

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