Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Modeling Ur Elements

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Modeling Ur Elements


Chronological Thread 
  • From: Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>
  • To: Coq Club <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] Modeling Ur Elements
  • Date: Wed, 3 May 2017 07:36:03 +0200
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=arnaud.spiwack AT gmail.com; spf=Pass smtp.mailfrom=arnaud.spiwack AT gmail.com; spf=None smtp.helo=postmaster AT mail-ua0-f180.google.com
  • Ironport-phdr: 9a23:s3gjlB9WmCSJTP9uRHKM819IXTAuvvDOBiVQ1KB30O4cTK2v8tzYMVDF4r011RmSDNmds6oMotGVmpioYXYH75eFvSJKW713fDhBt/8rmRc9CtWOE0zxIa2iRSU7GMNfSA0tpCnjYgBaF8nkelLdvGC54yIMFRXjLwp1Ifn+FpLPg8it2e2//5Lebx9UiDahfLh/MAi4oQLNu8cMnIBsMLwxyhzHontJf+RZ22ZlLk+Nkhj/+8m94odt/zxftPw9+cFAV776f7kjQrxDEDsmKWE169b1uhTFUACC+2ETUmQSkhpPHgjF8BT3VYr/vyfmquZw3jSRMNboRr4oRzut86ZrSAfpiCgZMT457HrXgdF0gK5CvR6tuwBzz4vSbYqINvRxY7ndcMsYSmpPXshfWS9PDJ6iYYQTFOcOJ/pUopPnqlcSsRezBw+hD/7vxD9SgX/22LU33vg7EQHAxgMgAs8Bu2nJotXtNacTX/q6w7XLzT7eaP5Zwyz96JDJchEvu/6DQbFwfNHVyUkuGALJlE2QqYvhPzKVyuQCrXSU7+pmVeKukm4nth9+riKhxsc2k4TEgJ8exF7D9SV82ok1JNu4RVZ1YN6lE5tQtjmaOJVrTcMjWW5koiE6yqcJuZO9YSMEy4wnygbBZ/Cbd4WE+BHuWeaLLTtmmX5oeqiziwux/ES8zOD3S9O630xQriVfl9nBrnAN2ALX6siAUvZ9+12u2TeL1wzK9+FLO1w4mbPVK5I8wbM8ioAfsUvEHi/xl0X2iLGZel849eiv7uTrerTmppmCOI9okgzyLLgil8ilDek7MgUCRXaX9fm+2bH54EH0Q6lGguUzkqbDsZDaIcobprS+Aw9Qyoss8Qy/DzG839QFgHYLNklFeAqGj4nnIV7BPPP4AOywg1SpijhrxvTGMqf9DZXKK3jPiK3hcqpl605A1AozyshS6I5TCrEYOf78RkvxtMHDARIiKAy1w+PnCM1n2Y8EWGKPBLWZMKLIvlOS6OIvObrEWIhAkzHkY9Mh+vSm2XQ+gBoWebSj9ZoRcnGxWPp8dRa3e33p1/4bF24XskIFVO31gVaBGWpafG6zQKs35Rk/CZLgFYDHV5ygi7yH3T6mE9tYfDYVWRi3DX70etDcCL83YyWIL5oky2RcWA==

Values of Set-level types (natural numbers, booleans) are rather like ur-elements. But it's probably not the answer you were looking for. Do you have something more specific in mind?

On 26 April 2017 at 17:10, Kevin Sullivan <sullivan.kevinj AT gmail.com> wrote:
ZFC set theory can be extended with ur elements -- non-set things, of which nothing can be a member, that are not the same as empty sets.https://en.wikipedia.org/wiki/Urelement. What is the preferred way to represent ur-element-like-things in type theory?



  • Re: [Coq-Club] Modeling Ur Elements, Arnaud Spiwack, 05/03/2017

Archive powered by MHonArc 2.6.18.

Top of Page