From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.223.142.214 with SMTP id q80mr1692wrb.22.1513607259142; Mon, 18 Dec 2017 06:27:39 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.28.213.140 with SMTP id m134ls2971278wmg.2.gmail; Mon, 18 Dec 2017 06:27:38 -0800 (PST) X-Received: by 10.28.63.83 with SMTP id m80mr1410wma.10.1513607258014; Mon, 18 Dec 2017 06:27:38 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1513607257; cv=none; d=google.com; s=arc-20160816; b=CTVXtfoyOXybzuK8a14CvAALgr+RNAyJu2xJNgxl2FC2SdZ7HHIZTfMq3uMGLwWZBW VdFKQpGHlBImVmJC/PNi5sn3+n75i13ER1GmkvH3sBOxNB283RuGwANE7qB47TIzEe/j CBNy3L5EmOaAER53tGkHEJgPKKFs9spIs1P1lRgt+el+jF75Uvc6UHpCWt57dGbAksb9 PA3biNYdlCWfmVoc09qSUAGIlyeBEheZTlkRKbhZA6i/XwPsFG0D4vwuCWa50E84OOWO tHhKKUAn0hgIyyzFZnIfUY2vijH7ttBNRTSIyHBIFFAxO7F4q+kiUJT30xg6C+98lytg Zu/A== 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=8iDFpearnRX1kLVEgVoJzr0rgbZ5rvD6A9X//P9uzgA=; b=bRR2xPNb3ohJj8gwGlc6hfy8gX7ddQabjjPPFpvGfeJ2ryE/axHJ9VX6N0BYRTZ4Dn Go25a9y4Vv6ubvAJTmh/yVJLHQfSsILpJdAjzL7aQ5hbvfkVSJeM7xpP+5p3FP5Y2f3D Yi6Lb6meZo+MgNowNbROQq6Ejo1U+T6dmLc0KBG4AAsd9bSssf0TUmB8tU+dHFZmmIHJ wYSOo5Lns+lKiCe0tHuxqxsEaLQsOqgVdsi++KZBEEKoaElGXQYEzcQKTLoDNOqprsQ1 cen9DZ3tYJaBwmKTpZcHvJ/ZIaulnriU4FYLBPh7l1Lb+jrLsVm/Lc4NKHuMg9V1cu3V YJzw== 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 a14si1267475wmg.0.2017.12.18.06.27.37 for (version=TLS1 cipher=AES128-SHA bits=128/128); Mon, 18 Dec 2017 06:27:37 -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 vBIEKHYC006100; Mon, 18 Dec 2017 15:22:37 +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 vBIBqSRF004048; Mon, 18 Dec 2017 12:52:28 +0100 Received: by fb04209.mathematik.tu-darmstadt.de (Postfix, from userid 11003) id 9542C1A3B40; Mon, 18 Dec 2017 12:52:28 +0100 (CET) Date: Mon, 18 Dec 2017 12:52:28 +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: <20171218115228.GB29410@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> <20171215170011.GA22027@mathematik.tu-darmstadt.de> <20171217102151.GA16619@mathematik.tu-darmstadt.de> MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline In-Reply-To: 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.18.142116 X-PMX-RELAY: outgoing > >The inconsistency proof you have given is a slightly distorted version > >of the following ridiculous argument: {a} and {b} are isomorphic thus > >equal for which reason a = b. > > Indeed, but we are not in set theory. In set level HoTT Single(True) = > Single(False) but True != False. This is not a question of set theory. In a topos we have propositional extensionality in the sense that \forall p,q:Omega. (p <-> q) -> p = q but what we don't have is that Single(a) \in \Omega for a \in A. Thomas