From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.80.164.203 with SMTP id x11mr208595edb.7.1512992536624; Mon, 11 Dec 2017 03:42:16 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.80.144.196 with SMTP id d4ls3336938eda.4.gmail; Mon, 11 Dec 2017 03:42:15 -0800 (PST) X-Received: by 10.80.174.140 with SMTP id e12mr209134edd.12.1512992535514; Mon, 11 Dec 2017 03:42:15 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1512992535; cv=none; d=google.com; s=arc-20160816; b=dZtTlDCmMJWWK0XDebNnKUS4xFhQyMRZIoO3/3RfJf2xfkqK3UmZF7XCyET/cqODIQ gdJO0XRrk7NUFw78rPxx/D7MgOoeYIVz4iCuwvCogC4tY5lB3ol03CW8a1itBRH60/Ns WjToFoDeS0ODTiHbVOwm5GzZaqMdEq7A2VmvC1ouj5yotliX3S+/tVsJQJRDUnAyGi9j XAgRHY79Bcc+60kFffAPo+xw5sEkim54tTR95ncffyJmoYKjmP08bGNpU3IBUGPr8lH4 ReBPFI0V+drw1I3zVo8KkSqZgIUFbmMJgEljZKTrXi84sODivrJIbOVHQ2Qkrju81s/F IUWQ== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=subject:date:in-reply-to:references:content-transfer-encoding :mime-version:to:from:message-id:dkim-signature :arc-authentication-results; bh=OcbkHROTmtgeT3CHfw/fZiA/b2EutCuNCFtMRcTGSog=; b=wO+zzAMAkwJ0KY2lYeRFw5D+Uy9UBqR/TycIlMGjLCZSJF9QMa2pCQbIyNNM4SSyQ7 7p7XUJe1l2SHHtO6lYxDFG/Fx6umLcBcZQvzd4pbD/KDt6HTFe3bIAOhnk9ilLULiIkQ fa8iF3Ga5OBh0kklz+wmIhn+GD4mGSQEy0gZ7G7v1gIBRFsJf+xvcxV5WeyZxqSb8rpk mwXHlFI6YqfIu+JW1b7Qt1VQDGB9Vpznfsr0CFLD7jVYOZJEBoi6HTldw07e610pFPRa JL5WfIS7cddOFvQD9/wnzSHOLMXLAbVmnwERo3TEoPEuTYDa0jRhueLfTL8eDfThsiA0 wdXg== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@messagingengine.com header.s=fm1 header.b=V8BgrhbP; 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 w21si1912760edl.5.2017.12.11.03.42.15 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Mon, 11 Dec 2017 03:42:15 -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=V8BgrhbP; 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 640F720DAD for ; Mon, 11 Dec 2017 06:42:14 -0500 (EST) Received: from web2 ([10.202.2.212]) by compute2.internal (MEProxy); Mon, 11 Dec 2017 06:42:14 -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=OcbkHR OTmtgeT3CHfw/fZiA/b2EutCuNCFtMRcTGSog=; b=V8BgrhbPFLxkod51oO21zU DH13nHhnyf6dEXuwYEbfvv0+SjCdYyCrgdSiWB1BkU8d2rSrrQ00D363tPrQOavN wjWl7vYs0bwZ8HDi/nG8NLQ7uDV2eMK4oNa6wwidO3ugLKj8Xfzr749KQ9Q94Kz7 fMGcsPbxjRhiD+eahGmqKChBBe3tz1zokcggnfRWF/zmO5h0v9DB862a1VxgvD4B 8ZGSPzUnfsRBZBg8jVv1sjYzImJuCiETj7+yTYjX2pQPD1y3naUV6YC/wx79WsD4 EaLj9SOTAlHH6h+nEfsq7m0jGMnfMyEWFjfQGud7T80VGgOLj+lpKoJl58PiPbOQ == X-ME-Sender: Received: by mailuser.nyi.internal (Postfix, from userid 99) id 42F9F621C0; Mon, 11 Dec 2017 06:42:14 -0500 (EST) Message-Id: <1512992534.265543.1200966552.20A0FEC1@webmail.messagingengine.com> From: Jon Sterling To: HomotopyTypeTheory@googlegroups.com MIME-Version: 1.0 Content-Transfer-Encoding: 7bit Content-Type: text/plain; charset="utf-8" X-Mailer: MessagingEngine.com Webmail Interface - ajax-c9e5630e References: <4c4fe126-f429-0c82-25e8-80bfb3a0ac78@gmail.com> In-Reply-To: <4c4fe126-f429-0c82-25e8-80bfb3a0ac78@gmail.com> Date: Mon, 11 Dec 2017 03:42:14 -0800 Subject: Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent? 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 not > receive a conclusive answer so I am trying here now. Is the theory 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 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 > > -- > 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.