From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.46.22.20 with SMTP id w20mr54940ljd.38.1513002500743; Mon, 11 Dec 2017 06:28:20 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.46.101.66 with SMTP id z63ls1006991ljb.7.gmail; Mon, 11 Dec 2017 06:28:19 -0800 (PST) X-Received: by 10.46.42.6 with SMTP id q6mr54237ljq.21.1513002499271; Mon, 11 Dec 2017 06:28:19 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1513002499; cv=none; d=google.com; s=arc-20160816; b=S1PvcvuISB9gAI/Pr1jxFFz7ioi8N8usNh/rcqdIGpGGMtm93l/QDM8kTaLGAg/ALJ CwNIYQmWuQ7dLklS/Ti4xqPF5r5eZlLFK7cyRWJ2sL6jAGqvkmiUktZRpNrN/X/9X+yj eZvpDRGmclIUOQxnbSJlS2x2gOsVlBapMn7exPOhTeqelFehxPQVRAV48ZVzdE99/ucF 72BN3wbiACUSJQygcKg7iMB+PMtBQ8AGqlZ9cjOTl/w/dOGxJE5euFiM/Ll3eKvR3hmy Y+baMOFa1d1QfFhFJXwA2Xj3Yw9oqNeX+B7WioppVNVaqYWFB2CE/TPU7hY9eeB8rCL/ MX2g== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=user-agent:in-reply-to:content-disposition:mime-version:references :message-id:subject:cc:to:from:date:arc-authentication-results; bh=9O69Dv/XUbVVb/+w96tdtyrg+lWqArbSVe6iwXKY+zo=; b=qajzpk2rb50OIOrmbxWQsdXsVhM4F1pdJFsFtUd5dGH6vOuK3TGJKxaDfeS6mE2IXk jIrf+U30jMsjX9knaOVe6VIW28ZMqzLq23rEK4+uAhW4c2UzV7dJmHH/29RWXVOWRpQ5 7uT3oxBpC4bRhySnYgHcafNy7pzxiwbztdRjGUEGqHzHREgyAjzD9Hf94SVPMdyuFRH7 dxaRZ9P2YYw7ZMefuyAgi0TCKpZ2MNGMojARqRnTiqziMpxcAnVAx2Q/+kCGD3finfoY xfviQrnTN8aUDjcXPaP4YHnJgy4SvkQfPIZw3X1HuWIGDWN9q8NJ9yIJiuLRrQ2wrCLL vbYg== ARC-Authentication-Results: i=1; gmr-mx.google.com; spf=pass (google.com: best guess record for domain of stre...@mathematik.tu-darmstadt.de designates 130.83.156.239 as permitted sender) smtp.mailfrom=stre...@mathematik.tu-darmstadt.de Return-Path: Received: from lnx503.hrz.tu-darmstadt.de (mail-relay15.hrz.tu-darmstadt.de. [130.83.156.239]) by gmr-mx.google.com with ESMTPS id q77si1392872lfi.1.2017.12.11.06.28.18 for (version=TLS1 cipher=AES128-SHA bits=128/128); Mon, 11 Dec 2017 06:28:19 -0800 (PST) Received-SPF: pass (google.com: best guess record for domain of stre...@mathematik.tu-darmstadt.de designates 130.83.156.239 as permitted sender) client-ip=130.83.156.239; Authentication-Results: gmr-mx.google.com; spf=pass (google.com: best guess record for domain of stre...@mathematik.tu-darmstadt.de designates 130.83.156.239 as permitted sender) smtp.mailfrom=stre...@mathematik.tu-darmstadt.de Received: from fb04281.mathematik.tu-darmstadt.de (fb04281.mathematik.tu-darmstadt.de [130.83.2.21]) by lnx503.hrz.tu-darmstadt.de (8.14.4/8.14.4/HRZ/PMX) with ESMTP id vBBESHkv002587; Mon, 11 Dec 2017 15:28:17 +0100 (envelope-from stre...@mathematik.tu-darmstadt.de) Received: from fb04209.mathematik.tu-darmstadt.de (fb04209.mathematik.tu-darmstadt.de [130.83.2.209]) by fb04281.mathematik.tu-darmstadt.de (8.12.3/8.12.3/Debian-7.2) with ESMTP id vBBESHRF002346; Mon, 11 Dec 2017 15:28:17 +0100 Received: by fb04209.mathematik.tu-darmstadt.de (Postfix, from userid 11003) id E97751A0D47; Mon, 11 Dec 2017 15:28:16 +0100 (CET) Date: Mon, 11 Dec 2017 15:28:16 +0100 From: Thomas Streicher To: Jon Sterling Cc: HomotopyT...@googlegroups.com Subject: Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent? Message-ID: <20171211142816.GA24950@mathematik.tu-darmstadt.de> References: <4c4fe126-f429-0c82-25e8-80bfb3a0ac78@gmail.com> <1512992534.265543.1200966552.20A0FEC1@webmail.messagingengine.com> <1512996187.281015.1201017552.7F33C02E@webmail.messagingengine.com> MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline In-Reply-To: <1512996187.281015.1201017552.7F33C02E@webmail.messagingengine.com> User-Agent: Mutt/1.5.23 (2014-03-12) X-PMX-TU: seen v1.2 by 5.6.1.2065439, Antispam-Engine: 2.7.2.376379, Antispam-Data: 2017.12.11.141516 X-PMX-RELAY: outgoing It's amazing how common knoledge from late 80s can disappeear easily. For interpreting Coq one uses Asm(A), assemblies over a pca A, Set is interpreted as modest sets and Prop as subterminal modest sets. It's important to take Asm(A) instead of the realizability topos for showing that Set is internally complete in a sufficiently strong sense. (See Ed Robinson's old LICS paper "How Complete is PER?"). Of course, these models don't validate UA but they were not meant to be. Id takes values in Prop and is isomorphic to Leibniz equality. See work from the 80s by Martin Hyland, myself and a few others. Thomas