From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:a54:4187:: with SMTP id 7mr17250993oiy.40.1589128261437; Sun, 10 May 2020 09:31:01 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a05:6820:13c:: with SMTP id i28ls448449ood.6.gmail; Sun, 10 May 2020 09:31:00 -0700 (PDT) X-Received: by 2002:a4a:a50e:: with SMTP id v14mr10444016ook.27.1589128260163; Sun, 10 May 2020 09:31:00 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1589128260; cv=none; d=google.com; s=arc-20160816; b=JAtUQ1kFShO8iFztXIqDapnr6F8fSbdshlFURDeodZTEWMLmFnPZtzAorlWgYpOsAi p/8U43DJS4vcFTZFo0ZwO13f5S+x4NHGecDrIGcDXstnpl9GXbH1xN9aj/SPXXlJcFT+ 90efHH5rEyKFYsXRljy2+gHdHu89Xxs571RRtcGodGfKU4eZ8F0hiIBBj5Y3wTOUeHX1 BaeT3b3zbAdqAPse+Ba6c+UesXveFnIzWMnH2VpFQIUdtdVYHdud6id5HsTIQtpGuTVT 7Sxsk6jALA5I7jRLvC+ILnUUzAbkwxwLDgKj6L2gumk8t8YVUskOOX9hH0na5zHEfXvA rorQ== 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=tSFoeadFbOIcyu096xd5OzxzQAaw5wtaKMcUSq37xGA=; b=k2KQe9DL9TgyvMxkjNtbNqs7zYXSlovy3QnMocZwPQotIaNxljcEf0wGJhqcYhIcVo MN+j5cPAD4Nki5I4SGyTRixS7/nAFDVOPsLxJdITdT72iHOx4qVe+lRizFuwmC3Oqxz2 uwuE3WpvZ3W3nCq8yFcLcEPkZyEI1Z/G8xuRdpych/xq9JiGNO/oY1jcYiuFTS0OyJM2 guIQgFq+4y6nu5wUOY5uz7JhV1JY+6UmaEYU27W/FkCqsO2vhac+maBj+Adsk3GKLVqi R3O3hQnwFZZqxWBVippgJ6CP46f49OaG3rwMkFI/ZqJJMkjAZCuaFkIXmXapGQzsU2ei sAng== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=FHvsU4T2; spf=pass (google.com: domain of shu...@sandiego.edu designates 2607:f8b0:4864:20::22a 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-x22a.google.com (mail-oi1-x22a.google.com. [2607:f8b0:4864:20::22a]) by gmr-mx.google.com with ESMTPS id f197si65518oob.1.2020.05.10.09.31.00 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Sun, 10 May 2020 09:31:00 -0700 (PDT) Received-SPF: pass (google.com: domain of shu...@sandiego.edu designates 2607:f8b0:4864:20::22a as permitted sender) client-ip=2607:f8b0:4864:20::22a; Authentication-Results: gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=FHvsU4T2; spf=pass (google.com: domain of shu...@sandiego.edu designates 2607:f8b0:4864:20::22a as permitted sender) smtp.mailfrom=shu...@sandiego.edu; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=sandiego.edu Received: by mail-oi1-x22a.google.com with SMTP id b18so13073090oic.6 for ; Sun, 10 May 2020 09:31:00 -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=tSFoeadFbOIcyu096xd5OzxzQAaw5wtaKMcUSq37xGA=; b=FHvsU4T2ckZEUMpcHHKbDCGMgvjy1CRV7WMVTKggsXp5sm40c75FptrSHSHN/fg4kV SQ+8cuhwk9MiE1kNNTvAK4XPHmfVoYJFcJ4yWXX43pfi7QJ/rmYdT8xCcw3aCus//FJa LJWjaWzkG37k/EP05i5RLvcsMisQNOr3M7OTOq3QSZxYQJy3SnwP9Lr7W18Q1RMfnfED 4I2BCAPG5CegDNM+mjMcIcz7EU5GKYu2MfuFxAn3z5bUroBu+/EfkH2rVubxB505jQos Xa55tb+G5C8E85HmFsK3oZEG0fb/eDl7EfhQwiEh0tQ9s7zQQ8LleoQRxNxEp559kfhI iUGw== X-Gm-Message-State: AGi0Pub78wUHUsN/PwJRS8JqX7SkPDk4bGNgUMuT7RWsJ7v/7FlWOkb9 a/DH8lzsmanZ07kBe9lAU9+0CskPFDOm9LfAwD58Zoa8EMgDFWFxGQMl5mJrsZH/J4rbvm3Kuwa wZWh9ezOyD5bHtQfICI7TXdWhocnIxLX/u1HNiYRCLcLgaSiJPLPd72SrBQpBaV7xJ+PfmYStBh w3e9ooJqxy X-Received: by 2002:a54:4601:: with SMTP id p1mr15176780oip.173.1589128259681; Sun, 10 May 2020 09:30:59 -0700 (PDT) Return-Path: Received: from mail-oo1-f46.google.com (mail-oo1-f46.google.com. [209.85.161.46]) by smtp.gmail.com with ESMTPSA id s69sm2006814otb.4.2020.05.10.09.30.59 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Sun, 10 May 2020 09:30:59 -0700 (PDT) Received: by mail-oo1-f46.google.com with SMTP id v6so1432429oou.4 for ; Sun, 10 May 2020 09:30:59 -0700 (PDT) X-Received: by 2002:a4a:9442:: with SMTP id j2mr10597242ooi.37.1589128258869; Sun, 10 May 2020 09:30:58 -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> <7b9eb7c9-040a-46e8-b470-28958f8d7713@googlegroups.com> In-Reply-To: <7b9eb7c9-040a-46e8-b470-28958f8d7713@googlegroups.com> From: Michael Shulman Date: Sun, 10 May 2020 09:30:46 -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 I realize this may be controversial too, but I think there's at least one sense in which sets are "more fundamental", namely that ordinary syntax consists of sets, because it is a (non-higher) inductive type. I think this is kind of the "reason" for the conservativity theorem. I don't think this fact detracts from the importance and independence of the homotopical point of view, any more than the fact that (say) finite sets have decidable equality detracts from the importance of constructivism. It's just the fact that simpler things are simpler. On Sun, May 10, 2020 at 8:35 AM Ulrik Buchholtz wrote: > > On Sunday, May 10, 2020 at 4:27:30 PM UTC+2, Nicolai Kraus wrote: >> >> I agree with Mike - sorry Ulrik :-) >> For me, "everything is based on sets" would mean that every fibrant type= can be written as the realization of a (semi-) simplicial type, or somethi= ng like this. > > > No need to apologize: I know I was being slightly provocative by juxtapos= ing a question about sets cover (SC) and a comment on 2-level type theory i= n this context, in order to provoke some discussion :-) > > Wouldn't you agree, however, that even though basic 2LTT is conservative = over HoTT, from a certain point of view, 2LTT privileges the =E2=80=9Cgroun= d floor=E2=80=9D exosets? In your very nice paper, https://arxiv.org/abs/17= 05.03307, you decorate the inner (fibrant, endo-) types as special, and lea= ve the exotypes undecorated, privileging the latter. While from a user's pe= rspective, however, it's the (inner) types that are standard/mathematical, = and the exotypes that are special. > > And regardless of the decorations, the mere fact that we bring in the exo= set level makes the theory harder to justify from the philosophical positio= n that general homotopy types are not reducible to sets. One can in fact se= e the conservativity result as foundational reduction (in the sense of http= s://math.stanford.edu/~feferman/papers/reductive.pdf section 5) from a syst= em justified by the principle that everything is based on sets to a system = justified by a framework where that isn't the case. > > Another connection is that it seems it should be easier to find an axiom,= which might imply SC, that would allow us to construct the type of semi-si= mplicial types, rather than such an axiom that doesn't imply SC. But I don'= t know any such axiom statable in book HoTT either way. > > BTW, you probably meant =E2=80=9Csimplicial set=E2=80=9D above. And yes, = that kind of axiom would be the strongest expression of =E2=80=9Ceverything= is based sets=E2=80=9D, and it currently needs 2LTT to even be stated. > > Cheers, > Ulrik > > -- > You received this message because you are subscribed to the Google Groups= "Homotopy Type Theory" group. > To unsubscribe from this group and stop receiving emails from it, send an= email to HomotopyT...@googlegroups.com. > To view this discussion on the web visit https://groups.google.com/d/msgi= d/HomotopyTypeTheory/7b9eb7c9-040a-46e8-b470-28958f8d7713%40googlegroups.co= m.