From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.31.177.76 with SMTP id a73mr2588117vkf.75.1513120514526; Tue, 12 Dec 2017 15:15:14 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.31.16.9 with SMTP id g9ls138304vki.5.gmail; Tue, 12 Dec 2017 15:15:12 -0800 (PST) X-Received: by 10.31.44.10 with SMTP id s10mr2572357vks.90.1513120512948; Tue, 12 Dec 2017 15:15:12 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1513120512; cv=none; d=google.com; s=arc-20160816; b=XAtgfLQFRqDOBJPbj1jFnQSo+y1lZ7C63sgn4ls1r+zcXi1Gg54C0NOVfMTm9o1gKD 3ERis6UReBSFoirBVVobaz/8ao7Lcc9OyIOmRdGdDFYmvXkztxCHMiizhxbKPHEcs+6M fRqgV15s8B/dyzBvEt+528h9IZflzjOSmFpU2sNn7fJidwaOiedXO5GUNswjyWXTX0GN ae16Dq9zgmMOnlKJQWK/nBB0DHSyxyzN/UoeqgC4wzH3EFdxWG05y4gK/qW9kEN36nTc ivf3/tDVt1q28O5nwWl770QO2mF0b9LbuGKhE+GqiAnaKwvMkJeNSmoL76hs51sXPH68 IltA== 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=/7yDYaII0Yqwi4naQcaCX2YtjsC5lJWrntzfJ+/4QJk=; b=CfWICliIroOqT1UMNwsyN9TK4HqQXiR6Vojcv11huv6HZHfAGzU8mLU6xlCSJYWruz U5FMZo1tyJEMxggTCkjUThZFk1Zi1L6Hhbzebrrf1dgRTTo8SXWMXjtOX7TSGQIjz6kJ gADpCocGee/3QAPdknnM+AloWQAbOcSEcZswKaZvKTjEb+22uvkJptSlEH2OI3GLxKnr EYtNSC43XviWy20cl9fjYIwsWl2CuioAZWJ57TT11u6hg4dLQzutptaQCDnR87L1LgkT 3os7F/t9Z+jAzfFJeltc8lKtzx3/Th0D09+Z+EyQ5XQYdqG4wDJ1O155KCj6+lVpO9KZ 596w== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=S+Ai/To8; spf=neutral (google.com: 2607:f8b0:4003:c0f::233 is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Return-Path: Received: from mail-ot0-x233.google.com (mail-ot0-x233.google.com. [2607:f8b0:4003:c0f::233]) by gmr-mx.google.com with ESMTPS id 68si27325uaj.0.2017.12.12.15.15.12 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Tue, 12 Dec 2017 15:15:12 -0800 (PST) Received-SPF: neutral (google.com: 2607:f8b0:4003:c0f::233 is neither permitted nor denied by domain of shu...@sandiego.edu) client-ip=2607:f8b0:4003:c0f::233; Authentication-Results: gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=S+Ai/To8; spf=neutral (google.com: 2607:f8b0:4003:c0f::233 is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Received: by mail-ot0-x233.google.com with SMTP id 103so465662otj.12 for ; Tue, 12 Dec 2017 15:15:12 -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=/7yDYaII0Yqwi4naQcaCX2YtjsC5lJWrntzfJ+/4QJk=; b=S+Ai/To8xtq9jtQ6IxKX0SO4RlqOBf4cTUUTuMvEG+E+rWo8eUjJSx73ortwyXBzhd hm4SWFJwP1b+tOSdn/ea655mKsb29JzPF7c0uD8VKiKPpxAhGlbqfs+/SFI5Zz5kl1Wx TjfN003mifQw9kzka4S9pCu8rjpEvweEon1uuPwyd5Yzv+Wp8BQhYWlcMUu1bkuJ56gw n/GEzjfon/242uBSDuuXjM8A+F8IFalYZEOxP4FbYDHdlaENQetagU28q59PS9HZMJq8 YpOuapzJQRJT14MWZ6/B2V4xO7NILu+cojvzKdbRa4fomw/V0RhD+RvR8jqb+JabGJC+ 262g== X-Gm-Message-State: AKGB3mJ+Zcmof0o0DwgqJd8jvJnfPGKE8U1TetmUgbW3iW+KHp/hXDUH O4DkS1grnRYUy72cTs9Ciu2kBzoJLjU= X-Received: by 10.157.29.151 with SMTP id y23mr426663otd.61.1513120512314; Tue, 12 Dec 2017 15:15:12 -0800 (PST) Return-Path: Received: from mail-ot0-f172.google.com (mail-ot0-f172.google.com. [74.125.82.172]) by smtp.gmail.com with ESMTPSA id u65sm152226oia.46.2017.12.12.15.15.11 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Tue, 12 Dec 2017 15:15:11 -0800 (PST) Received: by mail-ot0-f172.google.com with SMTP id 103so467047otj.12 for ; Tue, 12 Dec 2017 15:15:11 -0800 (PST) X-Received: by 10.157.43.244 with SMTP id u107mr450866ota.121.1513120511123; Tue, 12 Dec 2017 15:15:11 -0800 (PST) MIME-Version: 1.0 Received: by 10.157.89.169 with HTTP; Tue, 12 Dec 2017 15:14:50 -0800 (PST) In-Reply-To: <643DFB5A-10F8-467F-AC3A-46D4BC938E85@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> From: Michael Shulman Date: Tue, 12 Dec 2017 15:14:50 -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 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=E2=80=99t depend on other assumptions you= make. > > In set-level HoTT we define Prop as the types which have at most one inha= bitant. Now wether a type is a proposition may depend on other assumptions.= (-1)-univalence i.e. propositional extensionality turns Prop into a subobj= ect classifier (if you have resizing otherwise you get some sort of predica= tive topos). > > However, the dynamic interpretation of propositions gives you some additi= onal power, in particular you can proof unique choice, because if you can p= rove 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 u= sing projections you also get Sigma x:A.P x. > > Hence I guess I should have said a topos with unique choice (I am not sur= e wether this is enough). Btw, set-level HoTT also gives you QITs which eli= minate 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 i= s a type-theory based interactive proof system developed at microsoft and w= hich 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) : Pro= p 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 (defini= tionally): >>> >>> 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 th= is). It is more important that our core theory is extensional and something= pragmatically close to definitional proof-irrelevance can be realised as s= ome 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 extensionali= ty, that is P,Q : Prop, (P <-> Q) <-> (P =3D Q), which is indeed an instanc= e 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-se= ts or Lambda-sets to model the impredicative theory and identify the propos= itions with PERs that are just subsets. >>> >> >>> >> Cheers, >>> >> Thorsten >>> >> >>> >> >>> >> On 11/12/2017, 04:22, "homotopyt...@googlegroups.com on behalf of Kr= istina 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 theo= ry 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 theor= y >>> >> incompatible with univalence, so it is not just a matter of tack= ing on >>> >> an interpretation for Prop. >>> >> >>> >> Thanks in advance for any insight, >>> >> >>> >> Kristina >>> >> >>> >> >>> >> >>> >> >>> >> >>> >> >>> >> >>> >> This message and any attachment are intended solely for the addresse= e >>> >> 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 thi= s >>> >> message or in any attachment. Any views or opinions expressed by th= e >>> >> 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 you= r >>> >> 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. >>> > > > > > 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.