From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.99.135.199 with SMTP id i190mr1671446pge.168.1513728869069; Tue, 19 Dec 2017 16:14:29 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.159.255.70 with SMTP id u6ls4314594pls.9.gmail; Tue, 19 Dec 2017 16:14:28 -0800 (PST) X-Received: by 10.84.167.230 with SMTP id i35mr1632854plg.17.1513728868014; Tue, 19 Dec 2017 16:14:28 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1513728867; cv=none; d=google.com; s=arc-20160816; b=M6SLjASJ3aSwWm4h8FnMTpcijtdQNN8HWz25pRnIwNvZ7TBXx4iEN1c+fwT86rQjZY zb26JnEjbwGJ/E88YsnD2uCjRm001SpctKg+wyI0nITZzGMLnOrVz7OZdzc7EXo32kYI yHbFQHncAniRyDZyNdiuoIggBt7sM5lNrDxLtX2oz02ZnPiKTU353k9y4nDIK90Gbr/g fsUFmPuKPcQJoR9XVz5qCFTLuI5PpCR9HoWiiPBk3LrIz0L8Vef2zGpiI03Eqd5n8CiY xSt8IOrCHPtszWM3Pki2/u1R8BXMdwtMLbY6C67oEDiQ2yu6pcfOC9SX0ICnmRXvtFTq bYag== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-transfer-encoding:cc:to:subject:message-id:date:from :references:in-reply-to:mime-version:dkim-signature :arc-authentication-results; bh=x5OMPDlvCExeaSryVSrBbFJ3ZNTSYMIoSX9A2+qV/1s=; b=vSSx+iakiPLypCuZPfDhe9RbZezGkd/z1qNs9qyIX9XBBqnIzCjceG8PlLA/HYX9P4 D9ftWr9qw8TX8IU5iFVsaooQ9lKp3uM34uH4XGPuQTZ/4P7VZWNlaYN8uGkgSD//KvIt K7PicAZQbOPHy3WG4xcDse6g+nVG5m2NACkPMNxqRGyLwUshqaiBGJkiuk+V3g+cuBil jKD5PD0g+d3Tuzubg5+/l61Hw+WQDq6dl5SbFdHO1PUSHyp/Ne0Mi63Rk3/g+kHi0FAe wRN+GLEjPOmt4i4WIocJbjaRvAKHVsQX+jw3vcmg2y+eSsYkWT0Q0A8XQ5SDCvXDxo3c 0Bpw== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@andrej-com.20150623.gappssmtp.com header.s=20150623 header.b=OzqCChGH; spf=neutral (google.com: 2607:f8b0:4002:c09::231 is neither permitted nor denied by best guess record for domain of andrej...@andrej.com) smtp.mailfrom=andrej...@andrej.com Return-Path: Received: from mail-yb0-x231.google.com (mail-yb0-x231.google.com. [2607:f8b0:4002:c09::231]) by gmr-mx.google.com with ESMTPS id b9si848038pff.4.2017.12.19.16.14.27 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Tue, 19 Dec 2017 16:14:27 -0800 (PST) Received-SPF: neutral (google.com: 2607:f8b0:4002:c09::231 is neither permitted nor denied by best guess record for domain of andrej...@andrej.com) client-ip=2607:f8b0:4002:c09::231; Authentication-Results: gmr-mx.google.com; dkim=pass head...@andrej-com.20150623.gappssmtp.com header.s=20150623 header.b=OzqCChGH; spf=neutral (google.com: 2607:f8b0:4002:c09::231 is neither permitted nor denied by best guess record for domain of andrej...@andrej.com) smtp.mailfrom=andrej...@andrej.com Received: by mail-yb0-x231.google.com with SMTP id 69so14860876ybc.6 for ; Tue, 19 Dec 2017 16:14:27 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=andrej-com.20150623.gappssmtp.com; s=20150623; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc:content-transfer-encoding; bh=x5OMPDlvCExeaSryVSrBbFJ3ZNTSYMIoSX9A2+qV/1s=; b=OzqCChGHBbLfrzp35Qsu9VMF6s8FKcgVMAUWZ+0B7Ub591ckXWXRZ1GtvYF+oJollc lcgqelh1Z7V9FFHGOxICjDWl/MP4r1RwcxRZchD5Lq4rxoa5+9XFYlvUBx/LxcSL5GbS el8EvwHTWMZe45JC1f3wq4qwGw9CaqDBzO8f7odZhxf0dWDrcnB4k678MimcJETO5zv1 89S+l5EEOxjuNDTVNiCSmtQXWzG4fynSO2i+rk4YX/GOQeakVVOn9Lw2EIbP4G5TuSIT 1vSLGMK+YIX7zBThaWFzAc+n5hIwT0RV9Qnd56miP/fVWyXvvq8IM/XvfIcZwPBuFs9o FQ5A== X-Gm-Message-State: AKGB3mJz4hFKaOm6QnWcpEINBZY/xUiiCYKUieCD4h4/5FddF3500+4s 8SSalo3Y1xcFesoLHpQ2efuWOKGKL0nzh8w9Xy+grw== X-Received: by 10.37.90.87 with SMTP id o84mr3909702ybb.2.1513728866820; Tue, 19 Dec 2017 16:14:26 -0800 (PST) MIME-Version: 1.0 Received: by 10.37.9.2 with HTTP; Tue, 19 Dec 2017 16:14:26 -0800 (PST) X-Originating-IP: [193.77.148.136] In-Reply-To: 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> <20171217102151.GA16619@mathematik.tu-darmstadt.de> <20171218115228.GB29410@mathematik.tu-darmstadt.de> <55AAFF96-F751-4A01-BE3E-280A438A55DC@exmail.nottingham.ac.uk> From: Andrej Bauer Date: Wed, 20 Dec 2017 01:14:26 +0100 Message-ID: Subject: Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent? To: Steve Awodey Cc: Homotopy Type Theory Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable > If this is supposed to be subobject classification in the sense of an ele= mentary topos, > then the p=E2=80=99s that =E2=80=9Ccorrespond to" isomorphic h-props stil= l need to be identified. > That=E2=80=99s univalence for Omega, of course, which does indeed hold in= a topos. Isn't Thomas's point that the p's that correspond to isomorphic h-props are *equal*, and that there is only one reasonable notion of equality in a topos, which is extensional equality? With kind regards, Andrej