From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.28.218.138 with SMTP id r132mr337156wmg.20.1513106964436; Tue, 12 Dec 2017 11:29:24 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.223.142.136 with SMTP id q8ls2615190wrb.8.gmail; Tue, 12 Dec 2017 11:29:23 -0800 (PST) X-Received: by 10.28.8.12 with SMTP id 12mr348944wmi.1.1513106963089; Tue, 12 Dec 2017 11:29:23 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1513106963; cv=none; d=google.com; s=arc-20160816; b=x0RQKTe/o8vubRbMpGJoncEsCygjxYExuPJXk/hS0CclXdPZ7CvnmUCaUv8rIjqN+q +buydkDPzWgKZAHrON3eimY4vVmZPoqF8UKsEHDk/mM8bN4WBzUMmjdpi7rkOeLRkPix 4dGCOxAi8YezcCjfIzS/O2fi0/N5slaO6cah00ppTGC+UuHu0tb3yMJhTd+U1r+oOrj4 zHqcPRkRVhZMi4WdUi3/EcQv60py+9Ml9kGADLfjIzCgGbK/1lDE4vAiaNJjkj23N6Jf oqLvAGfOXeGC01pWDYc+5RtR9eOq6WwxAwrYKHr6ol36I9Zbbf3oirBZPFmxFLBFB/W5 GkIw== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=user-agent:in-reply-to:content-disposition:mime-version:references :message-id:subject:cc:to:from:date:arc-authentication-results; bh=pz9AmNJ8QtjFLHvcD49YK6ns871jOAcPQhbT9JRz9oc=; b=lKZqClf1EXIFpK+waPA6dzcjgWIY5ptFVg/7KoCX/GNzKFwTLKbPF30A4O0F8UBGRF 1SJqwI8hZ8towrak82orRNl/r8wVo5FrPKUBYuWkK4wJjL4WCsoNhfVZRn1d4rT29+/g vkcie5PvDpubLo0oCG1sYEHVpySTLf9ZCBb8JdwB2igsX/W0+9SsYqxeV8jBiTGxzE2X zOjng+3zmUI/e6XiH2MvOTe5zvKV7K+LKDSRLDeDvcjEukoENst1ebfP6rX8Nl/LrGbK 5UufNo0LcmDWnjLeX97CI+FJcKKFMBODlT2wx1QJK44OuKEZC5e6YhNL5Se6HboRCqR2 s1FQ== ARC-Authentication-Results: i=1; gmr-mx.google.com; spf=pass (google.com: best guess record for domain of stre...@mathematik.tu-darmstadt.de designates 130.83.156.225 as permitted sender) smtp.mailfrom=stre...@mathematik.tu-darmstadt.de Return-Path: Received: from lnx500.hrz.tu-darmstadt.de (mailout.hrz.tu-darmstadt.de. [130.83.156.225]) by gmr-mx.google.com with ESMTPS id r6si1771665wrg.2.2017.12.12.11.29.23 for (version=TLS1 cipher=AES128-SHA bits=128/128); Tue, 12 Dec 2017 11:29:23 -0800 (PST) Received-SPF: pass (google.com: best guess record for domain of stre...@mathematik.tu-darmstadt.de designates 130.83.156.225 as permitted sender) client-ip=130.83.156.225; Authentication-Results: gmr-mx.google.com; spf=pass (google.com: best guess record for domain of stre...@mathematik.tu-darmstadt.de designates 130.83.156.225 as permitted sender) smtp.mailfrom=stre...@mathematik.tu-darmstadt.de Received: from fb04281.mathematik.tu-darmstadt.de (fb04281.mathematik.tu-darmstadt.de [130.83.2.21]) by lnx500.hrz.tu-darmstadt.de (8.14.4/8.14.4/HRZ/PMX) with ESMTP id vBCJOW5E028107; Tue, 12 Dec 2017 20:24:32 +0100 (envelope-from stre...@mathematik.tu-darmstadt.de) Received: from fb04209.mathematik.tu-darmstadt.de (fb04209.mathematik.tu-darmstadt.de [130.83.2.209]) by fb04281.mathematik.tu-darmstadt.de (8.12.3/8.12.3/Debian-7.2) with ESMTP id vBCJTLRF024429; Tue, 12 Dec 2017 20:29:21 +0100 Received: by fb04209.mathematik.tu-darmstadt.de (Postfix, from userid 11003) id 82BF31A0CA8; Tue, 12 Dec 2017 20:29:21 +0100 (CET) Date: Tue, 12 Dec 2017 20:29:21 +0100 From: Thomas Streicher To: Jon Sterling Cc: HomotopyT...@googlegroups.com Subject: Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent? Message-ID: <20171212192921.GA11564@mathematik.tu-darmstadt.de> 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> <1513084622.1768586.1202387232.03F5CC27@webmail.messagingengine.com> MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline In-Reply-To: <1513084622.1768586.1202387232.03F5CC27@webmail.messagingengine.com> User-Agent: Mutt/1.5.23 (2014-03-12) X-PMX-TU: seen v1.2 by 5.6.1.2065439, Antispam-Engine: 2.7.2.376379, Antispam-Data: 2017.12.12.191817 X-PMX-RELAY: outgoing > 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). Of course, toposes all validate AUC. Since in an arbitrary topos logic is interpreted via the topos's Omega AUC holds then as well. Univalence is something which will not hold in most toposes and if it does one has to interpret Id in a way that it is not a proposition. Thomas