From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.46.101.14 with SMTP id z14mr337026ljb.26.1513084627598; Tue, 12 Dec 2017 05:17:07 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.25.190.212 with SMTP id o203ls221129lff.17.gmail; Tue, 12 Dec 2017 05:17:04 -0800 (PST) X-Received: by 10.46.100.12 with SMTP id y12mr338392ljb.25.1513084624791; Tue, 12 Dec 2017 05:17:04 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1513084624; cv=none; d=google.com; s=arc-20160816; b=nz3zw0T2b0XG7+TfXeZYayi6Ib/QodsAEKDx6YJP4NoZMls3dQA08e9hoi1Q7TqnW8 gVa8fnDk9HHxPmBtNORdD1Mz+UL/oLMCOMGKHMYk3G4avX4ThBWH0r7HDnpaK1ZuAehE +k2SUUyQSvswCrr/U224YRtvX3Lr6ywOcPLB2UXbCBt0H8EKkSYSBy/kCkIu6/UkKouE 9HfCRxqLtoXtvNrVgfAzRYH96NwltBE6qxG1j783Ujnvp9GFtVl2JDo088zT/aPYP/qZ 30RGiJJKd3HHcgxmFQ3Kj8cyIfPA8nmD3oxswTMdr4MiTKPAwjZ4Q0y86M7+/v9ZdyGX minQ== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=in-reply-to:subject:date:references:content-transfer-encoding :mime-version:to:from:message-id:dkim-signature :arc-authentication-results; bh=Xcsiponuya4FDo8AHKffAVHdOZMwR8/LF9zu+FYR4Ew=; b=CTpH0+OpB02YQt3jtycAYF4DiI6b9xwyf9FOX4B0swasjDyIYjDuzgLqFd/FEgXdGT CMbiwTmutWgo/E2zUvQ+ZRwzVmx4J26ta9hd0aDUddVTOXecPBRG5jr00e6vqtD7IfrB QZcTO8dV222pzbqTQHO6yT+tmHczskrQvubhMhVw/IB/5DFUqeWFGnKW39tZQkOyJfN0 6Gn9OEgym+CRlOxKUXQdZH3KoJZ4L9evUy9TolSREiqL9EiT1Qau+uc/GcQdKfm7RaJt uKSiXz19ZRtN1XGwFpPDtPo82X964JgOdvPIsr8VdFRf870CkofEJUZly+esX1+bPYC3 IAfQ== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@messagingengine.com header.s=fm1 header.b=CCtss3jI; spf=neutral (google.com: 66.111.4.27 is neither permitted nor denied by best guess record for domain of j...@jonmsterling.com) smtp.mailfrom=j...@jonmsterling.com Return-Path: Received: from out3-smtp.messagingengine.com (out3-smtp.messagingengine.com. [66.111.4.27]) by gmr-mx.google.com with ESMTPS id q27si1631322lfd.0.2017.12.12.05.17.04 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Tue, 12 Dec 2017 05:17:04 -0800 (PST) Received-SPF: neutral (google.com: 66.111.4.27 is neither permitted nor denied by best guess record for domain of j...@jonmsterling.com) client-ip=66.111.4.27; Authentication-Results: gmr-mx.google.com; dkim=pass head...@messagingengine.com header.s=fm1 header.b=CCtss3jI; spf=neutral (google.com: 66.111.4.27 is neither permitted nor denied by best guess record for domain of j...@jonmsterling.com) smtp.mailfrom=j...@jonmsterling.com Received: from compute2.internal (compute2.nyi.internal [10.202.2.42]) by mailout.nyi.internal (Postfix) with ESMTP id 4698620BD8 for ; Tue, 12 Dec 2017 08:17:02 -0500 (EST) Received: from web2 ([10.202.2.212]) by compute2.internal (MEProxy); Tue, 12 Dec 2017 08:17:02 -0500 DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d= messagingengine.com; h=content-transfer-encoding:content-type :date:from:in-reply-to:message-id:mime-version:references :subject:to:x-me-sender:x-me-sender:x-sasl-enc; s=fm1; bh=Xcsipo nuya4FDo8AHKffAVHdOZMwR8/LF9zu+FYR4Ew=; b=CCtss3jIN5cIphfWPBKQQp hjTTrjYt3nQnlhPdJy6qVhF6yEwnkG4ZvEhXf3PnryvWS/PMgVdivLWY+T4+BR6g bGVtyQpCba7PfSvc4tgHE2wESnwKLu4Q7Hmorxp8VB+b1zMxODxWCwzpQNEUBJbI TXPCZqe3IxVZX7CtFTwWJtz/2rbMGnEjkaxcXLcOBg+7YXoTcH6LXOLBow58PxL/ XSpUPEi+1GnGcrwzDVixeqDq7N3RDt8A+PjMeiAyYhymfmipYI0V7bKNd+7BVzn1 4IYDKzMCHjjTNpk7PsFYh2f2uYHFcSi5l6e5ygk/EOdUZW7E0PrrupMfSaWjsoeQ == X-ME-Sender: Received: by mailuser.nyi.internal (Postfix, from userid 99) id 1897E62793; Tue, 12 Dec 2017 08:17:02 -0500 (EST) Message-Id: <1513084622.1768586.1202387232.03F5CC27@webmail.messagingengine.com> From: Jon Sterling To: HomotopyTypeTheory@googlegroups.com MIME-Version: 1.0 Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset="utf-8" X-Mailer: MessagingEngine.com Webmail Interface - ajax-c9e5630e 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> Date: Tue, 12 Dec 2017 05:17:02 -0800 Subject: Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent? In-Reply-To: <643DFB5A-10F8-467F-AC3A-46D4BC938E85@exmail.nottingham.ac.uk> On Tue, Dec 12, 2017, at 04:21 AM, Thorsten Altenkirch wrote: > Good point. >=20 > 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 yo= u make. >=20 > 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 turns Prop > into a subobject classifier (if you have resizing otherwise you get some > sort of predicative topos). >=20 > 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 b= e. > However using projections you also get Sigma x:A.P x. >=20 > Hence I guess I should have said a topos with unique choice (I am not > sure wether this is enough).=20 Thorsten, I think that unique choice holds in every topos, at least when you state it in the topos logic. This is in Mac Lane & Moerdijk as exercise 11 in chapter VI, Topoi And Logic. I'm a little confused now, but maybe this has to do with some subtle difference between the ordinary topos-theoretic subobject classifier, and the HoTT-style one which you get from univalence (as you describe). Best, Jon > 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). >=20 > Thorsten >=20 >=20 >=20 >=20 >=20 >=20 > On 12/12/2017, 12:02, "Thomas Streicher" > wrote: >=20 > >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 yo= u 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: > >>=20 > >> Given a:A define Single(a) =3D Sigma x:A.a=3Dx. We have Single(a) : Pr= op and > >>=20 > >> p : Single(true) <-> Single(false) > >>=20 > >> since both are inhabited. Hence by extProp > >>=20 > >> extProp p : Single(true) =3D Single(false) > >>=20 > >> now we can use transport on (true,refl) : Single(true) to obtain > >>=20 > >> x =3D (extProp p)*(true,refl) : Single(false) > >>=20 > >> and we can show that=20 > >>=20 > >> second x : first x =3D false > >>=20 > >> but since Lean computationally ignores (extProp p)* we also get (defin= itionally): > >>=20 > >> first x =3D=3D true > >>=20 > >> My conclusion is that strong proof-irrelvance is a bad idea (note that= my ???99 paper on Extensionality in Intensional Type Theory used exactly t= his). It is more important that our core theory is extensional and somethin= g pragmatically close to definitional proof-irrelevance can be realised as = some tactic based sugar. It has no role in a foundational calculus. > >>=20 > >>=20 > >> Thorsten > >>=20 > >>=20 > >>=20 > >>=20 > >> On 12/12/2017, 10:15, "Andrea Vezzosi" wrote: > >>=20 > >> >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 inhabitant= s of a proposition are definitionally equal. This assumption is inconsisten= t with it being a tops since in any Topos you get propositional extensional= ity, that is P,Q : Prop, (P <-> Q) <-> (P =3D Q), which is indeed an instan= ce of univalence. > >> >> > >> > > >> >I don't know if it's relevant to the current discussion, but I though= t > >> >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-s= ets or Lambda-sets to model the impredicative theory and identify the propo= sitions with PERs that are just subsets. > >> >> > >> >> Cheers, > >> >> Thorsten > >> >> > >> >> > >> >> On 11/12/2017, 04:22, "homotopyt...@googlegroups.com on behalf of K= ristina Sojakova" wrote: > >> >> > >> >> Dear all, > >> >> > >> >> I asked this question last year on the coq-club mailing list bu= t did not > >> >> receive a conclusive answer so I am trying here now. Is the the= ory 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 make= s the Id > >> >> type behave differently usual and in particular, makes the theo= ry > >> >> incompatible with univalence, so it is not just a matter of tac= king on > >> >> an interpretation for Prop. > >> >> > >> >> Thanks in advance for any insight, > >> >> > >> >> Kristina > >> >> > >> >> > >> >> > >> >> > >> >> > >> >> > >> >> > >> >> 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. > >> >> > >>=20 > >>=20 > >>=20 > >>=20 > >> 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= .=20 > >>=20 > >> 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. > >>=20 > >> 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. > >>=20 >=20 >=20 >=20 >=20 > 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.= =20 >=20 > 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. >=20 > 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. >=20 > --=20 > 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.