From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.200.3.79 with SMTP id w15mr15237822qtg.10.1513515335859; Sun, 17 Dec 2017 04:55:35 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.200.3.34 with SMTP id q34ls6522259qtg.10.gmail; Sun, 17 Dec 2017 04:55:34 -0800 (PST) X-Received: by 10.200.15.57 with SMTP id e54mr14489343qtk.61.1513515334843; Sun, 17 Dec 2017 04:55:34 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1513515334; cv=none; d=google.com; s=arc-20160816; b=Aqy6KemNbR6pxBH32evysQ366vs7QlvhnbOD7eg/phvX+di8ruAtM41WSM0HRerQla lgIdsPtn4gHUeGE7NsYbkOkGKFeMw0IvWJfuKc8wcB8er2LT0zyuwm1w164ROZWzzieT f1drxbOc1cya51DX962hxKH2JyusWY4E8W3pwAFT4xM01aKUoG+Sv3yXtVtwt5hgHqVq GWUPmZoyuUjebBtBq8uAMEJrCbpb0VAHyXotWdB0GJO51PY9gjFxQ+wUHo53S08/RZMr vaj3VqKNq/iweCP4rCqWJIfKNOsKZS5LQJQD6lNMl/b+GAF7v34CXywVXALjXUiRxRYK F6sQ== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-transfer-encoding:cc:to:subject:message-id:date:from :references:in-reply-to:mime-version:dkim-signature :arc-authentication-results; bh=IkbNpa8mxBucxUKRUtKZlc3aTu2N50vWShz5naX+g08=; b=v808Gn97D8AwL5qte0qZOL/YnR3vyddFJZRslcckr5yATBNS4zqyfJAYYooj6fl4/c fLRvPaHDAAjFc5PPHcEgNBk4cKe+TyUX2jFIAYiBiVYpnpn1Z4By6wgPejK3x6LmTj5q 8hTPelY3Xz7lx3xWzQxjULu/Kt29Kc69IBQxaQBeSmPvyzY1OYFAwK3fR/5AKH7nKuxQ uZyB3I/0nE49mKuACCY97VgZg5WbPDqAY14eBUwZfqXGwCE5NLD1+5Wh6D/h5jP4Hmr3 ZFKr/ELbj8QVySk6BdHbVHl5ccuO4dQGigOa9W/2KSi8Vh2bmGrsfRV75wjUODvB2C8p EX6A== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=Uvfe75HV; spf=neutral (google.com: 2607:f8b0:4003:c0f::235 is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Return-Path: Received: from mail-ot0-x235.google.com (mail-ot0-x235.google.com. [2607:f8b0:4003:c0f::235]) by gmr-mx.google.com with ESMTPS id c13si568966qth.1.2017.12.17.04.55.34 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Sun, 17 Dec 2017 04:55:34 -0800 (PST) Received-SPF: neutral (google.com: 2607:f8b0:4003:c0f::235 is neither permitted nor denied by domain of shu...@sandiego.edu) client-ip=2607:f8b0:4003:c0f::235; Authentication-Results: gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=Uvfe75HV; spf=neutral (google.com: 2607:f8b0:4003:c0f::235 is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Received: by mail-ot0-x235.google.com with SMTP id q3so11335402oth.2 for ; Sun, 17 Dec 2017 04:55:34 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=sandiego-edu.20150623.gappssmtp.com; s=20150623; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc:content-transfer-encoding; bh=IkbNpa8mxBucxUKRUtKZlc3aTu2N50vWShz5naX+g08=; b=Uvfe75HViR8el/QLGDCnZVf3xVBU2wGh0ceZ5SoL4FQRcPMpzT9YfNrZBCVmUJSVc6 YN6ecuQHY9+jR8vaWsSMqdiMRiOwPG1eqdUWi/NbZYfoBV02aKI1nTALvCsAXjeCblbf aMvJu2MuIgol+Qs4fGmx+EHXrEGe3vbwLwzxXkGpRYOoec0F8XI1p5kTJ7SPVxxTWipv H10WBHBXw7f+Bt6FLLFUV5F6ZspuSzWzaVC7UjaZ8DlK89l2SpIHdzeXeSiI0uwREg4E kE+1eZZ+NAC7/eIaM0NLr307zvoN4xrtmspT8N7ZCC0COi/c+Tkx4/1/bq3qrYzPmuh+ NXtw== X-Gm-Message-State: AKGB3mJh5Gx52mjHUjWc4vjt3/fOEJ31eAIEEXr3Y+vfVAML/Bxe/xnv 87ZqI2OUMbYFsRhsYZLJR9KT5SP8LPg= X-Received: by 10.157.26.35 with SMTP id a32mr13069287ote.210.1513515333737; Sun, 17 Dec 2017 04:55:33 -0800 (PST) Return-Path: Received: from mail-ot0-f170.google.com (mail-ot0-f170.google.com. [74.125.82.170]) by smtp.gmail.com with ESMTPSA id c34sm5158375otd.13.2017.12.17.04.55.33 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Sun, 17 Dec 2017 04:55:33 -0800 (PST) Received: by mail-ot0-f170.google.com with SMTP id v40so679315ote.13 for ; Sun, 17 Dec 2017 04:55:33 -0800 (PST) X-Received: by 10.157.31.61 with SMTP id x58mr13421341otd.320.1513515332830; Sun, 17 Dec 2017 04:55:32 -0800 (PST) MIME-Version: 1.0 Received: by 10.157.89.169 with HTTP; Sun, 17 Dec 2017 04:55:12 -0800 (PST) In-Reply-To: <40D87932-BBF0-4CCF-A8D1-32E7A7BBFE5C@exmail.nottingham.ac.uk> 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> <40D87932-BBF0-4CCF-A8D1-32E7A7BBFE5C@exmail.nottingham.ac.uk> From: Michael Shulman Date: Sun, 17 Dec 2017 04:55:12 -0800 X-Gmail-Original-Message-ID: Message-ID: Subject: Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent? To: Thorsten Altenkirch Cc: Homotopy Type Theory Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable On Sat, Dec 16, 2017 at 7:21 AM, Thorsten Altenkirch wrote: > Not really: you can prove =C2=B3PropExt -> False=C2=B2 in the current sys= tem and you > shouldn=C2=B9t be able to do this. Ah, I see. I didn't realize that PropExt was something you could hypothesize inside of Lean; I thought you were proposing it as a modification to the underlying type theory. In that case, yes, I agree, the implementation is incorrect. (Are any Lean developers listening?) > By definitional proof-irrelevance I mean that we have a =C2=B3static=C2= =B2 universe > of propositions and the principle that any tow proofs of propositions are > definitionally equal. That is what I suggested in my LICS 99 paper. > However, it seems (following your comments) that we can=C2=B9t prove =C2= =B3PropExt > -> False=C2=B2 in this system. > > One could argue that Lean=C2=B9s type theory is defined by its implementa= tion > but then it may be hard to say anything about it, including wether it is > consistent. > > > I still wonder what exactly is the difference between a static > )(efnitionally proof-irrelvant) Prop which seems to correspond to Omega i= n > a topos and set-level HoTT (i.e. using HProp). Hprop is also a subobject > classifier (with some predicativity proviso) but the HoTT view gives you > some extra power. > > A prime example of that "extra power" is that with HProp you can prov= e > function comprehension (unique choice). This goes along with a > reduction in the class of models: I believe that a static Prop can > also be modeled by the strong-subobject classifier in a quasitopos, i= n > which case unique choice is false. > > Ok, so you are saying that a static Prop only gives rise to a quasitopos > which fits with the observation that we don't get unique choice in this > case. On the other hand set level HoTT gives rise to a topos? > > Thorsten > > > Ok, once we also allow QITs we know that this goes beyond the usual > topos logic (cf. the example in your paper with Peter). > > > > Thorsten > > > > > > On 12/12/2017, 23:14, "homotopyt...@googlegroups.com on behalf > of Michael Shulman" shu...@sandiego.edu> wrote: > > > > This is really interesting. It's true that all toposes satisfy > both > > unique choice and proof irrelevance. I agree that one > interpretation > > is that definitional proof-irrelevance is incompatible with the > > HoTT-style *definition* of propositions as (-1)-truncated types= , > so > > that you can *prove* something is a proposition, rather than > having > > "being a proposition" being only a judgment. But could we > instead > > blame it on the unjustified omission of type annotations? > Morally, a > > pairing constructor > > > > (-,-) : (a:A) -> B(a) -> Sum(x:A) B(x) > > > > ought really to be annotated with the types it acts on: > > > > (-,-)^{(a:A). B(a)} : (a:A) -> B(a) -> Sum(x:A) B(x) > > > > and likewise the projection > > > > first : (Sum(x:A) B(x)) -> A > > > > should really be > > > > first^{(a:A). B(a)} : (Sum(x:A) B(x)) -> A. > > > > If we put these annotations in, then your "x" is > > > > (true,refl)^{(b:Bool). true=3Db} > > > > and your two apparently contradictory terms are > > > > first^{(b:Bool). true=3Db} x =3D=3D true > > > > and > > > > second^{(b:Bool). false=3Db} x : first^{(b:Bool). false=3Db} x = =3D > false > > > > And we don't have "first^{(b:Bool). false=3Db} x =3D=3D true", = because > > beta-reduction requires the type annotations on the projection > and the > > pairing to match. So it's not really the same "first x" that's > equal > > to true as the one that's equal to false. > > > > In many type theories, we can omit these annotations on pairing > and > > projection constructors because they are uniquely inferrable. > But if > > we end up in a type theory where they are not uniquely > inferrable, we > > are no longer justified in omitting them. > > > > > > On Tue, Dec 12, 2017 at 4:21 AM, Thorsten Altenkirch > > wrote: > > > Good point. > > > > > > OK, in a topos you have a static universe of propositions. > That is wether something is a proposition doesn=C2=B9t depend on other > assumptions you make. > > > > > > In set-level HoTT we define Prop as the types which have at > most one inhabitant. Now wether a type is a proposition may depend on > other assumptions. (-1)-univalence i.e. propositional extensionality turn= s > Prop into a subobject classifier (if you have resizing otherwise you get > some sort of predicative topos). > > > > > > However, the dynamic interpretation of propositions gives you > some additional power, in particular you can proof unique choice, because > if you can prove Ex! x:A.P x , where Ex! x:A.P x is defined as Sigma x:A.= P > x /\ Pi y:A.P y -> x=3Dy then this is a proposition even though A may not > be. However using projections you also get Sigma x:A.P x. > > > > > > Hence I guess I should have said a topos with unique choice (= I > am not sure wether this is enough). Btw, set-level HoTT also gives you > QITs which eliminate many uses of choice (e.g. the definition of the > Cauchy Reals and the partiality monad). > > > > > > Thorsten > > > > > > > > > > > > > > > > > > > > > On 12/12/2017, 12:02, "Thomas Streicher" > wrote: > > > > > >>But very topos is a model of extensional type theory when > taking Prop > > >>=3D 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 a= t > microsoft and which does implement proof-irrelvance. Note that any topos > has extProp: > > >>> > > >>> Given a:A define Single(a) =3D Sigma x:A.a=3Dx. We have > Single(a) : Prop and > > >>> > > >>> p : Single(true) <-> Single(false) > > >>> > > >>> since both are inhabited. Hence by extProp > > >>> > > >>> extProp p : Single(true) =3D Single(false) > > >>> > > >>> now we can use transport on (true,refl) : Single(true) to > obtain > > >>> > > >>> x =3D (extProp p)*(true,refl) : Single(false) > > >>> > > >>> and we can show that > > >>> > > >>> second x : first x =3D false > > >>> > > >>> but since Lean computationally ignores (extProp p)* we also > get (definitionally): > > >>> > > >>> first x =3D=3D 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 propositiona= l > extensionality, that is P,Q : Prop, (P <-> Q) <-> (P =3D Q), which is ind= eed > 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" > sojakova...@gmail.com> 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 o= f > 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 view= s > of the > > >>> >> University of Nottingham. > > >>> >> > > >>> >> This message has been checked for viruses but the > contents of an > > >>> >> attachment may still contain software viruses which coul= d > 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 immediatel= y > 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 o= f > 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 receive= d > 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 expresse= d > 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. > > > > > > -- > > > You received this message because you are subscribed to the > Google Groups "Homotopy Type Theory" group. > > > To unsubscribe from this group and stop receiving emails from > it, send an email to HomotopyTypeThe...@googlegroups.com. > > > For more options, visit https://groups.google.com/d/optout. > > > > -- > > You received this message because you are subscribed to the > Google Groups "Homotopy Type Theory" group. > > To unsubscribe from this group and stop receiving emails from > it, send an email to HomotopyTypeThe...@googlegroups.com. > > For more options, visit https://groups.google.com/d/optout. > > > > > > > > > > > > > > This message and any attachment are intended solely for the address= ee > > 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 th= is > > message or in any attachment. Any views or opinions expressed by t= he > > 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 yo= ur > > computer system, you are advised to perform your own checks. Email > > communications with the University of Nottingham may be monitored a= s > > permitted by UK legislation. > > > > -- > > You received this message because you are subscribed to the Google > Groups "Homotopy Type Theory" group. > > To unsubscribe from this group and stop receiving emails from it, > send an email to HomotopyTypeThe...@googlegroups.com. > > For more options, visit https://groups.google.com/d/optout. > > > > > > > > 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. > > -- > You received this message because you are subscribed to the Google Groups= "Homotopy Type Theory" group. > To unsubscribe from this group and stop receiving emails from it, send an= email to HomotopyTypeThe...@googlegroups.com. > For more options, visit https://groups.google.com/d/optout.