coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Modeling Ur Elements

From: Kevin Sullivan <sullivan.kevinj AT gmail.com>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: [Coq-Club] Modeling Ur Elements
Date: Wed, 26 Apr 2017 11:10:35 -0400
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=sullivan.kevinj AT gmail.com; spf=Pass smtp.mailfrom=sullivan.kevinj AT gmail.com; spf=None smtp.helo=postmaster AT mail-oi0-f44.google.com
Ironport-phdr: 9a23:eqXvzx170piQ1ITgsmDT+DRfVm0co7zxezQtwd8Zse0eLvad9pjvdHbS+e9qxAeQG96Kt7Qc06L/iOPJYSQ4+5GPsXQPItRndiQuroEopTEmG9OPEkbhLfTnPGQQFcVGU0J5rTngaRAGUMnxaEfPrXKs8DUcBgvwNRZvJuTyB4Xek9m72/q89pDXbAhEniaxba9vJxiqsAvdsdUbj5F/Iagr0BvJpXVIe+VSxWx2IF+Yggjx6MSt8pN96ipco/0u+dJOXqX8ZKQ4UKdXDC86PGAv5c3krgfMQA2S7XYBSGoWkx5IAw/Y7BHmW5r6ryX3uvZh1CScIMb7S60/Vza/4KdxUBLmiCkJOT0k/m/JlsN9l7hUrA67qhFl34LYfIOYOfxjda3dZ9MaQm9BU95UWSNfHIO8bo0PBPccM+ZFq4n9o1oOrQWkCgmqGejizSRIhmLy3a0+0uQhDxvJ3Ao6E9INrnvUstT1NKEQUe2uw6nIyC/Mb/JS2Tvn9IfIdRUhrOiKULltf8TRzkwvGBnEjlWWsYHkMTKV1ucMs2iD8eVvSOOvhHQ9pwF2uDivycEhgZTKiIIN0l3I6zl1zYIvKdC7SEN3e8CoHIZTui2AOIZ7TcUvSHxytikg0L0Jo5u7cTAKyJs5wx7fbOSKc42S7RLiUOadODB4hHN5dL6miRa//ketxvfzVsmz11ZKoS5FncfWun8R0BzT79CLSvp7/ki/xTaCzx7f5v1ALEwulqfWK4QtzqAtmpcQq0jOESD7lF3zjKCMd0Uk/uao6/7gYrXjvpKcLJJ0igX6MqQvhMywG+I4PhINX2eF5+S81bvj/U/iTbVFi/05iKjZsJTAKcsHoa65BhdZ0pw/5BanEzemzNMYkGEbI1JCYRKLlpTmO1XTIP/jFvq/mFStkDJzx//cJLHhA5PNLmLCkLj7Z7p95VRcm0IPyoUV7JVNT7oFPfjbW0nrtdWeAAVze1i/xP+iA9Fg3KsfX3iOC+mXKvWBn0WP47cMLveNYscupTL5KuYs4ba6lmI9nV4DdK/v3pYJaXa6NvtjKkSdJ3Hrh4FSQi8xogMiQbmy2xW5WjlJaiPqUg==

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?

[Coq-Club] Modeling Ur Elements, Kevin Sullivan, 04/26/2017