From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.28.12.206 with SMTP id 197mr173156wmm.10.1513080156751; Tue, 12 Dec 2017 04:02:36 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.223.156.134 with SMTP id d6ls1363810wre.10.gmail; Tue, 12 Dec 2017 04:02:35 -0800 (PST) X-Received: by 10.223.141.212 with SMTP id o78mr452551wrb.13.1513080155511; Tue, 12 Dec 2017 04:02:35 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1513080155; cv=none; d=google.com; s=arc-20160816; b=hJxnZzOUemINM2hwsuFRzBnf12ZQIOC1WCwD64TjSatI3oEnvgNPNeDxb0LFMLAGrO vPAIHvwE3j6TDQCj2qh4Gl6ipDpfhuOHGs92N2J6pYLz0Ap5OQ1orfjlCL0BjQkeEAUu ULEnVt1Ul0xaY9ftyhxYOU5q8P63zLByH+Tx0VZgdydcOAu2eG1HfOK+o28u8JvXRyW0 nQq20t01WqdivbnpEl3MK2JfzzazNXk+IG3wn2hM/+sUJcVmCpV2tGrBsaSCxEImGzve CsR+bkLGpNLW85x/kiTwYa1LhwrSZ+9oN6JLDUX1RjMy73DDuEJAIlb2UyyOsH92ZnIc bZow== 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=vHz7AbpIuLsI46tnG5qgvb0n77yiqLHPoOnxIeusBv4=; b=jIx88mUtjkhXigHbeH9df44BUIp7/DJIpgsPcLOceeB61i0ZttCOTfrG4sHrVjsUWS EIRk5pl+N+6qEiJUX+F4U88ByZu/rfEnwFA4nrZhUvxYwwxe1yTwlJUmWa18aA/BXT3w 7KfWs821v1LAfc1SH5i71O16jdIyavr6qcwDM3VUqbTh0oe7/V5HJdbuXMPgoRniCRqE Txn4ReXuFiHE5ddRpyXWkquiRQCw19kMPoUDT4cXAgHKltsQAoEqZ+5y2d4y3zVqlvY5 Z3a5pplYi0YdZ4aY8ypcDZdlI6SzMLYPw2FXE/BrExnxsdcXwZaXJuU2Peu8UJS8Rb8G jKgQ== 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 r134si1538084wmd.3.2017.12.12.04.02.35 for (version=TLS1 cipher=AES128-SHA bits=128/128); Tue, 12 Dec 2017 04:02:35 -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 vBCC2Xv5009863; Tue, 12 Dec 2017 13:02:33 +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 vBCC2XRF017442; Tue, 12 Dec 2017 13:02:33 +0100 Received: by fb04209.mathematik.tu-darmstadt.de (Postfix, from userid 11003) id 78D001A0CA8; Tue, 12 Dec 2017 13:02:33 +0100 (CET) Date: Tue, 12 Dec 2017 13:02:33 +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: <20171212120233.GA32661@mathematik.tu-darmstadt.de> References: <4c4fe126-f429-0c82-25e8-80bfb3a0ac78@gmail.com> <11CC10D7-7853-48E7-88BD-42A8EFD47998@exmail.nottingham.ac.uk> MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline In-Reply-To: <11CC10D7-7853-48E7-88BD-42A8EFD47998@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.12.115117 X-PMX-RELAY: outgoing But very topos is a model of extensional type theory when taking Prop = Omega. All elements of Prop are proof irrelevant and equivalent propositions are equal. Since it is a model of extensional TT there is no difference between propsoitional and judgemental equality. Thomas > If you have proof-irrelevance in the strong definitional sense then you cannot be in a topos. This came up recently in the context of Lean which is a type-theory based interactive proof system developed at microsoft and which does implement proof-irrelvance. Note that any topos has extProp: > > Given a:A define Single(a) = Sigma x:A.a=x. We have Single(a) : Prop and > > p : Single(true) <-> Single(false) > > since both are inhabited. 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 > > My conclusion is that strong proof-irrelvance is a bad idea (note that my ???99 paper on Extensionality in Intensional Type Theory used exactly this). It is more important that our core theory is extensional and something pragmatically close to definitional proof-irrelevance can be realised as some tactic based sugar. It has no role in a foundational calculus. > > > Thorsten > > > > > On 12/12/2017, 10:15, "Andrea Vezzosi" wrote: > > >On Mon, Dec 11, 2017 at 3:23 PM, Thorsten Altenkirch > > wrote: > >> Hi Kristina, > >> > >> I guess you are not assuming Prop:Set because that would be System U and hence inconsistent. > >> > >> By proof-irrelevance I assume that you mean that any two inhabitants of a proposition are definitionally equal. This assumption is inconsistent with it being a tops since in any Topos you get propositional extensionality, that is P,Q : Prop, (P <-> Q) <-> (P = Q), which is indeed an instance of univalence. > >> > > > >I don't know if it's relevant to the current discussion, but I thought > >the topos of sets with Prop taken to be the booleans would support > >both proof irrelevance and propositional extensionality, classically > >at least. Is there some extra assumption I am missing here? > > > > > >> It should be possible to use a realizability semantics like omega-sets or Lambda-sets to model the impredicative theory and identify the propositions with PERs that are just subsets. > >> > >> Cheers, > >> Thorsten > >> > >> > >> On 11/12/2017, 04:22, "homotopyt...@googlegroups.com on behalf of Kristina Sojakova" wrote: > >> > >> Dear all, > >> > >> I asked this question last year on the coq-club mailing list but did not > >> receive a conclusive answer so I am trying here now. Is the theory with > >> a proof-relevant impredicative universe Set, proof-irrelevant > >> impredicative universe Prop, and function extensionality (known to be) > >> consistent? It is known that the proof-irrelevance of Prop makes the Id > >> type behave differently usual and in particular, makes the theory > >> incompatible with univalence, so it is not just a matter of tacking on > >> an interpretation for Prop. > >> > >> Thanks in advance for any insight, > >> > >> Kristina > >> > >> > >> > >> > >> > >> > >> > >> This message and any attachment are intended solely for the addressee > >> and may contain confidential information. If you have received this > >> message in error, please send it back to me, and immediately delete it. > >> > >> Please do not use, copy or disclose the information contained in this > >> message or in any attachment. Any views or opinions expressed by the > >> author of this email do not necessarily reflect the views of the > >> University of Nottingham. > >> > >> This message has been checked for viruses but the contents of an > >> attachment may still contain software viruses which could damage your > >> computer system, you are advised to perform your own checks. Email > >> communications with the University of Nottingham may be monitored as > >> permitted by UK legislation. > >> > > > > > This message and any attachment are intended solely for the addressee > and may contain confidential information. If you have received this > message in error, please send it back to me, and immediately delete it. > > Please do not use, copy or disclose the information contained in this > message or in any attachment. Any views or opinions expressed by the > author of this email do not necessarily reflect the views of the > University of Nottingham. > > This message has been checked for viruses but the contents of an > attachment may still contain software viruses which could damage your > computer system, you are advised to perform your own checks. Email > communications with the University of Nottingham may be monitored as > permitted by UK legislation. >