From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.25.181.145 with SMTP id g17mr107427lfk.19.1513767656925; Wed, 20 Dec 2017 03:00:56 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.46.109.2 with SMTP id i2ls2746372ljc.14.gmail; Wed, 20 Dec 2017 03:00:55 -0800 (PST) X-Received: by 10.46.88.88 with SMTP id x24mr489885ljd.9.1513767655389; Wed, 20 Dec 2017 03:00:55 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1513767655; cv=none; d=google.com; s=arc-20160816; b=G+k1uWqBFzM06DWbVeS20c8amHETFEhM9D8bgh9yZ4QkvIEw26Rb5S4IiAJHMhMJRz i7sP2MlnEWdfcsWiD3owQlv4tAbddmT4LDy688D2/l+Rgimq1OJKpDtgCEknN9cg5VVn VxcO3RMg2aBBrbRwzKPTYRJVeA+7V1hw3uTgJRnbG6igIzKgcF4TGRARRcvL+h6bE/Wx rovI5oAHdr86jS218cifLzWDteNpZRgLZ6XLW+wVmxcUrVRu2/0Oeza3GJ1x1hkp0k9Z sAsSgGPES1MBykq8ytT32EOYkeZhJOSeadG8YwX4UT9RFAA2sQSuHtNo9W9gg3YXYGMK xang== 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=zRZWbPvwemp2UDHs84FRMOPcxMKKde1xJmKaiukw1bw=; b=x/j9tTzmOPdiYPbkOaInXVilG7/W57MHzlbm3OPxWrFiexEa5VvvH9ykdPp+ZRZNQK fNd1UUS/Y0g9Lt2l/qki7AK3hWLSHj6lFg4SpUDEaHn59+so848i2kHdACjFSbNSnv3U O67J3UKK4hJ50cN23Rn5pZui73ZEeVF8wgNMvi20vdxyuN2fF1hlyNAyMqoXj6J2mspe va+fk4zQm9NoTeuiQgC2gtodW1T8mDJOQAmUY53NUqgAmmRCSN0H3JDSlE2rF7/jpeBa wUFg1ATe/9SfVfSdag2fY0a5L4VErv1OInoNrI9w8uMfn/OT3YREju2H+MbbLFaW/2vx bm2Q== 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 198si1745648ljj.1.2017.12.20.03.00.55 for (version=TLS1 cipher=AES128-SHA bits=128/128); Wed, 20 Dec 2017 03:00:55 -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 vBKB0riG005171; Wed, 20 Dec 2017 12:00:53 +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 vBKB0qRF005868; Wed, 20 Dec 2017 12:00:52 +0100 Received: by fb04209.mathematik.tu-darmstadt.de (Postfix, from userid 11003) id B661A1A52E2; Wed, 20 Dec 2017 12:00:52 +0100 (CET) Date: Wed, 20 Dec 2017 12:00:52 +0100 From: Thomas Streicher To: Thorsten Altenkirch Cc: Andrej Bauer , Homotopy Type Theory Subject: Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent? Message-ID: <20171220110052.GC8054@mathematik.tu-darmstadt.de> References: <20171217102151.GA16619@mathematik.tu-darmstadt.de> <20171218115228.GB29410@mathematik.tu-darmstadt.de> <55AAFF96-F751-4A01-BE3E-280A438A55DC@exmail.nottingham.ac.uk> <20171219153118.GA9218@mathematik.tu-darmstadt.de> <20171219163139.GB13875@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.20.105416 X-PMX-RELAY: outgoing Now at first sight it looks as if doing toposes in a univalent metatheory makes them inconsistent in the sense that all toposes are trivial. But, luckily, that is not the case. If a and a' are in A then (a,refl(a)) and (a',refl(a')) are in Single(a) and Single(a') respectively. These types are certainly isomorphic but not judgementally equal. You can project (a,refl(a)) on a and (a',refl(a')) to a' by applying DIFFERENT first projection functions pi and pi' respectively. But you cannot apply pi' to (a,refl(a)) before having it transformed into an object of Single(a') along an iso between Single(a) and Single(a'). Thorsten has claimed that this were possible in LEAN but it shouldn't! Here is an excerpt from Thorsten's original mail > Hence by extProp > > extProp p : Single(true) = Single(false) > > now we can use transport on (true,refl) : Single(true) to obtain > > x = (extProp p)*(true,refl) : Single(false) > > and we can show that > > second x : first x = false > > but since Lean computationally ignores (extProp p)* we also get > (definitionally): > > first x == true > he clearly says that "since Lean computationally ignores (extProp p)*" but that is balatantly wrong since it mixes judgemental and propositional equality. And there we are back to what I originally said. Of course, {a} and {a'} are isomorphic and thus equal as elements of P(A) if we postulate UA for P(A). Thus we shouldn't! Another gap in Thorsten's argument is the following. Though Single(a) and Single(a') are isomorphic in order to conclude that they are propositionally equal they would have to be elements of a univalent universe BUT I don't see where such a universe should come from in the general topos case! Thomas