From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.159.235.152 with SMTP id f24mr58618plr.37.1512994526826; Mon, 11 Dec 2017 04:15:26 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.98.194.93 with SMTP id l90ls1541220pfg.11.gmail; Mon, 11 Dec 2017 04:15:25 -0800 (PST) X-Received: by 10.99.168.15 with SMTP id o15mr45656pgf.17.1512994525837; Mon, 11 Dec 2017 04:15:25 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1512994525; cv=none; d=google.com; s=arc-20160816; b=oScYFjKa2MDqhurx0w3JzM0cTO00y/gsCNHcQ4pdA3ezYkq3B8dAtotD/KLLoi2Dj3 4LjkKCNur8gdjd0wPcjWvlgu+giKPbtwniHsuOIrkGhGhcD1nOg0Jtgq46d14ZX56xNv 6YMPr4PElc0qcxR7nnU9m0j79D006R6xi1iMh4Ky9lcVAVin6DWV0/bCdlbU1JRJCtDB OTDHbvppyaYB1P7QNdX6//Fxkh5osIOKpnQasUX1k9Syk4pcNfkA/2lTuJv/n0K8nrR1 ghQrVIX4JGZ4m6i9sPKumAAWxGj3wiIkJdXz/Xg9MXOmLjdZ4R+kC5nMAsybI6/ZgKww ecrg== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-language:content-transfer-encoding:in-reply-to:mime-version :user-agent:date:message-id:from:references:to:subject :dkim-signature:arc-authentication-results; bh=RnM26iAGnNqOua61D0oxn6ZEXM63I8AXZBJoWFx1YcQ=; b=Tlk3uKfRgcrDtOyHHK62tIw0/89lhkl5dJgc3SeYQjLBqbGWAR9mLiYyfsBJekCoif TEkoWQgI+NAREl84xt/IZp27UEGAqKBhTxUUCPc7gxoRd9h6DAAw6OShze9wvg7h6A08 rbjj5MTIuGq8eL0rjZDQ5R0hs5jgjVBdc9XIqHV265wmHBEiDv1a5JpLVDrIyzGnMRzH BQjGgo1E2MV5dGnEphiPSmqktD17/6wxn9xn0N2gPU0HD/Ysy4rtUb+LGW40Yw50Cbkz 6PUo4lJo988/285FEh6gqvFLgVYhDlggmxfUHSUpwWdzEbsOj9CIZqbqqi/7kFRLl9tJ lVQA== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=UoJGNHvg; spf=pass (google.com: domain of sojakova...@gmail.com designates 2607:f8b0:4002:c09::230 as permitted sender) smtp.mailfrom=sojakova...@gmail.com; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=gmail.com Return-Path: Received: from mail-yb0-x230.google.com (mail-yb0-x230.google.com. [2607:f8b0:4002:c09::230]) by gmr-mx.google.com with ESMTPS id e92si399145pld.1.2017.12.11.04.15.25 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Mon, 11 Dec 2017 04:15:25 -0800 (PST) Received-SPF: pass (google.com: domain of sojakova...@gmail.com designates 2607:f8b0:4002:c09::230 as permitted sender) client-ip=2607:f8b0:4002:c09::230; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=UoJGNHvg; spf=pass (google.com: domain of sojakova...@gmail.com designates 2607:f8b0:4002:c09::230 as permitted sender) smtp.mailfrom=sojakova...@gmail.com; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=gmail.com Received: by mail-yb0-x230.google.com with SMTP id j7so5445062ybl.3 for ; Mon, 11 Dec 2017 04:15:25 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=subject:to:references:from:message-id:date:user-agent:mime-version :in-reply-to:content-transfer-encoding:content-language; bh=RnM26iAGnNqOua61D0oxn6ZEXM63I8AXZBJoWFx1YcQ=; b=UoJGNHvgWVq1qaJldcGyG3bt/QIMolxToDM35r8/L07nv7Jtx/blDgI4J1eV38ciwx Vv0RbV8Wb8fMWXPBWsIevpldEsfMx1el87BwKrMmo7GJ9eAyn6OsZKhG81mdxPOftydj bwY0UqOceCp7aM3+Ij8V3BG/qlB7nTcIDmrb2J526zMkPvlOLBRdWsr0OeSzWQTLG82U 6Z/Lf2Z7DixZK6RD/7POm1Q7KJKnI+9E/Yuq6iTwTgpT/Ap7iQWUcQDXbZAdc5BUeGiv hiyPPbJgiPhHTDCt2BKZrTDasuj2iBcsYfKpx7OsUCFuvmDMuFnPwaVpU3fGl+ENQ79c e3yQ== X-Gm-Message-State: AKGB3mIjvq5sFk3v6t4P5eG3/RXUGx7UQTU/YTQIwY1NlJbFuIC7m5s9 bNS/dxs5vElNjSaaJ/i/tahFtLJ6 X-Received: by 10.37.210.216 with SMTP id j207mr114096ybg.268.1512994525289; Mon, 11 Dec 2017 04:15:25 -0800 (PST) Return-Path: Received: from [10.111.19.233] (h50.129.138.40.static.ip.windstream.net. [40.138.129.50]) by smtp.gmail.com with ESMTPSA id 128sm6124508ywr.3.2017.12.11.04.15.20 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Mon, 11 Dec 2017 04:15:20 -0800 (PST) Subject: Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent? To: HomotopyTypeTheory@googlegroups.com References: <4c4fe126-f429-0c82-25e8-80bfb3a0ac78@gmail.com> <1512992534.265543.1200966552.20A0FEC1@webmail.messagingengine.com> From: Kristina Sojakova Message-ID: Date: Mon, 11 Dec 2017 07:15:24 -0500 User-Agent: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:52.0) Gecko/20100101 Thunderbird/52.5.0 MIME-Version: 1.0 In-Reply-To: <1512992534.265543.1200966552.20A0FEC1@webmail.messagingengine.com> Content-Type: text/plain; charset=utf-8; format=flowed Content-Transfer-Encoding: 7bit Content-Language: en-US Hi Jon, Thanks for the answer! In this model, what would be the interpretation of the eq_A(a,b) : Prop type in Coq, which is logically equivalent to Id_A(a,b) : Type but proof irrelevant? Best, Kristina 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 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.