From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.157.22.193 with SMTP id s1mr1639645ots.104.1513073750738; Tue, 12 Dec 2017 02:15:50 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.157.18.139 with SMTP id g11ls1840108otg.15.gmail; Tue, 12 Dec 2017 02:15:49 -0800 (PST) X-Received: by 10.202.86.203 with SMTP id k194mr1591667oib.88.1513073749875; Tue, 12 Dec 2017 02:15:49 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1513073749; cv=none; d=google.com; s=arc-20160816; b=WmgQsirnBWQ1Nj3WLbSJfeB4pPwoAg7Uv13HbNPka0oPgu6YfaYH8Eb4f/fU3hE7hH 7Jd4u51oQCnLqcIT6sBNEJrBEG8I+fYawoAFsuu0E2jp+GxCCGfdUDICQKp+z/b6DUVw 4SmB0tZxlegB+rXh7+WotA9ijNB0wd2GfmPCJ0jcWCYvdaQTvqhQgxg+oJ67cVfiXkiQ uzzzWhudTzRy/5KR5l2lqSEYbECZB1s7OsrVuCS11AL0hF+A+8EY+U4IdkeeEGZ4RiWe LPoim4pRTpVUz1wFIGWy6VmXlFYawp8OVolmBKqLSbJQaSMpJKTTVrjrm9OSLJ+phihX ciQQ== 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=SIclVFfT0flqupcbDnvQwKnwRVQd06GPZ25PCvqB07k=; b=hy2GdUGRoW4Uf0tZHqSlT8+2/sdH1sTW8h6sZDmUn3RUbyKlFhPFD9G7g3EPvoTsdr 0vVjZuT4+eFBEYQ8QEIjh9Fxco1KiTrCEgCxHZ6pDZmHxXPBWVDpNMfofQYeq9Omfn2g LrHr/wSHTI/C3ovzDeUVBFZS9RlGRZOD5wLulGLmeYLEYvC0e1DcXR7hpUymntaJe5DA gu5zSaa1SDx/dzLgRzFnhtgpwfX0l2vtIisB2qDQ/TppOX6j1Iuq62ZeWUbcGj3pjmlE MhJAruHLZPrCy3h2D5zrINJAWTupZG0WiJTeFOnxAfsaakO4CFWt80+dqMBCLeCIJyoG wzsw== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=e+y+hhgX; spf=pass (google.com: domain of sanz...@gmail.com designates 2607:f8b0:4001:c0b::234 as permitted sender) smtp.mailfrom=sanz...@gmail.com; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=gmail.com Return-Path: Received: from mail-it0-x234.google.com (mail-it0-x234.google.com. [2607:f8b0:4001:c0b::234]) by gmr-mx.google.com with ESMTPS id m74si990880oig.2.2017.12.12.02.15.49 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Tue, 12 Dec 2017 02:15:49 -0800 (PST) Received-SPF: pass (google.com: domain of sanz...@gmail.com designates 2607:f8b0:4001:c0b::234 as permitted sender) client-ip=2607:f8b0:4001:c0b::234; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=e+y+hhgX; spf=pass (google.com: domain of sanz...@gmail.com designates 2607:f8b0:4001:c0b::234 as permitted sender) smtp.mailfrom=sanz...@gmail.com; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=gmail.com Received: by mail-it0-x234.google.com with SMTP id o130so16663806itg.0 for ; Tue, 12 Dec 2017 02:15:49 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc:content-transfer-encoding; bh=SIclVFfT0flqupcbDnvQwKnwRVQd06GPZ25PCvqB07k=; b=e+y+hhgX2OSSplmIkU7BiaATAJ1eTOPrmjMjwrQ/VL7fUxB46LoNJpnzOaXbIm/NeG /IA32GZBIU/WSBp78VpYyQvpmahcRc/MlhHTMPl8Fv1sezs86f+hKI0g7BYGXG6IIDih Um4fO3EaPn/F8Or361CEe+t8VdhaLUVGH0z+AtGLwzhvBSxkEbDFUOPzXBmc3Bb/4GtL HY17HlTHYX5Kfqey+DwYLH0LEWjKVys/IeQ++wNcHiI/3Zo7ZVlUMglmMwL0MHiFeYgF qMPQElCk57rklaNUraW38ZdVXsYXjEKnIbo9IQLgR5ABXmJaHmnEn6FCrTYgAmDT/5tv hqkQ== X-Gm-Message-State: AKGB3mIINgMgbkJ+8qiawE3wEeHX7fYhZwDW6Zy1svpxzGhyRM1244Iv IGQ9eh6vh9aiFPnqCvyxM5X3GvurfamWKBOqFGI= X-Received: by 10.36.70.195 with SMTP id j186mr1820716itb.32.1513073749483; Tue, 12 Dec 2017 02:15:49 -0800 (PST) MIME-Version: 1.0 Received: by 10.107.128.214 with HTTP; Tue, 12 Dec 2017 02:15:48 -0800 (PST) In-Reply-To: References: <4c4fe126-f429-0c82-25e8-80bfb3a0ac78@gmail.com> From: Andrea Vezzosi Date: Tue, 12 Dec 2017 11:15:48 +0100 Message-ID: Subject: Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent? To: Thorsten Altenkirch Cc: Kristina Sojakova , Homotopy Type Theory Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable 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, t= hat is P,Q : Prop, (P <-> Q) <-> (P =3D 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 proposition= s with PERs that are just subsets. > > Cheers, > Thorsten > > > On 11/12/2017, 04:22, "homotopyt...@googlegroups.com on behalf of Kristin= a 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 wi= th > 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 o= n > an interpretation for Prop. > > Thanks in advance for any insight, > > Kristina > > -- > 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.