From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.25.163.6 with SMTP id m6mr646183lfe.2.1513357231394; Fri, 15 Dec 2017 09:00:31 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.46.29.73 with SMTP id d70ls1195051ljd.4.gmail; Fri, 15 Dec 2017 09:00:29 -0800 (PST) X-Received: by 10.25.18.27 with SMTP id h27mr678417lfi.4.1513357229212; Fri, 15 Dec 2017 09:00:29 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1513357229; cv=none; d=google.com; s=arc-20160816; b=Nqq5zLSfT+J+umCwoOS5x/iWlQJjTzZ1VdrEXMUcjcu7ipNq8m3vvVsLU7+U2es0ld KzcncvCH8yxwDpZlvNK8HXjdxdHAEO7q/X/3a+jDFJs5BouMTntuGf5LfqDxJ0GJj4ak 6/5VXzt8hHCrON3UexfFuFQtysvQbQ/i8Lu8r7jTFsaMvQdoReC3qJBHwQCRt/2+FMOg esLum7viRS2Ko1GoMOVU5VODAwKqkhUsCWUKW+xfrNL9j6iFKr5NF5v0XAgOJ4SlWn7Y NtxlkOoYfoXx3UvRCornYnqpHeY2gkcXJR6kz0hYMb0zc4Mw7MGHNsSJVUs94O3kjqDO I3xw== 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=IvkGyVbW/9yqKDPzSwDGKQf5wMG44ipcS6TGD6LFZUM=; b=TCIXAp2UouCDt0jZSot6zbbsoRefEW3CKQAZz7B/m8QsU3JFqpzqdTF1JonodlgN5X d02dJjNCAuQ4MgZoztLHldn6YYjrISg9+B8lllrcyq7TDH/3rKnpdFmcKPm0+bzFcKy5 wcFX4s5/DbsIioFVVe0YAP7UzKdG7j1jg/AKl1Tpe5kwFAWsbzDG69JGpphT+qNmhAo0 Q9hhxvpbaAeTQLN2yiByxvJxLCNFSQKyqaTWluFEKe4jgxI3lRlGch/1jBoac1swM6tr ekF5RE/p52DxdbR4HgAnFwuYArj9+Tb3YLZidtSpUCUeoBe+I9NgN7+z++oEGpgaEwl0 ymwg== 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.225 as permitted sender) smtp.mailfrom=stre...@mathematik.tu-darmstadt.de Return-Path: Received: from lnx500.hrz.tu-darmstadt.de (mailout.hrz.tu-darmstadt.de. [130.83.156.225]) by gmr-mx.google.com with ESMTPS id g77si564838lfl.5.2017.12.15.09.00.28 for (version=TLS1 cipher=AES128-SHA bits=128/128); Fri, 15 Dec 2017 09:00:29 -0800 (PST) Received-SPF: pass (google.com: best guess record for domain of stre...@mathematik.tu-darmstadt.de designates 130.83.156.225 as permitted sender) client-ip=130.83.156.225; 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.225 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 lnx500.hrz.tu-darmstadt.de (8.14.4/8.14.4/HRZ/PMX) with ESMTP id vBFGtHh6007532; Fri, 15 Dec 2017 17:55:20 +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 vBFH0BRF005245; Fri, 15 Dec 2017 18:00:12 +0100 Received: by fb04209.mathematik.tu-darmstadt.de (Postfix, from userid 11003) id E18A51A3D47; Fri, 15 Dec 2017 18:00:11 +0100 (CET) Date: Fri, 15 Dec 2017 18:00:11 +0100 From: Thomas Streicher To: Thorsten Altenkirch Cc: Andrea Vezzosi , Kristina Sojakova , Homotopy Type Theory Subject: Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent? Message-ID: <20171215170011.GA22027@mathematik.tu-darmstadt.de> References: <4c4fe126-f429-0c82-25e8-80bfb3a0ac78@gmail.com> <11CC10D7-7853-48E7-88BD-42A8EFD47998@exmail.nottingham.ac.uk> <20171212120233.GA32661@mathematik.tu-darmstadt.de> <643DFB5A-10F8-467F-AC3A-46D4BC938E85@exmail.nottingham.ac.uk> MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline In-Reply-To: <643DFB5A-10F8-467F-AC3A-46D4BC938E85@exmail.nottingham.ac.uk> 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.15.162116 X-PMX-RELAY: outgoing Hi Thorsten, my analysis of your proof of true = false in Lean is as follows. I don't see that (\Sigma x:A) a = x is an element of Prop though it certainly is isomorphic to an element in Prop, namely true. But leaving this aside I analyse the situation as follows. Your argument essentially is as follows. Since Single(true) and Single(false) are isomorphic they are equal (essentially by UA applied to subsingletons). Now you have c in Single(true) and d in Single(false) whose first projections are true and false respectively. >From this you conclude that that true and false are equal since c and d are equal. But they aren't since they belong to different types. This style of argument allows you prove that all types are propositions as follows. Suppose a and a' are elements of A. Then Single(a) and Single(a') are equivalent propositions and thus equal. Then also their first projections are equal and thus a = a'. I fully agree with Mike's analysis that projections have to be typed. But, moreover, we must not neglect equality proofs when replacing equals by equals. Moreover, toposes will not validate univalence. As pointed out to me by Martin Escardo you can't even formulate it because in arbitrary toposes you don't have universe (not to speak of univalent ones). Thomas PS Your observation doesn't really increase my believe in the gain of certainty when formalizing proofs :-)