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.0 required=5.0 tests=DKIMWL_WL_MED,DKIM_SIGNED, DKIM_VALID,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 3942 invoked from network); 25 Apr 2023 00:02:59 -0000 Received: from mail-yw1-x113a.google.com (2607:f8b0:4864:20::113a) by inbox.vuxu.org with ESMTPUTF8; 25 Apr 2023 00:02:59 -0000 Received: by mail-yw1-x113a.google.com with SMTP id 00721157ae682-54ee0b6ee72sf39303937b3.0 for ; Mon, 24 Apr 2023 17:02:59 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1682380977; cv=pass; d=google.com; s=arc-20160816; b=edYpkAh1EUjCG8z/rkHKZNWC1bll2vgHJ6dbs9OyCwSTWg5EgCblrrGGyc/YuRWD+s xCn5vNv7lO94/K6HhwxSGiM60C4AdqgIkF42sH+LyyNj/rr9z7X7ByNiakkeBsnNaTlS ptJuoyxMV9cPJ1n0jSBYpFFhP+hQ+rmt6+IMmytv9GAbQ8W/O15Y7fptjhlt0aGDkcpT jhxj4T877YMsin9rbBdumtkt8/O9tdAgm73q5IKlN16HAv+j5tsaiGt8/6YNGzj0745g FHn8jTQW/q1ND1uZRp1SW8jqQ6MHqxKfcLWcZUE/VtXkxClGFSY04AX6ral/nZAV1Xpg KTrQ== 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; bh=jQsTNtc1LO5mPG6ElTTaUf6fNqvHqBhWvFlPXq1uGUE=; b=0pSO3mdPlvBreYSBxZ9JeutN3C+oCFIq5cAd3AhDTyYVDFglR9Elf/9q2/47UmJEtU y/QUyTGL73MwxBE21ILbhjhWdaU9sN59r79Ksl17sGR4Z491gM+GKDjn64xx7G/psBpu 8kUVS2NxCrvQp5Rb40BCx9EjK47em2tez4OCRQ71J2IbRsQbUPRKmy1uBfsVpabTZZsS pvRYV5yYkbnEuBKQTACDeSjoWe0oun2JZyR1jHBoI0UpuaqNEQxyvwiTubRmnAfXd8zp WxGQHAdjoXnnBlmbXxFnfQHXeF6vhZcY6HNEtSGiekbuysmlDA5YjUkj4dDwh/bVIusP 9Zfw== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@sandiego.edu header.s=google header.b=PUKQtXEl; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::1129 as permitted sender) smtp.mailfrom=shulman@sandiego.edu; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=sandiego.edu DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20221208; t=1682380977; x=1684972977; 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=jQsTNtc1LO5mPG6ElTTaUf6fNqvHqBhWvFlPXq1uGUE=; b=cAK1kJrXVQbgkj3xkzSZnSRTMRzpbhKp0976TYJe5t37j+OIZZPgbDhNl0uLDY8u4V Bmlq1iKrdEF51yelrdTEGc2rSVbRCmZ+DuWi6W7vq40zILkv2ZQZ0hQWB76rRBd3+jI2 jvW1CAgT7ouqBy1+DhD8AVKbaHwNUGJ2lVUOmZMu7wnnAMmtZ5ziKOR0HOtzsAGxq/TF MSHGD5tJoU+Y2hgbA9OSBvF8eHlk2BBBql0jXDVJU1ZTKaOtF6PzutTEeyc5hupQKnE0 kcZkjOVLrCvmrXbxu2ie3fDkyrB8NF+kPSaJ6uDbHc1UXmv5kw0W4BEy16YEFFNfNqO3 Qp+A== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20221208; t=1682380977; x=1684972977; 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=jQsTNtc1LO5mPG6ElTTaUf6fNqvHqBhWvFlPXq1uGUE=; b=h+akOLl7zEguoXqVFAq6Hquy4vka52ukdZwHzDRK9j8oD7u6Ts5SEklLAouygrUNx9 SfYG2FdsUd8XsAEjTKCTx9jBkln2ti5Gy5LsPCKovDAev+GCvMzfwyW3x7rcVWyarEhD njw/Q4ZU9Wal8xcBRQAQufi4DhxT9e3vfZhELPZRrT7vZyz9vJpmzOsefnxU94lDwgcT Eau3ypOkENuxzey7YONqwDhhMqtdlR8nutoT3A1uqc3Flx33FgQUJPbw5cq29xt6uuHe rVzjf7qA2/lW4OOeJhxYXUXh3hHF8gVTCA88a2RGr0GAr/KGX8YWdUKH0848lhvKJiDQ 3Law== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AAQBX9dMkjSvp+S+Ya8Wstbxh87DbfQ6JqNWwP1slKJ21eZg6UYDgTFv F8LiEOFW0fdk/vZkFMPgyJU= X-Google-Smtp-Source: AKy350Z4dkMb65mEIhIJAqVoJJB3D0fbtG+nZsiV5ywMkp+LUn9tUQdIfo6y3QjA9QjpT90zLZbWqA== X-Received: by 2002:a81:af5b:0:b0:54f:b56a:cd0f with SMTP id x27-20020a81af5b000000b0054fb56acd0fmr7264141ywj.3.1682380977092; Mon, 24 Apr 2023 17:02:57 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a25:b8b:0:b0:b95:7033:8256 with SMTP id 133-20020a250b8b000000b00b9570338256ls219246ybl.5.-pod-prod-gmail; Mon, 24 Apr 2023 17:02:55 -0700 (PDT) X-Received: by 2002:a25:e092:0:b0:b8f:469a:cb9b with SMTP id x140-20020a25e092000000b00b8f469acb9bmr13021435ybg.52.1682380975453; Mon, 24 Apr 2023 17:02:55 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1682380975; cv=none; d=google.com; s=arc-20160816; b=XxzrKdJst4n3KkYyNQhtHwZq0KssaFdsNp8IyLPFnB+Oeun3SPaBDBFGWN+iwZNHWc b4Drg+cHab+lv36fmvoSDyyRaDe6ZDN4dXKtmosyZ+5D5mbMZ1IefzXanzBE7vfaYA2i w1BUu1E3uK0wA2uBMscIzPL3mLrUglGpeCyWiVYf92qW+oSc0ecPlTOYtesnmqr91Cxh Vl5uU+7LH47F9iDgODEGALg4k0K5B0uaBqiDkSzbLJydKZ77l8V+M1q31HBjtvIunkjl vZG27s/DTqmhyAqLBnDonceIeDlLaUiUXXv52erzQT1dBhE3OG2HviwOmvOp4y+5nVpH Qrvg== 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=LbQ80GyCPKyHnOynKyOZmKLxODvHYiO9NgtCAOJNjag=; b=TAymicyK08ih4/p0MPKGAV7YqyFtOsqJnyWQUdjzHOnzSSEDpIlEKD9xH8oRX6Eqmr pn77adeKyPw82OmDWmq1TUNLNyUTtZV1jHpLsCgO/JlSoyfuC6BN9kVdFsY6KFcQdtrp hoK5873muSHPpNwcxGWWlbD3exVSe75k6tozWja5Sz46JcnF72ES2NpuzXNsd1aCxRav uXmKCSBOKRCKxIpwOFM9IM4bSOgzzDa436szTOyqdenc+w92bx4NCnQRLoDsJbolDRyZ IyS1MpOEmyAmIpXneaD4j3058XcH+VSQ+JY1KxocSfa4wIfLDdU77V0LGl0oaCj/gBd3 DbiA== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@sandiego.edu header.s=google header.b=PUKQtXEl; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::1129 as permitted sender) smtp.mailfrom=shulman@sandiego.edu; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=sandiego.edu Received: from mail-yw1-x1129.google.com (mail-yw1-x1129.google.com. [2607:f8b0:4864:20::1129]) by gmr-mx.google.com with ESMTPS id bw17-20020a056902161100b00b95dbfe6762si539716ybb.1.2023.04.24.17.02.55 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Mon, 24 Apr 2023 17:02:55 -0700 (PDT) Received-SPF: pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::1129 as permitted sender) client-ip=2607:f8b0:4864:20::1129; Received: by mail-yw1-x1129.google.com with SMTP id 00721157ae682-555d2810415so74001397b3.0 for ; Mon, 24 Apr 2023 17:02:55 -0700 (PDT) X-Received: by 2002:a0d:e8d0:0:b0:549:2623:5d21 with SMTP id r199-20020a0de8d0000000b0054926235d21mr10663466ywe.6.1682380975128; Mon, 24 Apr 2023 17:02:55 -0700 (PDT) MIME-Version: 1.0 References: In-Reply-To: From: Michael Shulman Date: Mon, 24 Apr 2023 17:02:44 -0700 Message-ID: Subject: Re: [HoTT] Free higher groups To: Nicolai Kraus Cc: homotopytypetheory@googlegroups.com Content-Type: multipart/alternative; boundary="00000000000066632905fa1dd8dd" X-Original-Sender: shulman@sandiego.edu X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@sandiego.edu header.s=google header.b=PUKQtXEl; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::1129 as permitted sender) smtp.mailfrom=shulman@sandiego.edu; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=sandiego.edu 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: , --00000000000066632905fa1dd8dd Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable 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 ha= s > a positive answer. I had suspected that it might separate HoTT from > Voevodsky's HTS (aka 2LTT with a fibrancy assumption on strict Nat). Sinc= e > 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 HoT= T? > > 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-= 77db-5cbf56da17f3%40gmail.com >> . >> >> -- >> You received this message because you are subscribed to the Google Group= s >> "Homotopy Type Theory" group. >> To unsubscribe from this group and stop receiving emails from it, send a= n >> email to HomotopyTypeTheory+unsubscribe@googlegroups.com. >> To view this discussion on the web visit >> https://groups.google.com/d/msgid/HomotopyTypeTheory/D102F774-D134-46B9-= A70A-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 > > . > --=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/CADYavpxM-_a_nM0qu7XBv66oP8VG852BaMwmzo3%2BNgGxijf8Rg%40= mail.gmail.com. --00000000000066632905fa1dd8dd Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
This is fantastic, especially the simplicity of the c= onstruction.=C2=A0 As Peter said, a wonderful way to commemorate the 10th a= nniversary 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 interpretat= ion 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:
Hi David,

= Congratulations (again)! I find it very interesting that this question has = a positive=C2=A0answer. I had suspected that it might separate HoTT from Vo= evodsky's=C2=A0HTS (aka 2LTT with a fibrancy assumption on strict Nat).= Since this isn't the case, do we know of another type in=C2=A0HoTT tha= t is inhabited in HTS, while we don't know whether we can construct=C2= =A0an inhabitant in HoTT?

Best,
Nicolai
<= div>=C2=A0

On Fri, Apr 21, 2023 at 8:30=E2=80=AFPM Jon Sterling = <jon@jonmsterl= ing.com> wrote:
Dear David,

Congratulations on your beautiful result; I'm looking forward to unders= tanding the details. Recently I had been wondering if anyone had proved thi= s, 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 problem= s 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 sh= ould be useful also in many other applications. For example it gives a stra= ightforward proof of Blakers-Massey.
>
> Best wishes,
> David
>
> --
> 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/f2af459c-53a6-e7b9-77db-5cbf56da17f3%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://groups.google.com/= d/msgid/HomotopyTypeTheory/D102F774-D134-46B9-A70A-51CB84BE4B6F%40jonmsterl= ing.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://groups.google.com/d/msgid/HomotopyTypeTheory/CA%2BAZ= BBpPwgh1G9VZV0fgJFd8Mzqfchskc4-%2B-FXT42WQkzmC9w%40mail.gmail.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://g= roups.google.com/d/msgid/HomotopyTypeTheory/CADYavpxM-_a_nM0qu7XBv66oP8VG85= 2BaMwmzo3%2BNgGxijf8Rg%40mail.gmail.com.
--00000000000066632905fa1dd8dd--