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: e+coq-club AT x80.org (Emilio Jesús Gallego Arias)
To: Matej Kosik <5764c029b688c1c0d24a2e97cd764f AT gmail.com>
Cc: 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 14:02:36 +0100
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=e+coq-club AT x80.org; spf=Neutral smtp.mailfrom=e+coq-club AT x80.org; spf=None smtp.helo=postmaster AT cc-tupan-roaming-a.ensmp.fr
Ironport-phdr: 9a23:A5/KCxSL3HVEVKvULDdaETQlqNpsv+yvbD5Q0YIujvd0So/mwa6yZhGN2/xhgRfzUJnB7Loc0qyN4vymBTVLvc/JmUtBWaQEbwUCh8QSkl5oK+++Imq/EsTXaTcnFt9JTl5v8iLzG0FUHMHjew+a+SXqvnYdFRrlKAV6OPn+FJLMgMSrzeCy/IDYbxlViDanb75/KBq7oR/eu8ULjodvJbs9wQbVr3VVfOhb2XlmLk+JkRbm4cew8p9j8yBOtP8k6sVNT6b0cbkmQLJBFDgpPHw768PttRnYUAuA/WAcXXkMkhpJGAfK8hf3VYrsvyTgt+p93C6aPdDqTb0xRD+v4btnRAPuhSwaMTMy7WPZhdFqjK9DoByvuQFxw4naYI+bNvVwfa3SctwGSmRORctRSzVBD5mgY4cTFecMP+BVpJT9qVsUqhu+ABGhC/3oxjBUgX/2xLQ23PglEQHbxwMtBN0PvXfIoNnvM6cSS++1x7TMwTvMavNW2DP96InPchs8pf+DQ6lwadDKyUIyFg3KlFGQqYj7MDOa0eQGrnSW7/BhVe21kG4rrgd8qSWsyMc0koTFm4YYx1/e+Sln3Yo4Kse0RFN7bNOnCpdcqi+XOoluTs8/TWxltzw2xqAGtJO5ZiQG1YoryhHFZ/CacYWF7RTuX/uLLzhinnJqYre/ig6y8Ue+zu38UdG530pWoSZcjtnMq2gN2AbV6sSeUPt9+V2u2TOO1wDV5eFIOFo7mbDFJJ4n2b4wk4ITvV7NHi/sgEn2jamWeVs4+uWw9ujqZrrrqoWCO4NphQzyKLkil8y8DOgiLwQDUWqW9fy51LL5/E35RLtKjucxkqncqJ3VO8MXqbK+Aw9My4os9xK/Dyq939kDkngKL05JdAiAj4jzNFHCOOr4Auung1SwjDdrwOjLMaHmApXUN3TMjLPhfatm5ENH0woyzdVf54pOBb0bIfLzXFXxtN3CARMjPQy02bWvNNIo84oCVGDHIaiCMaCa5QLXuL4ke7PdbtFF6D2kIKApvaLn13JoxlQRIvf107MYbXm5GrJtJEDPMlT2hdJUHCQBuRN7R+j3gnWSAWYVYGy9F+IR4zA/CYXuL4rY1Jvlr7WF2Cq0GdV/fGFPERHfQj/Ta4yYVqJUO2qpKch7n2lcWA==
Organization: X80 Heavy Industries

Hi Matej,

Matej Kosik
<5764c029b688c1c0d24a2e97cd764f AT gmail.com>
writes:

> after starting the toplevel like this:
>
> coqtop -noinit
>
> neither Prop nor Set have any inhabitants and thus it is not the case that
> "Prop < Set".
> The only thing that we can claim is "Prop ≤ Set".

What do you mean by inhabitant? I am not sure what you mean here, but
note that `forall x : Prop, x` is an inhabitant of Prop.

Cheers,
Emilio

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