From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:a17:90a:a796:: with SMTP id f22mr15969996pjq.42.1589119277014; Sun, 10 May 2020 07:01:17 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a17:902:8f8f:: with SMTP id z15ls3892883plo.8.gmail; Sun, 10 May 2020 07:01:15 -0700 (PDT) X-Received: by 2002:a17:902:9044:: with SMTP id w4mr11359800plz.83.1589119275200; Sun, 10 May 2020 07:01:15 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1589119275; cv=none; d=google.com; s=arc-20160816; b=OSAu8pWIB4L2eyJCQL6lKPBq1IRLMIEeqjgNJ3yO5MSq/yT98mEqgdfkuXcJAvFOvu GRlJ1GWk//KIGBfLCWkAet7Ot9NgNrz7olyKHge2gYCbpZbiNtifFHB6NHmqltknhgiL s4jeBMPBbazwWuPpTKlD1w+zR4jrmSKbcGttxcQa5S/Fta0CUFxngZjroi58t/8GGPUo yCe9HPyLmawrFQDea77rvr6I0PLY6nxPOd9ctnF9L7htM2FVo8F587uU8E1tmkDr8DV+ onlrOPmNG1ONUpQoEwxXnYHIr7/6VbhExVTZmieFps9kavlNjl1gwLlUzhV7swMULDij +C9w== 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 :in-reply-to:references:mime-version:dkim-signature; bh=CLZxw+0TwtcZfuvyOCLsFPQNRxBlTh3Ejh2Lrw2bgMc=; b=RZjpDU0GPmVDlmUs8TcRKn8xoyj8vBeSG4xaObeoJPkf86C5buVC/7LwtMwbnsFNxN revo4fCz79RRLUWmeoCTdsIGIcrQRP41cMMAYtBzDJDBPn2vAR0TYUtig6Zxt0baL3Y0 WMtVt7PRW9ZP/pDCvbdcfdQ+KmmeDgYe5FHnNvLCNo1Vm18iTYc8MibGfDnyQwOmaq4h DVCDeinzEkz/VRD3HCbW8IEaycohK+sDJGUrj10mT32nVESByfPCKSc18zFDOvl0mek4 qp+aGgsp2FkcvjkSIgAoBoSTp0FiMysNXaphtjjFZxdnQSDjghxaNwdMaGe3zpj/3RpU E0mA== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=TwRW8tMv; spf=pass (google.com: domain of shu...@sandiego.edu designates 2607:f8b0:4864:20::229 as permitted sender) smtp.mailfrom=shu...@sandiego.edu; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=sandiego.edu Return-Path: Received: from mail-oi1-x229.google.com (mail-oi1-x229.google.com. [2607:f8b0:4864:20::229]) by gmr-mx.google.com with ESMTPS id bi9si509183plb.3.2020.05.10.07.01.15 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Sun, 10 May 2020 07:01:15 -0700 (PDT) Received-SPF: pass (google.com: domain of shu...@sandiego.edu designates 2607:f8b0:4864:20::229 as permitted sender) client-ip=2607:f8b0:4864:20::229; Authentication-Results: gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=TwRW8tMv; spf=pass (google.com: domain of shu...@sandiego.edu designates 2607:f8b0:4864:20::229 as permitted sender) smtp.mailfrom=shu...@sandiego.edu; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=sandiego.edu Received: by mail-oi1-x229.google.com with SMTP id c12so11846183oic.1 for ; Sun, 10 May 2020 07:01:15 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=sandiego-edu.20150623.gappssmtp.com; s=20150623; h=mime-version:references:in-reply-to:from:date:message-id:subject:to :cc:content-transfer-encoding; bh=CLZxw+0TwtcZfuvyOCLsFPQNRxBlTh3Ejh2Lrw2bgMc=; b=TwRW8tMvwDvWnhB2K+BlZSyUWe3nGgppAFU004o3A+oeeN54o5/5GBCTdsKr8kQuee ncdDXht0AUXnpVdRzUv8PX1ediArXn1KxEw/JS7URR8QAlVQBCwHQrEF31duw1zSXgyR WRehTkErzE+KZf77OkLmdRSkBZucBHMrlEoHkH3Frme8dCIWjwqL3fGLA4vOsYCpW4V1 vdSlwr79ewtx12zi4FCOw/RIeEEQcEPL+ghZO3yXsUyprSI6Wp8wX9mp1HHoveTfQCcW fNuRIUxYPT8AftDwTDTFlqdFgHKbj5CYOB8XquOCLzg9hOi9bZX83LLE88WAkXWReySF M5SQ== X-Gm-Message-State: AGi0PuYybvdiA0CK20MBdrKn/cCDlfP4roEBWK6BAGWXRhyV4iNPD+B5 yCnx9qpVCaOAyeqmnvo0h/8Sxx/lrQp0VFexsRi4Ed1pH5d2JKKQs6LtGK5AlY7nkSLYRW7RFjG 8hoSvfNsgO6Zcz73G3YmwByHHBX4LXnRjZBnMLC4fxQSwm1MjLjcQwCoMcqV4LDvvbvmILmYqcc v+WLKxUsQl X-Received: by 2002:aca:1811:: with SMTP id h17mr3972068oih.87.1589119274627; Sun, 10 May 2020 07:01:14 -0700 (PDT) Return-Path: Received: from mail-oi1-f169.google.com (mail-oi1-f169.google.com. [209.85.167.169]) by smtp.gmail.com with ESMTPSA id 60sm1927564oth.38.2020.05.10.07.01.13 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Sun, 10 May 2020 07:01:13 -0700 (PDT) Received: by mail-oi1-f169.google.com with SMTP id a2so12644646oia.11 for ; Sun, 10 May 2020 07:01:13 -0700 (PDT) X-Received: by 2002:aca:f541:: with SMTP id t62mr16120780oih.148.1589119272764; Sun, 10 May 2020 07:01:12 -0700 (PDT) MIME-Version: 1.0 References: <67E9DCCA-F9CA-45B7-9AC8-E5A7E94FE9A9@nottingham.ac.uk> <20200507100930.GA9390@mathematik.tu-darmstadt.de> <8C57894C7413F04A98DDF5629FEC90B1652F5334@Pli.gst.uqam.ca> <8C57894C7413F04A98DDF5629FEC90B1652F53A3@Pli.gst.uqam.ca> <20200508064039.GC21473@mathematik.tu-darmstadt.de> <8C57894C7413F04A98DDF5629FEC90B1652F54CC@Pli.gst.uqam.ca> <20200509082829.GA8417@mathematik.tu-darmstadt.de> <8C57894C7413F04A98DDF5629FEC90B1652F55C8@Pli.gst.uqam.ca> <20200509184313.GB28841@mathematik.tu-darmstadt.de> <8C57894C7413F04A98DDF5629FEC90B1652F563A@Pli.gst.uqam.ca> In-Reply-To: From: Michael Shulman Date: Sun, 10 May 2020 07:01:00 -0700 X-Gmail-Original-Message-ID: Message-ID: Subject: Re: [HoTT] Identity versus equality To: Ulrik Buchholtz Cc: Homotopy Type Theory Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable On Sun, May 10, 2020 at 5:53 AM Ulrik Buchholtz wrote: > What HoTT/UF offers us is another axis of foundational variation, besides= the old classical/constructive, impredicative/predicative, infinitist/fini= tist, namely: everything is based on sets/general homotopy types are not re= ducible to sets. Exactly! > A question: Recall that if we assume the axiom of choice (AC) for sets, t= hen there is a surjection from a set onto Set, namely the map that takes a = cardinal (or ordinal) to the set of ordinals below it. > Is there (with AC for sets) also a surjection from a set to the type of 1= -types? To the full universe? As far as I know, it is an open question whether AC for sets implies these stronger principles (although I'd be surprised if it were true). Those principles are true, of course, in the model of simplicial sets based on ZFC, and there are models in which they fail, but I don't know of a model in which they fail but AC for sets holds. Although I don't think I've really tried to look for one either; has anyone? There is however the theorem stated at https://ncatlab.org/nlab/show/n-types+cover#relation_to_other_axioms, that AC for sets together with the axiom "every type is surjected onto by a set" is equivalent to the "oo-AC" that "every surjection onto a set has a section". > The 2-level type theories can be viewed as another way of making a type t= heory that is faithful to the idea that everything is based on sets. While I kind of see how one could say this, I think it's misleading especially in light of the above dichotomy, becuase 2LTT doesn't imply any of the *internal* "types are based on sets" axioms for the fibrant layer. As you know, 2LTT without additional axioms is conservative over HoTT, while even with stronger axioms it can still be modeled in many or all higher toposes. > I like to think of the outer layer as an exoskeleton for type theory, giv= ing it a bit of extra strength while we don't know how to use its own power= s fully, or whether indeed it is strong enough to effect constructions like= that of simplicial types. Every type (which for me is a fibrant type, sinc= e that's the mathematically meaningful ones) has a corresponding exotype (i= ndeed an exoset), but there are more exotypes, such as the exonatural numbe= rs, which are sometimes useful. I think "exo-" is a great prefix for the outer layer!