From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.223.196.221 with SMTP id o29mr864627wrf.9.1513770074777; Wed, 20 Dec 2017 03:41:14 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.223.161.27 with SMTP id o27ls6590624wro.2.gmail; Wed, 20 Dec 2017 03:41:13 -0800 (PST) X-Received: by 10.28.0.74 with SMTP id 71mr692045wma.32.1513770073881; Wed, 20 Dec 2017 03:41:13 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1513770073; cv=none; d=google.com; s=arc-20160816; b=JxtCO3MdFluU2U7KXBPmMNpxoMdzs3zu60SOIwnnDbUZElz4jV8BM/QVAW5AG/cP3b 8dsQ9dxCGnzHekeLYaoONOM30xIVu4iCB6w0hiE/OJi0gk0byblvdvsyN8EYypKzz8og 9/yJCkjRsjs0itzSXX1o1AIiieobvAcBmGsR6xmIBkRgeKy2hWcvAirYfGGvDj4ARcZV fdYhdCPVP16uxWMwBBrpsHBq3JJj6syHZ2H2HvzaqrlvA+lmScSLPVvES3Tvng6mc4Yg yBaPPGToed8Ea9EMdJeg8UiGQXBcNwEl2cIXqRPLhd7D8QFJIhIv1lVbOg53s8wFQ8OK R2cA== 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=Dld2+yIK3VPI+b/GW1wfQkCZmLQUjsCN1wlY33Vyq80=; b=YghxHvhD2/JqVH/vWP/fIEb3uveSFB79HHFr0I4xa3zbvrtCDvGz5l8fIa0QsSi5k5 OWue+xTU8KKAqAPGLoC691wRpLdIG4JyJrnBl7v79k+al9hT6bZ8Mq7XjlkM+dWuqd8V nj2qQIsh07X+LchCGXam49ldZg7zm3/kkuv1xYp2Mi6Gx4z8NfIdw5Ic4PWvsWzNHwVQ 4PCuWapV714qiScEFgiahMPn2SXZIv0Lu+5O5pOoG52/07i5Il/6Cwe49LfSfCcWvwEA cFq9yrfnMDs7te2GqI0GslPFgKngeCbSaR9Lrzhr6f6LFTli9tuOMk7dUSaenxA6nnQ7 J6wQ== 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 m4si2151317wrm.4.2017.12.20.03.41.13 for (version=TLS1 cipher=AES128-SHA bits=128/128); Wed, 20 Dec 2017 03:41:13 -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 vBKBa3iW029443; Wed, 20 Dec 2017 12:36:05 +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 vBKBf4RF006981; Wed, 20 Dec 2017 12:41:04 +0100 Received: by fb04209.mathematik.tu-darmstadt.de (Postfix, from userid 11003) id 99CE11A3B65; Wed, 20 Dec 2017 12:41:04 +0100 (CET) Date: Wed, 20 Dec 2017 12:41:04 +0100 From: Thomas Streicher To: Thorsten Altenkirch Cc: Andrej Bauer , Homotopy Type Theory Subject: Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent? Message-ID: <20171220114104.GG8054@mathematik.tu-darmstadt.de> References: <20171218115228.GB29410@mathematik.tu-darmstadt.de> <55AAFF96-F751-4A01-BE3E-280A438A55DC@exmail.nottingham.ac.uk> <20171219153118.GA9218@mathematik.tu-darmstadt.de> <20171219163139.GB13875@mathematik.tu-darmstadt.de> <20171220110052.GC8054@mathematik.tu-darmstadt.de> <5B8F4A6C-DD7C-4A14-812C-4AEA35C41BEA@exmail.nottingham.ac.uk> MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline In-Reply-To: <5B8F4A6C-DD7C-4A14-812C-4AEA35C41BEA@exmail.nottingham.ac.uk> 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.20.113316 X-PMX-RELAY: outgoing Hi Thorsten, > we have already established that my argument was incorrect (for the > reasons you state) and I was misinformed about the behaviour of > Lean. I know, I just wanted to spot where the problem precisely is. > >Another gap in Thorsten's argument is the following. Though Single(a) and > >Single(a') are isomorphic in order to conclude that they are propositionally > >equal they would have to be elements of a univalent universe BUT I don't see > >where such a universe should come from in the general topos case! > I don???t understand this point. In a type theoretic implementation of a topos Single(a) and Single(a???) would be propositionally equal due to propositional extensionality. The only additional assumption I need to make is that the universe of proposition is strict, e.g. we have that El(A -> B) is definitionally equal to EL(A) -> El(B). This seems to be quite natural from the point of type theory where universes are usually strict and moreover this is true in any univalent category giving rise to a topos. Well, Single(a) and Single(a') were propsitionally equal if they were elements of a univalent universe U but where should this come from if you start from an elementary topos in a univalent metatheory. Thomas