From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.25.115.12 with SMTP id o12mr626392lfc.33.1513506115948; Sun, 17 Dec 2017 02:21:55 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.46.32.233 with SMTP id g102ls1610295lji.10.gmail; Sun, 17 Dec 2017 02:21:54 -0800 (PST) X-Received: by 10.25.208.73 with SMTP id h70mr910426lfg.34.1513506114127; Sun, 17 Dec 2017 02:21:54 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1513506114; cv=none; d=google.com; s=arc-20160816; b=NpQQzXQtFwlnainkB0tFV8olAXWcIqLH1vooaKtLUgQB0GBH0HdjegY+IEapJSR8fd /x5mj7ip8OhUPlvdcPMZJX7q8ovddEnI/O+PZwTKLvTp1WwGvDDrbCLUpyLW8CV/QW5x +tHXWTeJ6WmsvqAaJPveXbqJjKr4larlppk+DlKGjMkbTYHom4talPlxNuQib1prdRQl Ejw3x6Zk2sV2LG2TZxFcAScDeq6yxb2XVhfG70n5DuA8PwkN2J6NOAM4A5Yri81c6K2s m0jHSoAAWGBmQ/vEZjkPDXWJ3Bsq+77RtgAUonJ9gdoYK/kQ3K9SF9nWlUeFPd7v154Y NRmA== 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=xuFonKyvhuIled6gpllTgZOuvme/c/ruYMZGlP925eU=; b=UQ5zgt5OqH9s9h64905dWzY5/H8Cige9F1Zpv7vvkOnHE3QsibbP8FUuy4GnjggcrN 5r/wHXyRwqJz1SFye6Jm+PgnNovo7NMsQ36Y1fKEAg6lvKeSC6+hT5o1iOyIqrP0Ajfz lnS5a99FfdxhAuOjnkGLnr8iQ34ZC595pYGt/C4OL98uewXlR2USRR99aiOaUgkGB+7R Sec0c/WdR1ZwXkeZAcrfI9y5yjNTBUrJtiDTWL4PGLLIpAtKqxOS0ejMc8uENsq32gwb MdWKW/Wg6ENKLeiFmJ3nGECxZOWwbRx+6COH2dEZQjwOHc40vw9mSJog5J+KF/tdhioi YYbQ== 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 64si1130972ljz.5.2017.12.17.02.21.53 for (version=TLS1 cipher=AES128-SHA bits=128/128); Sun, 17 Dec 2017 02:21:53 -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 vBHAGsu8008346; Sun, 17 Dec 2017 11:16:54 +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 vBHALpRF022472; Sun, 17 Dec 2017 11:21:51 +0100 Received: by fb04209.mathematik.tu-darmstadt.de (Postfix, from userid 11003) id 233EC1A3684; Sun, 17 Dec 2017 11:21:51 +0100 (CET) Date: Sun, 17 Dec 2017 11:21:51 +0100 From: Thomas Streicher To: Thorsten Altenkirch Cc: Andrea Vezzosi , Kristina Sojakova , Homotopy Type Theory Subject: Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent? Message-ID: <20171217102151.GA16619@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> <20171215170011.GA22027@mathematik.tu-darmstadt.de> MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline In-Reply-To: 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.17.101516 X-PMX-RELAY: outgoing > >Moreover, toposes will not validate univalence. As pointed out to me > >by Martin Escardo you can't even formulate it because in arbitrary > >toposes you don't have universe (not to speak of univalent ones). > > I was only talking about the special case of (-1)-univalence or > propositional extensionality that is for P,Q : Prop > > (P <-> Q) -> (P = Q) This would be ok but you assume also that Single(True) and Single(false) are propositions but they are just both ISOMORPHIC to 1 in Omega = Prop. That's where you apply UA for (sub)singletons UNCONSCIOUSLY. The inconsistency proof you have given is a slightly distorted version of the following ridiculous argument: {a} and {b} are isomorphic thus equal for which reason a = b. Thomas