Skip to Content.
Sympa Menu

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

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" ?


Chronological Thread 
  • From: Matej Kosik <5764c029b688c1c0d24a2e97cd764f AT gmail.com>
  • 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 11:43:07 +0100
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=5764c029b688c1c0d24a2e97cd764f AT gmail.com; spf=Pass smtp.mailfrom=5764c029b688c1c0d24a2e97cd764f AT gmail.com; spf=None smtp.helo=postmaster AT mail-lf0-f51.google.com
  • Ironport-phdr: 9a23:x/Au2BS4vfFSX+cBaiKHefzAi9psv+yvbD5Q0YIujvd0So/mwa6yZxeN2/xhgRfzUJnB7Loc0qyN4vymBTVLucfJmUtBWaQEbwUCh8QSkl5oK+++Imq/EsTXaTcnFt9JTl5v8iLzG0FUHMHjew+a+SXqvnYdFRrlKAV6OPn+FJLMgMSrzeCy/IDYbxlViDanb75/KBq7oR/eu8ULjoduNqI8wQbVr3VVfOhb2XlmLk+JkRbm4cew8p9j8yBOtP8k6sVNT6b0cbkmQLJBFDgpPHw768PttRnYUAuA/WAcXXkMkhpJGAfK8hf3VYrsvyTgt+p93C6aPdDqTb0xRD+v4btnRAPuhSwaMTMy7WPZhdFqjK9DvRyvuRJ/zY7Xbo+bOvVxcaHScs8VS2daQsZcVDZMDp+gY4YBDecMO/tToYnnp1sJqBuzHQ6iC/nzyjBWhH/9wKg00+M6EQHH3wwrAtUDvXTWodj0O6odTfy5wLfMwDrYbv5b2jTw55TVfh89vf2DQKx8fMXLxkUxCQzIiledppD4MD6X1+kAvGab4vFvVeKqkWEnqgVxriKzyccrj4nEn4QYwU3H+yVh2Is5O8G0RUphbdOnEJZcrT+WO5Z2T884Q2xkpT42xqACtJO1ZiQHyIkrywTBZ/CbcIWE+A/vWemQLDp+mXlrYqiwhwyo/kil0uD8Vte70FJNriddl9nDrHEN1xjK5siDRPtx4l6t2TiP2gzO8O1ELkc0la3UK54l3LE8jIYcsUPGHiPumUX2irGZdlk89+S29+jqZq/qq5ycOoNulA3yL6Qjlta/DOglKgQOWnKU+eW41L3t5035R7BKg+U2n6TbsZ3XKtgUqrKnDwJRyYku6hWyAjS639gFgXYLME9KdAyIgofzJV3BPvT1APWjjFuxkjpmxv/LPrP6D5XCK3jMirbhfbJn50FAzwozyMhT54hIBbEZPPLzRkjxucTEAR8+Kgy42vroCNFg1owFQm+PGa+YMKbKsVCS/O4vIu+MZJUUuDnnMfQl6eTu3jcFngoWerDs1p8KYli5GO5nKgOXeynCmNAEREIDogc8BM/tk1yBGWoOOCjuVPpmtztlWNKtVIybStrxieaMjXiwEsIIOm5uBVWFEHOufIKBDaRfIBmOK9Nsx2RXHYOqTJUsgEmj
Hi Guillaume,

On 01/18/2017 10:27 PM, Guillaume Melquiond wrote:
> On 18/01/2017 17:30, Matej Kosik wrote:
>> My question is about weakening (not strengthening)
>>
>> Prop < Set
>>
>> to
>>
>> Prop <= Set
>
> Théo already explained it, so I just want to stress the important part
> of his answer. "Prop < Set" does not mean that Prop is of type Set, it
> just means that Prop is smaller than Set. In other words, any type of
> Prop is a type of Set (but the converse does not hold).

That is an interesting question
(If "X < Y", could we then conclude that "X : Y")
but this is not what I wanted to ask now.

My question is, why do we insist upon universe constraint "Prop < Set"
instead of "Prop ≤ Set"?
--
Matej Košík

Archive powered by MHonArc 2.6.18.

Top of Page