From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.98.192.19 with SMTP id x19mr3082124pff.31.1513277557097; Thu, 14 Dec 2017 10:52:37 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.84.235.2 with SMTP id o2ls1364771plk.15.gmail; Thu, 14 Dec 2017 10:52:35 -0800 (PST) X-Received: by 10.84.128.193 with SMTP id a59mr3170021pla.22.1513277555923; Thu, 14 Dec 2017 10:52:35 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1513277555; cv=none; d=google.com; s=arc-20160816; b=ka3zm3Q3WOW9SGRKWAKf+Tz/CZaSf5lTT4WD5tUYyuIPWvRL6u7qiEkHaO4mUtD0nZ QZx3gsgPT6ND09OYgqy43xcX+yJ/c2dkWfFItfi375ePxZ1TBbfb0xTZYThLMlDEURPs GuhQaeusRR5QMK7RC0HAr9BG6fQxDe3gTEy2G5Vjfv0zKpzIR5BOjaWFndvloV50vl3b Y+Ztrwnay6XgVD8fkY0M9o6JxevNS/nlr3LGd8tNmnetpQyiVF6vF2932WKtl7AGwbwq I4/r8smN2O74HMc7XiB/qlpXNg9uLzQT1NVa9HBtBUEGMmasQ4kXoRNstzOfRdDfvwuL vxWA== 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=E1lZQeFhcTzzcnFDagIipIw4HjUG/UFySWqkSvwidy4=; b=SvPjiPonYhYkZ2+IGHz+iBYs3+DsHCnXy7UtDLcroPQ2QkB/Nfp9DZtU7HxTGOCA12 c2WKjYAGPDYMyVz4L3o/xUItAkIEG6IH9rSkwRLJm74G8IA7o/dZQ+Kffqd8Y3hd0soD sKyTC8QpTo5vRfoOCNhxDlMCpKPnUgnRLhRsUBg+BaxIC9n8anSJyHfvYc1b/DKdiG4S Sxqn+pu28JSmRRE7r5DbifnmH7wmdzbh7kas/B1DMqecm7/QDbl1Dq5oJm4sEe1Jjhh5 W1/RCHTkWkX6lKKhTCoT5C4/Xpeox/XYmUxOQLIkzCAAo73MAFFoM5egL5BJmx638GUh qOmg== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=Z+/R9QBI; spf=neutral (google.com: 2607:f8b0:4003:c06::233 is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Return-Path: Received: from mail-oi0-x233.google.com (mail-oi0-x233.google.com. [2607:f8b0:4003:c06::233]) by gmr-mx.google.com with ESMTPS id b73si161645pga.4.2017.12.14.10.52.35 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 14 Dec 2017 10:52:35 -0800 (PST) Received-SPF: neutral (google.com: 2607:f8b0:4003:c06::233 is neither permitted nor denied by domain of shu...@sandiego.edu) client-ip=2607:f8b0:4003:c06::233; Authentication-Results: gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=Z+/R9QBI; spf=neutral (google.com: 2607:f8b0:4003:c06::233 is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Received: by mail-oi0-x233.google.com with SMTP id x20so4565570oix.12 for ; Thu, 14 Dec 2017 10:52:35 -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=E1lZQeFhcTzzcnFDagIipIw4HjUG/UFySWqkSvwidy4=; b=Z+/R9QBInx3MuZHxQxhR1b28feh00hxOpbqOfStRcPTEe91C6HjEYDybj9o2pNV0Su exLE1FELrUIhVJwLZoInDEQjxzKZVlAIi7gq6lH2nqsZQN+E0SPSJiGQGD7rflQLM/nS C8ku5ytZ369sRtkjHemopUmeVVeHgaRZuEM3uxVUw2MYGS1d7uIx31pZ5UJ0M2d294Pt bFd17gax2aYw7pILQQbH/phK30SRZtxrx0An86b850xQSi2IAxXJRnna2x/oldMDvlne ZtkPjoRFTtKGnZ+Fb/XRS4AXTuXHOd3Hip7eeiO7vH87b37bpyhNrl4q7ivBNgcfCLfU 2f7Q== X-Gm-Message-State: AKGB3mJ9H+rsNn0Hy9m8bMkkhuKQJ37RtuLIOUjq9K4bFdg2fFPvyDwT xJ/ZGMwGsBf44DrrVGd2rmV/KeHe9Gw= X-Received: by 10.202.242.137 with SMTP id q131mr5161977oih.233.1513277555123; Thu, 14 Dec 2017 10:52:35 -0800 (PST) Return-Path: Received: from mail-oi0-f41.google.com (mail-oi0-f41.google.com. [209.85.218.41]) by smtp.gmail.com with ESMTPSA id q7sm2078491oif.20.2017.12.14.10.52.34 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 14 Dec 2017 10:52:34 -0800 (PST) Received: by mail-oi0-f41.google.com with SMTP id r63so4578270oia.6 for ; Thu, 14 Dec 2017 10:52:34 -0800 (PST) X-Received: by 10.202.216.70 with SMTP id p67mr4710105oig.243.1513277553828; Thu, 14 Dec 2017 10:52:33 -0800 (PST) MIME-Version: 1.0 Received: by 10.157.89.169 with HTTP; Thu, 14 Dec 2017 10:52:13 -0800 (PST) In-Reply-To: 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> From: Michael Shulman Date: Thu, 14 Dec 2017 10:52:13 -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 Thu, Dec 14, 2017 at 4:32 AM, Thorsten Altenkirch wrote: > Excellent observation! So basically the implementation of Lean is incorre= ct because we shouldn=E2=80=99t be able to derive true =3D false from the a= ssumption of propositional extensionality if we take account of the type an= notations. > > The example arose from the question whether we can add propositional exte= nsionality to Lean. That s we define HProp =3D Sigma P:Type.Pi x,y.P.x=3Dy.= Note that the equality we use here is the static Prop valued equality. Now= I suggested to add propositional extensionality for HProp as an axiom to L= ean but it seemed to lead to the problem. Well, if I understand you correctly, it sounds like the implementation of Lean isn't *currently* incorrect -- omitting such type annotations is a perfectly fine optimization for implementations of most type theories. It's just that it would have to be modified in order to *remain* correct under the addition of propositional extensionality for HProp. Right? > I still wonder what exactly is the difference between a static )(efnition= ally proof-irrelvant) Prop which seems to correspond to Omega in a topos an= d 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 pow= er. A prime example of that "extra power" is that with HProp you can prove 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, in which case unique choice is false. > 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" = 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 fa= lse > > And we don't have "first^{(b:Bool). false=3Db} x =3D=3D true", becaus= e > beta-reduction requires the type annotations on the projection and th= e > 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=E2=80=99t depend on other assumptio= ns you make. > > > > In set-level HoTT we define Prop as the types which have at most on= e inhabitant. Now wether a type is a proposition may depend on other assump= tions. (-1)-univalence i.e. propositional extensionality turns Prop into a = subobject classifier (if you have resizing otherwise you get some sort of p= redicative 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 /\ P= i y:A.P y -> x=3Dy then this is a proposition even though A may not be. How= ever using projections you also get Sigma x:A.P x. > > > > Hence I guess I should have said a topos with unique choice (I am n= ot sure wether this is enough). Btw, set-level HoTT also gives you QITs whi= ch eliminate many uses of choice (e.g. the definition of the Cauchy Reals a= nd 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 Pr= op > >>=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 betwee= n > >>propsoitional and judgemental equality. > >> > >>Thomas > >> > >> > >>> If you have proof-irrelevance in the strong definitional sense th= en you cannot be in a topos. This came up recently in the context of Lean w= hich 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) =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 exac= tly this). It is more important that our core theory is extensional and som= ething pragmatically close to definitional proof-irrelevance can be realise= d 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 Sy= stem U and hence inconsistent. > >>> >> > >>> >> By proof-irrelevance I assume that you mean that any two inhab= itants of a proposition are definitionally equal. This assumption is incons= istent with it being a tops since in any Topos you get propositional extens= ionality, that is P,Q : Prop, (P <-> Q) <-> (P =3D Q), which is indeed an i= nstance of univalence. > >>> >> > >>> > > >>> >I don't know if it's relevant to the current discussion, but I t= hought > >>> >the topos of sets with Prop taken to be the booleans would suppo= rt > >>> >both proof irrelevance and propositional extensionality, classic= ally > >>> >at least. Is there some extra assumption I am missing here? > >>> > > >>> > > >>> >> It should be possible to use a realizability semantics like om= ega-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 li= st but did not > >>> >> receive a conclusive answer so I am trying here now. Is th= e theory with > >>> >> a proof-relevant impredicative universe Set, proof-irrelev= ant > >>> >> 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 o= f tacking on > >>> >> an interpretation for Prop. > >>> >> > >>> >> Thanks in advance for any insight, > >>> >> > >>> >> Kristina > >>> >> > >>> >> > >>> >> > >>> >> > >>> >> > >>> >> > >>> >> > >>> >> This message and any attachment are intended solely for the ad= dressee > >>> >> and may contain confidential information. If you have received= this > >>> >> message in error, please send it back to me, and immediately d= elete 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 t= he > >>> >> University of Nottingham. > >>> >> > >>> >> This message has been checked for viruses but the contents of = an > >>> >> attachment may still contain software viruses which could dama= ge your > >>> >> computer system, you are advised to perform your own checks. E= mail > >>> >> communications with the University of Nottingham may be monito= red as > >>> >> permitted by UK legislation. > >>> >> > >>> > >>> > >>> > >>> > >>> This message and any attachment are intended solely for the addre= ssee > >>> and may contain confidential information. If you have received th= is > >>> message in error, please send it back to me, and immediately dele= te 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. Emai= l > >>> communications with the University of Nottingham may be monitored= as > >>> permitted by UK legislation. > >>> > > > > > > > > > > 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, s= end 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 Gr= oups "Homotopy Type Theory" group. > To unsubscribe from this group and stop receiving emails from it, sen= d 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.