coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Indefinite description

From: Nikhil Swamy <nswamy AT microsoft.com>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: [Coq-Club] Indefinite description
Date: Fri, 20 Aug 2021 00:58:52 +0000
Accept-language: en-US
Arc-authentication-results: i=1; mx.microsoft.com 1; spf=pass smtp.mailfrom=microsoft.com; dmarc=pass action=none header.from=microsoft.com; dkim=pass header.d=microsoft.com; arc=none
Arc-message-signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=microsoft.com; s=arcselector9901; h=From:Date:Subject:Message-ID:Content-Type:MIME-Version:X-MS-Exchange-SenderADCheck; bh=tDFcmq0X9j+O1/lge0Mo2UL/YGKUHMb4MtVMeR05akI=; b=heQoW2coRj0jvLTVWnZSmD8VvV+VvODZrzSk7sA7L6c2cstUXYS/FjS6+ddddARysg3NxhkfZ3nxFkre0P49nnY01HAxGbFaP2jYRVRk02tEj4g8OeUtyG9OjXK0NOt0G/lfcwIaXg2YbtnPl7hl4WVERS/uo9m4BoYbNwY4Xj6VgsGKnqnmSJOWdJLNRoAVBAUDu0bM9GJSWPLqoQOz9r1M3lfQIW6EphjxwSQ4dSCQVTnHQutkj4fsUet/MXjsAx1XfmfPtpRjCPUuM5so5c1RUrJdS5sP3QC/MgJ+MHVuL9YPLK93MUB12IeL1ro0+LfQ2jWqE/M4atMcFrdTmw==
Arc-seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=fOnOTpyYYHj0aGosgu8dCoUVmqVojKN9/L7sw6VsgArLqrV/iNrIXT1h1rDEPutr+5o4PfV+oe1TR4H3OBTD9OZONFow9IU6JJYW+Jko3X+FENjdeWPIMBY/xdnZw5TM3+jVzu6meOLzVv7PES+fxXLNwftG4kWQyOPYppUjkZjql1RdgPWb9VtW2LX0grEiNHh2IAwX00f3g1Yxs/kiJ6wZlOHuCAGnNyiVDLkUsTxqTn4qVFWmiR0znsqflBh28/PKNE7w4Ze14NSP4HWgH3j2+UBtWX5FBiSBamQ14+kZXYZAsbmYYfhA90uLgysEl+OdpgXWo6j+ePXv7YbUqA==
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=nswamy AT microsoft.com; spf=Pass smtp.mailfrom=nswamy AT microsoft.com; spf=TempError smtp.helo=postmaster AT outbound.mail.eo.outlook.com
Ironport-hdrordr: A9a23:7YzOFKtCmLpTQpigatbjJ2TB7skC9oMji2hC6mlwRA09TyXGra2TdaUgvyMc1gx7ZJh5o6HnBEDyewKkyXcV2/hbAV7GZmXbUQSTXeVfBOfZogEIeBeOvNK1t50QFJSWYeeYZTcVsS+Q2njaLz9U+qjjzEnev5a9854Cd2FXQpAlyz08JheQE0VwSgUDL4E+DoCg6s1OoCflUWgLb+ygb0N1E9TrlpnurtbLcBQGDxko5E2lljWz8oP3FBCew1M3Ty5P+7E/6mLI+jaJqZlL8svLhCM05VWjr6i+q+GRieerw/b8yPT9Hw+cyzpAor4RHoFq8gpF5N1Ho2xa6OUk6y1QRPibrUmhM11d6CGdpjUJ3FsVmgXf4E7djn35rcPjQjUmT8JHmIJCaxPcr1EtpddmzctwrhWkXrdsfGb9dR7Glqz1vtBR5zuJiGtnlfRWg21UUIMYZrMUpYsD/FlNGJNFGC7h8ogoHORnEcmZvZ9tABqnRmGcunMqzM2nX3w1EBvDSk8eutaN2zwTmHxi1UMXyMEWg39F/pMgTJtP4fjCL81T5cdzZ95Tabg4CPYKQMOxBGCISRXQMHiKKVCiD60DM2Klke+E3Fz03pDYRHUs9up7pH3saiImiYcCQTOfNSTV5uw2zvnkehTCYQjQ
Ironport-phdr: A9a23:F/pARBQDoue8kpfud6j7yn8R1NpsonufAWYlg6HPa5pwe6iut67vIFbYra00ygOTBcOKsrkZ1KL/iOPJYSQ4+5GPsXQPItRndiQuroEopTEmG9OPEkbhLfTnPGQQFcVGU0J5rTngaRAGUMnxaEfPrXKs8DUcBgvwNRZvJuTyB4Xek9m72/q99pHNfwlEnj6wba59IBi2rwjaq9Ubj5ZlJqst0BXCv2FGe/5RxWNmJFKTmwjz68Kt95N98Cpepuws+ddYXar1Y6o3Q7pYDC87M28u/83kqQPDTQqU6XQCVGgdjwdFDBLE7BH+WZfxrzf6u+9g0ySUIcH6UbY5Uimk4qx2ShHnlT0HOiY5/m/Jl8JwkKxVrhG9qBNw2IPbep2ZOOZkc6/BYd8WWGxMVdtRWSxbBYO8apMCAfIAPeZbr4n9pl8OpgajCwiiHuzvzz9JjWLx0K08yOQgHxvJ3AkgHt8VtXTUrcn6NL0VUeCuy6nIwynDY+lK1jf67YjFaxYsquyDUrxsa8Te01UvFx/bgVWKr4zoJzKY2vgDvWSH8+ZtVeKih3InpQ1soTWixMgih43Xi48JxV7I6Ct3zok1KNC6R0B2f92pHIVNui2EOIZ7QMwvTmVutS0nybMGoYa2cScWxJg9wxPSZeaLfoaS7h7+WuudOSl0iXN5dL+xghu+7FSsxfb9W8SxyllGsiRIn9zSunwQyhPe782KRuZj8kqnxD2BzRrc6vteLkAxjafbK4Auwro3lpcLtkTDAzP2l17xjK+LcEUr5/Kk6+H9bbXnop+QLZF7igbkPqQph8y/HeA4Mg8JX2iY4+izyLrj/UjhTLVLiP05jLXZvYjVKMgHvKK0BwFY3pwt5hqlEjur3swUnXwdI1JEfBKHgZLpO1bLIP3gC/e/mFqtny1ux/HGJbDhB5TNIWTZkLfmZrZ97EBcyBYpwd9D4JJUD6kNIOjvVU/pqNzYEhg5PhSozObgEdVxz58RWWaSAqCCK67Sql+J5uc3I+aWfoMVuTD9K+Ik5/H0l3M5l0UdLuGV2s5dY3ehW/9iPk+xYHz2g95HH31A9l41S/Wvg1mfWxZSYWyzVuQy/GdoJpihCNLlR4OtgbjJ5ziyG4weMmZdFVmJAF/tdo6eXOwLZj7UKchkxG9XHYO9QpMsgEn9/DTxzKBqe7K8EsIwsJPozt9u4OPP0xo18G4tZyx8+2aQU2tzg2UEATo/3aQ5rEs7zUqf1a9/gLpTEtkBupuhty8/NJXGyPd9Bcy0UQXELI/hdQ==
Msip_labels: MSIP_Label_f42aa342-8706-4288-bd11-ebb85995028c_Enabled=True;MSIP_Label_f42aa342-8706-4288-bd11-ebb85995028c_SiteId=72f988bf-86f1-41af-91ab-2d7cd011db47;MSIP_Label_f42aa342-8706-4288-bd11-ebb85995028c_SetDate=2021-08-20T00:58:53.004Z;MSIP_Label_f42aa342-8706-4288-bd11-ebb85995028c_Name=General;MSIP_Label_f42aa342-8706-4288-bd11-ebb85995028c_ContentBits=0;MSIP_Label_f42aa342-8706-4288-bd11-ebb85995028c_Method=Standard;

Does anyone know of semantic models of type theory extended with the axiom of indefinite description? Are there such models for extensional type theory (with indefinite description)?

Many thanks in advance,

Nik

[Coq-Club] Indefinite description, Nikhil Swamy, 08/20/2021