From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.80.195.1 with SMTP id a1mr272637edb.8.1512996190328; Mon, 11 Dec 2017 04:43:10 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.80.179.211 with SMTP id t19ls3408028edd.3.gmail; Mon, 11 Dec 2017 04:43:09 -0800 (PST) X-Received: by 10.80.163.200 with SMTP id t8mr269430edb.1.1512996189238; Mon, 11 Dec 2017 04:43:09 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1512996189; cv=none; d=google.com; s=arc-20160816; b=Ev1JBPP+NWV2V/cEo+InGN5U9mm7b1j1Br+EdoPtZinNMMaFTuVGkWIzLDbvKIiOWG 6m+WsI0afLcVVm67s39dOHJofwX9obV61ine8bi/4opTp/V/JBSRTqd/RhrWPYwVbFLl etu6JuTkmWSIU4FEkzcO9IpbtLZxBvzIpEX5Xd4S6q7iDgociDRlrlJyU+MLhonSx+yG XZEyVPJT1JnDYCcFrOzjHM3/rEO7TJ0bH/oXIfyaeTzi/Kl/BvHhFhCj1aZPW7Hrmb/O D2J8vk1pWgwxaeZw+aHHZPjWAYOy7+lAjImEGef66siZyNtl/Euh0FM5WgciSuC2Rd7X aAzQ== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=subject:date:references:in-reply-to:content-transfer-encoding :mime-version:to:from:message-id:dkim-signature :arc-authentication-results; bh=Q2TXIpswgMOn6j9L6nk9MOFxgIOIW0DXFWL3SokiyuE=; b=l9XfQKmHymSlKscYNHaqxcUdjCAsTNt7Ka2CjNm5vLUOxxCQkMFPrD83SNqzooL5HX +gvGIOlgQsrHRCAaF27LkNeIkEiJC6KIOi0533/0vxAdlBQdwIA6FUwxaQEeYkZwdx7V jGfmAjMYYGm9QjhHdAJAxdpwhsEOPdwp9P3Z6n3dALKvf2kWABrUln4ckKAtXCOP2UdP mDOth86sAnmJNJQkwCT06XPPe9X603Gyehle72E5asN9K/PeKUxPN+HoRC1/dkE3GxG5 yTy+vg+TmsZEBebtPw3YxmfV/6Fk7JipxTdRlJ8Qjjb/tFmq7y4pljFd5ko+QSYgKGbt Vyow== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@messagingengine.com header.s=fm1 header.b=MhCp7ZVM; 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 w21si1926914edl.5.2017.12.11.04.43.08 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Mon, 11 Dec 2017 04:43:09 -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=MhCp7ZVM; 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 2666220B19 for ; Mon, 11 Dec 2017 07:43:08 -0500 (EST) Received: from web2 ([10.202.2.212]) by compute2.internal (MEProxy); Mon, 11 Dec 2017 07:43:08 -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=Q2TXIp swgMOn6j9L6nk9MOFxgIOIW0DXFWL3SokiyuE=; b=MhCp7ZVMVPQS9raG/t1XVl 8MoNYxdWWSfhpXeGXj66iUeCvPq8t7rgwKzfV1QKZhRe/7gXC2NQgZq00JiF/uxt WLwuPWYLlIycVBKVHiF4McMOtaxlq0d33FmR/DiGvORAZ30pCBkyPwCRKvvzT4U6 5hlvj/y8ZPBnCm+2+o7mV5dHTe4XBLFWWUQQGYN3fvjpS4WMZpDPvp74YDNIN73b 4vhrvCGKpFO99MP+sPjG8OWcu1xqE+4dyZiTdgkA1RF0oEkVoybHOhip4TSwbWpo hxjMPBOGS+hO992r05PaK9cTqytREUjJRW4sKfwGSO4xwscGoq46z+3kSeLKR24Q == X-ME-Sender: Received: by mailuser.nyi.internal (Postfix, from userid 99) id 06E4462AF5; Mon, 11 Dec 2017 07:43:07 -0500 (EST) Message-Id: <1512996187.281015.1201017552.7F33C02E@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 In-Reply-To: References: <4c4fe126-f429-0c82-25e8-80bfb3a0ac78@gmail.com> <1512992534.265543.1200966552.20A0FEC1@webmail.messagingengine.com> Date: Mon, 11 Dec 2017 04:43:07 -0800 Subject: Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent? Hi Kristina, If you are using the subobject classifier to model Prop, I think that you can just use the ordinary equality predicate of the topos logic. The equality predicate for a type 'A' is given by the (generalized/Lawvere-style) existential quantification along the diagonal "=CE=B4 : X -> X * X". I think this ought to be the same as alternatively first constructing the identity type in the proof-relevant fragment and then reflecting it into the subobject classifier, since toposes model extensional identity types.=20 Best, Jon On Mon, Dec 11, 2017, at 04:15 AM, Kristina Sojakova wrote: > Hi Jon, >=20 > Thanks for the answer! In this model, what would be the interpretation=20 > of the eq_A(a,b) : Prop type in Coq, which is logically equivalent to=20 > Id_A(a,b) : Type but proof irrelevant? >=20 > Best, >=20 > Kristina >=20 >=20 > On 12/11/2017 6:42 AM, Jon Sterling wrote: > > Can we make sense of this by interpreting into a realizability topos? > > > > In particular, I am under the impression that Eff (the effective topos) > > models an impredicative universe of proof-relevant types, and on the > > other hand its subobject classifier can be used to model a > > proof-irrelevant Prop. > > > > As a topos, Eff models extensional type theory, and thence we have the > > functional extensionality law. > > > > Best, > > Jon > > > > > > On Sun, Dec 10, 2017, at 08:22 PM, Kristina Sojakova wrote: > >> Dear all, > >> > >> I asked this question last year on the coq-club mailing list but did n= ot > >> receive a conclusive answer so I am trying here now. Is the theory wit= h > >> 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 I= d > >> 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 > >> > >> --=20 > >> You received this message because you are subscribed to the Google Gro= ups > >> "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. >=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.