From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on inbox.vuxu.org X-Spam-Level: X-Spam-Status: No, score=-1.1 required=5.0 tests=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_AU,FREEMAIL_FROM,HTML_MESSAGE,MAILING_LIST_MULTI, RCVD_IN_DNSWL_NONE,T_SCC_BODY_TEXT_LINE autolearn=ham autolearn_force=no version=3.4.4 Received: (qmail 10040 invoked from network); 29 Apr 2023 18:49:50 -0000 Received: from mail-lj1-x23a.google.com (2a00:1450:4864:20::23a) by inbox.vuxu.org with ESMTPUTF8; 29 Apr 2023 18:49:50 -0000 Received: by mail-lj1-x23a.google.com with SMTP id 38308e7fff4ca-2a8b52c112fsf3959091fa.0 for ; Sat, 29 Apr 2023 11:49:50 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1682794189; cv=pass; d=google.com; s=arc-20160816; b=bt7cP7JzmEdTPptVwF0NkjZfU0V3fDUQP8bjBFPe4Aq8vGlxWUmeEnY6H0qPPIBc+y voK6NSM9OTX04bEs//cLQ7QxsMbNc0tnZM3K5tpKp7pVfyqdwn4fZGvSkerbDqgK/iuD 6/20dkhDbb+iW1i+lYpUpETShrW/hkjTogVgH6PPwsAmH67ryvMRNE/kY0PLPqxZnkMF gtc6C+p92iytImfvDMiMl1KZNK7QHk7YPAZhLU02Dz1Fw+nwiP6lrySLLo33csNu+pwO j89d7T7xDDiN1A7M8566hMtjWfhA28FaDYa2ErGoG7pcNjBAXnThnxAWyCNHf5Nxcm82 YuRA== ARC-Message-Signature: i=2; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=list-unsubscribe:list-subscribe:list-archive:list-help:list-post :list-id:mailing-list:precedence:cc:to:subject:message-id:date:from :in-reply-to:references:mime-version:sender:dkim-signature :dkim-signature; bh=Mi9/zcnRCJLQkwfNZk4n14Q1KYhXuMmy87fO05uGmDg=; b=PPC0l3XUPTV5hu+xTeXk6b0ngY7/QOOC9ZqRwse7hZg6amR0ISIbPmgGI5MaRFgGVB h6cY8tOZJ4Tmr5x0Pu2oQIm7r2Y9L7R/UQQ8t6SKmgPAMD1HobH2+TD6NmkbSwxFsOqJ BmHDr8eiYrei+jefvI3tuacq9R+aLfruyDiXYkDGSsxywGqjH1DHLmzN5HgXYjN/zKAL iaud23OzfrQWybTXW3ZccyiowCS7wtf/q1SOhqlD/DHaaBeVWtucPbg1piM411ahc8NY Qp4PROapRcP32871Or9HjRcAHUiGri9yMpKd2whOXAubtAe2Ax4Nad/4rRh6mEB7a95X P7ug== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20221208 header.b=Ur+TpV54; spf=pass (google.com: domain of ulrikbuchholtz@gmail.com designates 2a00:1450:4864:20::12f as permitted sender) smtp.mailfrom=ulrikbuchholtz@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20221208; t=1682794189; x=1685386189; h=list-unsubscribe:list-subscribe:list-archive:list-help:list-post :list-id:mailing-list:precedence:x-original-authentication-results :x-original-sender:cc:to:subject:message-id:date:from:in-reply-to :references:mime-version:sender:from:to:cc:subject:date:message-id :reply-to; bh=Mi9/zcnRCJLQkwfNZk4n14Q1KYhXuMmy87fO05uGmDg=; b=BBYctto7k252KJcjUCjzm+7WkwSDDC8nr+Kk/h3ssVw8JniskrG2dsSjzxUXfPXbUe 2yi6KFTG1GNxE5APAmU9kTEeYDFuH9cUsI8OP56iESV0RFzG55SzOtTqC0bpqoeG30Gz g/O0wYd75Bts9M2jZVtYuw3qUn7MNy5Te78yKFlYjEUk57IeZav/A5iFmXSJGUFtW4Ao K9O/EDshpFjo7F1Wrl8C6Thg0PeRdLigNkv/6JHOTpvKVqv3o0gO1Hn2EEjhWSfpr1so VtBYB9QoF5U3W3nsHFTx39dkQUVixxFtUFERUJala6iZmwxXqBo9lm7U6pWtqnquT1Dd 7P8A== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20221208; t=1682794189; x=1685386189; h=list-unsubscribe:list-subscribe:list-archive:list-help:list-post :list-id:mailing-list:precedence:x-original-authentication-results :x-original-sender:cc:to:subject:message-id:date:from:in-reply-to :references:mime-version:from:to:cc:subject:date:message-id:reply-to; bh=Mi9/zcnRCJLQkwfNZk4n14Q1KYhXuMmy87fO05uGmDg=; b=VWRyJjEdc22p+vNHi17/FGNANu5ohxXLSBlm/r99BNDd/szUY+hhIx5x3FB1JhEIr6 SrM2GDQp+GNVZLHwFGTxVgrsHKYESqdGiRLNh8QcORrtou+wRGnhtxVKeVQqDJetJYEK bmrc2/bbppXX6xIX4jcYlZQf9OcBCJvrIhLfiqJ1LQUD84AA5A7/r9k95c4xR8Xa9hVK lVUF0K1NCI5dVvI5HewqfF8B2WE/yitdTI4kNKcIoGQTrkVQdbEzF8i+MAEFP/YNxEIj l+0X5lehcph3bki+M8kcox4G3SSelZL2n5tkGGtiS4QLCTwSTgAU+oorkgZL8Wq6RXhY p9vw== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20221208; t=1682794189; x=1685386189; h=list-unsubscribe:list-subscribe:list-archive:list-help:list-post :x-spam-checked-in-group:list-id:mailing-list:precedence :x-original-authentication-results:x-original-sender:cc:to:subject :message-id:date:from:in-reply-to:references:mime-version :x-beenthere:x-gm-message-state:sender:from:to:cc:subject:date :message-id:reply-to; bh=Mi9/zcnRCJLQkwfNZk4n14Q1KYhXuMmy87fO05uGmDg=; b=Y5O51Lcge79MDMbvDOvh/o+cmDcuJYxLKIO0o/HZDzdaTgv0XCD8ZnP+hK5R6fbMJt v7gigHHdduDaPrVwHd1Jr93eihqeUliPi6QcJ9Rphq1erSfGSWeK8MbfYrvk1v9zDjNu /huK4wKnWVp5i8jiowvqpc8c3hpaKgmz9YS6yV6M2/IeR6ra/DlwOL3aIAFcEdipMBNc kN6u1xoDkIyQz+FHZoA5I0r9jVgc6MvtanD7k39/dkjNXYcBfHyFBJFxY9Q6yLrLRYta Ezmt4xaNn5VNmredachlJPQIQXnRipnvhnHcuaBQYfwpTvpw3ZYh2oQntcWPt4UshtEt 0GdQ== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AC+VfDyUugIqOWMx4JEOvLaEXcVlSLkeby9JYOUAsOWr1Qf95f21QHQJ C4diggsLjiD/DFf+kVxBpD8= X-Google-Smtp-Source: ACHHUZ6sjbnMSpMK+3LkY++iM4AIez4ayAwW7csaxeE/6FvapKnxrceumbxQyQkYzjsplB5uapAhsg== X-Received: by 2002:a2e:3e15:0:b0:2a5:fe8f:b314 with SMTP id l21-20020a2e3e15000000b002a5fe8fb314mr2056254lja.5.1682794189444; Sat, 29 Apr 2023 11:49:49 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a05:6512:110f:b0:4e8:c8b4:347a with SMTP id l15-20020a056512110f00b004e8c8b4347als58606lfg.1.-pod-prod-gmail; Sat, 29 Apr 2023 11:49:46 -0700 (PDT) X-Received: by 2002:ac2:5e8f:0:b0:4ec:a9c5:f3ae with SMTP id b15-20020ac25e8f000000b004eca9c5f3aemr2469942lfq.11.1682794186690; Sat, 29 Apr 2023 11:49:46 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1682794186; cv=none; d=google.com; s=arc-20160816; b=uGodSBnTW7iJ++TztA8++SSZ0Q0WtBS6vHNqSe/szWsJCWSh3Pl6Y1AmpMp3XoGzD5 Mov0unrWxq2Dihaf0AqHGS4kSCZRGgqfI7O/VMhZe/tezG09YZ7pxMo3PyMLFvQpbdwx cvq2cfR0jaC8I7JEjLlrRJCPNGdMY9ykwvwD8iqhawVdlQ24QaW6ge4NENc21mL++oMk pcTUSj/COKHZ34+TFXiVjyUN3RjeH8u2mH++fmgd/NTP+b0wRA3Hlzso/Gzo+9hYeNtO WYPNpL3CTD1leza5dqMrPDw8Sh3q4x+N+NVml0PF9odqdTi7/h2FotSdLRaARpCa+qez dtVQ== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=cc:to:subject:message-id:date:from:in-reply-to:references :mime-version:dkim-signature; bh=xUcx4iaJ1we9Wh29dGcqlmE6FO1zB3gn1uddogDQ038=; b=ja3C1QxCCuy75bNbEqPg8usSFdW+VtyBkQvxOWcdJtD6gAwL+mB8Dd/OnznLR9uY+L o3/7l2Nx/3vLAAC62wxWtqV+rXzBcJEAJ+5XXlW8WELtKEGaXnXjIt+5wMj9JMdayaJl SBzBFPvXhuV4yY4XMrbnlQhzfzxBwa0Cd0km4V+O5pF5AU1w9khM+Vy3rMJ4B7/rHJ22 zOgpEpR2sfs7KzI3zWCv8jH4VlX4Rz2AdT73QHLduANUpFuO7CqOa2zYylMFk8Rmr3A/ HgGe+CbTH2a+o3xVzenBwceF/M09yCskQvOpXwzogyjhBB9YFKsuxOWN5Nrmkz1yfuJF +siA== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20221208 header.b=Ur+TpV54; spf=pass (google.com: domain of ulrikbuchholtz@gmail.com designates 2a00:1450:4864:20::12f as permitted sender) smtp.mailfrom=ulrikbuchholtz@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-lf1-x12f.google.com (mail-lf1-x12f.google.com. [2a00:1450:4864:20::12f]) by gmr-mx.google.com with ESMTPS id k19-20020a0565123d9300b004edc2bbd25bsi1656837lfv.3.2023.04.29.11.49.46 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Sat, 29 Apr 2023 11:49:46 -0700 (PDT) Received-SPF: pass (google.com: domain of ulrikbuchholtz@gmail.com designates 2a00:1450:4864:20::12f as permitted sender) client-ip=2a00:1450:4864:20::12f; Received: by mail-lf1-x12f.google.com with SMTP id 2adb3069b0e04-4ec9c7c6986so1401449e87.0 for ; Sat, 29 Apr 2023 11:49:46 -0700 (PDT) X-Received: by 2002:a2e:97c4:0:b0:2a8:ca28:e4e with SMTP id m4-20020a2e97c4000000b002a8ca280e4emr2636320ljj.24.1682794186009; Sat, 29 Apr 2023 11:49:46 -0700 (PDT) MIME-Version: 1.0 References: <87leigyeya.fsf@uwo.ca> <87zg6qy4gx.fsf@uwo.ca> <21ED9406-6C3A-4B26-A74B-34C2821C97B6@gmail.com> In-Reply-To: <21ED9406-6C3A-4B26-A74B-34C2821C97B6@gmail.com> From: Ulrik Buchholtz Date: Sat, 29 Apr 2023 19:49:34 +0100 Message-ID: Subject: Re: [HoTT] Free higher groups To: Steve Awodey Cc: Dan Christensen , "homotopytypetheory@googlegroups.com" Content-Type: multipart/alternative; boundary="000000000000aff1cb05fa7e0ddd" X-Original-Sender: UlrikBuchholtz@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20221208 header.b=Ur+TpV54; spf=pass (google.com: domain of ulrikbuchholtz@gmail.com designates 2a00:1450:4864:20::12f as permitted sender) smtp.mailfrom=ulrikbuchholtz@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Precedence: list Mailing-list: list HomotopyTypeTheory@googlegroups.com; contact HomotopyTypeTheory+owners@googlegroups.com List-ID: X-Google-Group-Id: 1041266174716 List-Post: , List-Help: , List-Archive: , List-Unsubscribe: , --000000000000aff1cb05fa7e0ddd Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable > How about just covering a type by a 0-type? > We have countermodels for this, see: https://ncatlab.org/nlab/show/n-types+cover#InModels A question that came up for me recently is whether we can construct the modality for which the acyclic maps are the left class. (This exists in every Grothendieck higher topos. In infinity groupoids, and many, but not all, models, the right class are the hypoabelian maps.) Then there's the question whether every simply connected acyclic type is contractible. (This is open for Grothendieck higher toposes, AFAIK.) These are mentioned in the talk I mentioned up-thread, which also contained the short new proof that the Higman group presentation is non-trivial and aspherical (as well as acyclic). The slides are here: https://ulrikbuchholtz.dk/hott-uf-2023.pdf Cheers, Ulrik > Steve > > > > On Apr 29, 2023, at 1:37 PM, Dan Christensen wrote: > > > > Another set-level statement is whether there are enough injective > > abelian groups. It's true in Grothendieck oo-toposes, but presumably i= s > > not provable in HoTT. > > > > Dan > > > > On Apr 28, 2023, Michael Shulman wrote: > > > >> The existence of hypercompletion is a good suggestion. > >> > >> Also I realized there are set-level statements that are already known > to be > >> true in all Grothendieck 1-toposes but not all elementary 1-toposes, > such as > >> WISC and Freyd's theorem that a small complete category is a preorder. > So > >> those will be true in any Grothendieck oo-topos too, and can be > presumed to > >> fail in HoTT. But it's nice to have one that involves higher types to= o. > >> > >> On Mon, Apr 24, 2023 at 5:37=E2=80=AFPM Dan Christensen w= rote: > >> > >> A not-so-interesting answer to Mike's question is the type of deloopin= gs > >> of S^3. The reason this isn't so interesting is that it's in the imag= e > >> of the natural functor from Spaces to any oo-topos, so it's true just > >> because it is true for Spaces. Similarly, a statement asserting that > >> pi_42(S^17) =3D (insert what it is) is true in any oo-topos. Another > >> reason these aren't interesting is that I expect that they are provabl= e > >> in HoTT with enough work. > >> > >> So, I'll second Mike's question, with the extra condition that it woul= d > >> be good to have a type for which there is some reason to doubt that it > >> is provably inhabited in HoTT. > >> > >> Oh, what about whether the hypercomplete objects are the modal > >> objects > >> for a modality? I'm throwing this out there without much thought... > >> > >> Dan > >> > >> On Apr 24, 2023, Michael Shulman wrote: > >> > >>> This is fantastic, especially the simplicity of the construction. As > >>> Peter said, a wonderful way to commemorate the 10th anniversary of > >> the > >>> special year and the release of the HoTT Book. > >>> > >>> Relatedly to Nicolai's question, this question also has an easy proof > >>> in any Grothendieck infinity-topos. Now that we know it also has a > >>> proof in HoTT, do we know of any type in HoTT whose interpretation in > >>> any Grothendieck infinity-topos is known to be inhabited, but which > >>> isn't known to be inhabited in HoTT? > >>> > >>> On Fri, Apr 21, 2023 at 5:25=E2=80=AFPM Nicolai Kraus > >>> wrote: > >>> > >>> Hi David, > >>> > >>> Congratulations (again)! I find it very interesting that this > >>> question has a positive answer. I had suspected that it might > >>> separate HoTT from Voevodsky's HTS (aka 2LTT with a fibrancy > >>> assumption on strict Nat). Since this isn't the case, do we know > >>> of another type in HoTT that is inhabited in HTS, while we don't > >>> know whether we can construct an inhabitant in HoTT? > >>> > >>> Best, > >>> Nicolai > >>> > >>> On Fri, Apr 21, 2023 at 8:30=E2=80=AFPM Jon Sterling > >>> wrote: > >>> > >>> Dear David, > >>> > >>> Congratulations on your beautiful result; I'm looking forward > >>> to understanding the details. Recently I had been wondering if > >>> anyone had proved this, and I am delighted to see that it is > >>> now done. > >>> > >>> Best wishes, > >>> Jon > >>> > >>> On 21 Apr 2023, at 12:04, David W=C3=A4rn wrote: > >>> > >>>> Dear all, > >>>> > >>>> I'm happy to announce a solution to one of the oldest open > >>> problems in synthetic homotopy theory: the free higher group > >>> on a set is a set. > >>>> > >>>> The proof proceeds by describing path types of pushouts as > >>> sequential colimits of pushouts, much like the James > >>> construction. This description should be useful also in many > >>> other applications. For example it gives a straightforward > >>> proof of Blakers-Massey. > >>>> > >>>> Best wishes, > >>>> David > >>>> > >>>> -- > >>>> 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 > >>> HomotopyTypeTheory+unsubscribe@googlegroups.com. > >>>> To view this discussion on the web visit > >>> > >> > https://groups.google.com/d/msgid/HomotopyTypeTheory/f2af459c-53a6-e7b9-7= 7db-5cbf56da17f3%40gmail.com > . > >> > >>> > >>> -- > >>> 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 > >>> HomotopyTypeTheory+unsubscribe@googlegroups.com. > >>> To view this discussion on the web visit > >>> > >> > https://groups.google.com/d/msgid/HomotopyTypeTheory/D102F774-D134-46B9-A= 70A-51CB84BE4B6F%40jonmsterling.com > . > >> > >>> > >>> -- > >>> 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 > >> HomotopyTypeTheory+unsubscribe@googlegroups.com. > >>> To view this discussion on the web visit > >>> > >> > https://groups.google.com/d/msgid/HomotopyTypeTheory/CA%2BAZBBpPwgh1G9VZV= 0fgJFd8Mzqfchskc4-%2B-FXT42WQkzmC9w%40mail.gmail.com > . > >> > >> -- > >> 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 HomotopyTypeTheory+unsubscribe@googlegroups.com. > >> To view this discussion on the web visit > >> > https://groups.google.com/d/msgid/HomotopyTypeTheory/87leigyeya.fsf%40uwo= .ca > . > > > > -- > > 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 HomotopyTypeTheory+unsubscribe@googlegroups.com. > > To view this discussion on the web visit > https://groups.google.com/d/msgid/HomotopyTypeTheory/87zg6qy4gx.fsf%40uwo= .ca > . > > -- > 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 HomotopyTypeTheory+unsubscribe@googlegroups.com. > To view this discussion on the web visit > https://groups.google.com/d/msgid/HomotopyTypeTheory/21ED9406-6C3A-4B26-A= 74B-34C2821C97B6%40gmail.com > . > --=20 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 e= mail to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/= HomotopyTypeTheory/CAE-BQ1zWQHqUv9woQPw75Sqz1c7_M9F-nzX3RYYmXAxVxy8skQ%40ma= il.gmail.com. --000000000000aff1cb05fa7e0ddd Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
How about just covering a type by a 0-type?

=
We have countermodels for this, see: https://ncatlab.org/nlab/show/n-types+cover= #InModels

A question that came up for me recen= tly is whether we can construct the modality for which the acyclic maps are= the left class. (This exists in every Grothendieck higher topos. In infini= ty groupoids, and many, but not all, models, the right class are the hypoab= elian maps.)

Then there's the question whether= every simply connected acyclic type is contractible. (This is open for Gro= thendieck higher toposes, AFAIK.)

These are mentio= ned in the talk I mentioned up-thread, which also contained the short new p= roof that the Higman group presentation is non-trivial and aspherical (as w= ell as acyclic). The slides are here: https://ulrikbuchholtz.dk/hott-uf-2023.pdf
=
Cheers,
Ulrik


Steve


> On Apr 29, 2023, at 1:37 PM, Dan Christensen <jdc@uwo.ca> wrote:
>
> Another set-level statement is whether there are enough injective
> abelian groups.=C2=A0 It's true in Grothendieck oo-toposes, but pr= esumably is
> not provable in HoTT.
>
> Dan
>
> On Apr 28, 2023, Michael Shulman <shulman@sandiego.edu> wrote:
>
>> The existence of hypercompletion is a good suggestion.
>>
>> Also I realized there are set-level statements that are already kn= own to be
>> true in all Grothendieck 1-toposes but not all elementary 1-topose= s, such as
>> WISC and Freyd's theorem that a small complete category is a p= reorder.=C2=A0 So
>> those will be true in any Grothendieck oo-topos too, and can be pr= esumed to
>> fail in HoTT.=C2=A0 But it's nice to have one that involves hi= gher types too.
>>
>> On Mon, Apr 24, 2023 at 5:37=E2=80=AFPM Dan Christensen <jdc@uwo.ca> wrote:
>>
>> A not-so-interesting answer to Mike's question is the type of = deloopings
>> of S^3.=C2=A0 The reason this isn't so interesting is that it&= #39;s in the image
>> of the natural functor from Spaces to any oo-topos, so it's tr= ue just
>> because it is true for Spaces.=C2=A0 Similarly, a statement assert= ing that
>> pi_42(S^17) =3D (insert what it is) is true in any oo-topos.=C2=A0= Another
>> reason these aren't interesting is that I expect that they are= provable
>> in HoTT with enough work.
>>
>> So, I'll second Mike's question, with the extra condition = that it would
>> be good to have a type for which there is some reason to doubt tha= t it
>> is provably inhabited in HoTT.
>>
>> Oh, what about whether the hypercomplete objects are the modal
>> objects
>> for a modality?=C2=A0 I'm throwing this out there without much= thought...
>>
>> Dan
>>
>> On Apr 24, 2023, Michael Shulman <shulman@sandiego.edu> wrote:
>>
>>> This is fantastic, especially the simplicity of the constructi= on.=C2=A0 As
>>> Peter said, a wonderful way to commemorate the 10th anniversar= y of
>> the
>>> special year and the release of the HoTT Book.
>>>
>>> Relatedly to Nicolai's question, this question also has an= easy proof
>>> in any Grothendieck infinity-topos.=C2=A0 Now that we know it = also has a
>>> proof in HoTT, do we know of any type in HoTT whose interpreta= tion in
>>> any Grothendieck infinity-topos is known to be inhabited, but = which
>>> isn't known to be inhabited in HoTT?
>>>
>>> On Fri, Apr 21, 2023 at 5:25=E2=80=AFPM Nicolai Kraus
>>> <nicolai.kraus@gmail.com> wrote:
>>>
>>>=C2=A0 =C2=A0 Hi David,
>>>
>>>=C2=A0 =C2=A0 Congratulations (again)! I find it very interesti= ng that this
>>>=C2=A0 =C2=A0 question has a positive answer. I had suspected t= hat it might
>>>=C2=A0 =C2=A0 separate HoTT from Voevodsky's HTS (aka 2LTT = with a fibrancy
>>>=C2=A0 =C2=A0 assumption on strict Nat). Since this isn't t= he case, do we know
>>>=C2=A0 =C2=A0 of another type in HoTT that is inhabited in HTS,= while we don't
>>>=C2=A0 =C2=A0 know whether we can construct an inhabitant in Ho= TT?
>>>
>>>=C2=A0 =C2=A0 Best,
>>>=C2=A0 =C2=A0 Nicolai
>>>
>>>=C2=A0 =C2=A0 On Fri, Apr 21, 2023 at 8:30=E2=80=AFPM Jon Sterl= ing
>>>=C2=A0 =C2=A0 <jon@jonmsterling.com> wrote:
>>>
>>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 Dear David,
>>>
>>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 Congratulations on your beautiful r= esult; I'm looking forward
>>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 to understanding the details. Recen= tly I had been wondering if
>>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 anyone had proved this, and I am de= lighted to see that it is
>>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 now done.
>>>
>>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 Best wishes,
>>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 Jon
>>>
>>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 On 21 Apr 2023, at 12:04, David W= =C3=A4rn wrote:
>>>
>>>> Dear all,
>>>>
>>>> I'm happy to announce a solution to one of the oldest = open
>>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 problems in synthetic homotopy theo= ry: the free higher group
>>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 on a set is a set.
>>>>
>>>> The proof proceeds by describing path types of pushouts as=
>>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 sequential colimits of pushouts, mu= ch like the James
>>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 construction. This description shou= ld be useful also in many
>>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 other applications. For example it = gives a straightforward
>>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 proof of Blakers-Massey.
>>>>
>>>> Best wishes,
>>>> David
>>>>
>>>> --
>>>> You received this message because you are subscribed to th= e
>>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 Google Groups "Homotopy Type T= heory" group.
>>>> To unsubscribe from this group and stop receiving emails >>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 from it, send an email to
>>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 HomotopyTypeTheory+unsu= bscribe@googlegroups.com.
>>>> To view this discussion on the web visit
>>>
>> https://groups.google.com/d/msgid/HomotopyTypeTheory/f2af459c-5= 3a6-e7b9-77db-5cbf56da17f3%40gmail.com.
>>
>>>
>>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 --
>>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 You received this message because y= ou are subscribed to the
>>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 Google Groups "Homotopy Type T= heory" group.
>>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 To unsubscribe from this group and = stop receiving emails from
>>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 it, send an email to
>>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 HomotopyTypeTheory+unsu= bscribe@googlegroups.com.
>>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 To view this discussion on the web = visit
>>>
>> https://groups.google.com/d/msgid/HomotopyTypeTheory/D102F= 774-D134-46B9-A70A-51CB84BE4B6F%40jonmsterling.com.
>>
>>>
>>>=C2=A0 =C2=A0 --
>>>=C2=A0 =C2=A0 You received this message because you are subscri= bed to the
>> Google
>>>=C2=A0 =C2=A0 Groups "Homotopy Type Theory" group. >>>=C2=A0 =C2=A0 To unsubscribe from this group and stop receiving= emails from it,
>>>=C2=A0 =C2=A0 send an email to
>> HomotopyTypeTheory+unsubscribe@googlegroups.com. >>>=C2=A0 =C2=A0 To view this discussion on the web visit
>>>
>> https://groups.google.com/d/msgid/Homotop= yTypeTheory/CA%2BAZBBpPwgh1G9VZV0fgJFd8Mzqfchskc4-%2B-FXT42WQkzmC9w%40mail.= gmail.com.
>>
>> --
>> 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 HomotopyTypeTheory+unsubscribe@googlegroup= s.com.
>> To view this discussion on the web visit
>> https://groups.= google.com/d/msgid/HomotopyTypeTheory/87leigyeya.fsf%40uwo.ca.
>
> --
> You received this message because you are subscribed to the Google Gro= ups "Homotopy Type Theory" group.
> To unsubscribe from this group and stop receiving emails from it, send= an email to HomotopyTypeTheory+unsubscribe@googlegroups.com.
> To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/= 87zg6qy4gx.fsf%40uwo.ca.

--
You received this message because you are subscribed to the Google Groups &= quot;Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an e= mail to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid= /HomotopyTypeTheory/21ED9406-6C3A-4B26-A74B-34C2821C97B6%40gmail.com.

--
You received this message because you are subscribed to the Google Groups &= quot;Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an e= mail to = HomotopyTypeTheory+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://gro= ups.google.com/d/msgid/HomotopyTypeTheory/CAE-BQ1zWQHqUv9woQPw75Sqz1c7_M9F-= nzX3RYYmXAxVxy8skQ%40mail.gmail.com.
--000000000000aff1cb05fa7e0ddd--