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 autolearn=ham autolearn_force=no version=3.4.4 Received: (qmail 17367 invoked from network); 21 Apr 2023 11:28:16 -0000 Received: from mail-yb1-xb37.google.com (2607:f8b0:4864:20::b37) by inbox.vuxu.org with ESMTPUTF8; 21 Apr 2023 11:28:16 -0000 Received: by mail-yb1-xb37.google.com with SMTP id 3f1490d57ef6-b92309d84c1sf5440744276.1 for ; Fri, 21 Apr 2023 04:28:16 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20221208; t=1682076494; x=1684668494; h=list-unsubscribe:list-subscribe:list-archive:list-help:list-post :list-id:mailing-list:precedence:x-original-sender:mime-version :subject:references:in-reply-to:message-id:to:from:date:sender:from :to:cc:subject:date:message-id:reply-to; bh=F9tj47fOl4tzGAzM2URKqWltQWvTN6v++kkmGYEJftU=; b=tYFwgqQZNnzLAK8zFa2+s4IVwuhiZ47cliuyLoOw5Nxm/N5bbNOH9MfY1PYUCgO5gw gsLRPvgyHMsFtrNeSis3GMvR/3lrLilCHtuDHEGkiSR50gBa4HT2xI/kOhkSRgkrVuYs RcarXoluufiIDQ27qAohTkdy04GR+3pXAeBlksjrqX3L0pPIs914/AlrFMjz6DUbOf2d hcOLk/chrVfUrGb90XVEuYc9fBKwPfhuvMCKQmtCM/uQ/w7ZJGG0yG7PdSt18rLx/7Fa 4J2NjUgd84weQ1TgxlFQncWfVgrOnMwTwIvUbH0EYz2PbL7HP5LkXRxA5yn+bp8dZKVv 1rOQ== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20221208; t=1682076494; x=1684668494; h=list-unsubscribe:list-subscribe:list-archive:list-help:list-post :list-id:mailing-list:precedence:x-original-sender:mime-version :subject:references:in-reply-to:message-id:to:from:date:from:to:cc :subject:date:message-id:reply-to; bh=F9tj47fOl4tzGAzM2URKqWltQWvTN6v++kkmGYEJftU=; b=VfzBOOwtiJdSgkxFhL4CLa2kos4JIUXItQaNPDGCOJU/zUHiWR7IiGP3X/DFPk/UXO /m4OA3eTwYTYPGHAz8SjNMCypIK6BcBtc6NiTmUPtLclhfv9KtDWntxe2+7FtutgWAGc pS5am34njKH4gckEagz1vGfIAbfbqfuyNs+Gsk7ilJ9XA2K9mrerq9V3BplQPM8yhNnB GXCbwvmKhjX0FflXhsdjbNaXocOuQRlzLSuTq/+Lkxu7wNjj3f9ZZBzvub7c0cEDCRRs dW/9eHUAXCEVgZDNcWtQmCfqyHtMrMZCBR2SyHyY+hHNkCuETw9Wm+Vc4l9Ro7ZV284t pCvA== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20221208; t=1682076494; x=1684668494; h=list-unsubscribe:list-subscribe:list-archive:list-help:list-post :x-spam-checked-in-group:list-id:mailing-list:precedence :x-original-sender:mime-version:subject:references:in-reply-to :message-id:to:from:date:x-beenthere:x-gm-message-state:sender:from :to:cc:subject:date:message-id:reply-to; bh=F9tj47fOl4tzGAzM2URKqWltQWvTN6v++kkmGYEJftU=; b=cSmlk69S2UWzDPXJbkBS+dwj6tKB2ZqVCWtuSmblKAzsaIsH4ZuMhJ58oaDpwz97bG mF0Di20PXL+dAo3Du6d4wmYouBLjTuhIaFL3+HKk7Rzxx73bsfiHg7nquskwWydhhkdC udX8sziDz7Z32FbbaOaCzxIEUT+U0TZqCl3EbDgpIcnBSaDLR89f8nU+o0jq2HII/La2 S2ZAMCUxU6KazrdYbh2Ub5eWi1AIhsesenzkJWjCQvloMxgfEgJarb84xqyi6oro4LUu Mgli7vdaSS7LdkKPxqu14FDPGRiV8A+Me4N8SsZ98//X0QT4oSKsHZRrTZDaNo7z7a2s s00w== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AAQBX9f0WEfKiyNmxn+ZxVz8FBVfU/a2LmfZeYo6WOINvcyATi4tqbWk SGmqIrfOGLAOywrVqN1T8q8= X-Google-Smtp-Source: AKy350YPHfXd83eljCPkqt3gZR263DmUfRR9UBDasDRRIRUbvLBFrbZ60GtGCHNWpyBMASv9wDbjXA== X-Received: by 2002:a81:4408:0:b0:54b:fd28:c5ff with SMTP id r8-20020a814408000000b0054bfd28c5ffmr1210205ywa.3.1682076494586; Fri, 21 Apr 2023 04:28:14 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a81:98c3:0:b0:54f:8af1:7323 with SMTP id p186-20020a8198c3000000b0054f8af17323ls2422083ywg.7.-pod-prod-gmail; Fri, 21 Apr 2023 04:28:13 -0700 (PDT) X-Received: by 2002:a81:b514:0:b0:556:414:5805 with SMTP id t20-20020a81b514000000b0055604145805mr1185429ywh.7.1682076493070; Fri, 21 Apr 2023 04:28:13 -0700 (PDT) Date: Fri, 21 Apr 2023 04:28:12 -0700 (PDT) From: Ulrik Buchholtz To: Homotopy Type Theory Message-Id: <4e1cf0e3-a5b0-4014-b144-0a5bb98b01e3n@googlegroups.com> In-Reply-To: References: Subject: [HoTT] Re: Free higher groups MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_4044_1832388778.1682076492356" X-Original-Sender: UlrikBuchholtz@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: , ------=_Part_4044_1832388778.1682076492356 Content-Type: multipart/alternative; boundary="----=_Part_4045_1241474095.1682076492356" ------=_Part_4045_1241474095.1682076492356 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Congratulations, that's really great! And indeed, this is going to be very useful in general: for instance,=20 together with Tom de Jong and Egbert Rijke, we used your work as an input= =20 to give a short constructive proof of the non-triviality of the Higman=20 group. I'll talk about this in Vienna on Sunday. Best wishes, Ulrik On Friday, April 21, 2023 at 12:04:20=E2=80=AFPM UTC+2 cod...@gmail.com wro= te: > Dear all, > > I'm happy to announce a solution to one of the oldest open problems in=20 > synthetic homotopy theory: the free higher group on a set is a set. > > The proof proceeds by describing path types of pushouts as sequential=20 > colimits of pushouts, much like the James construction. This description= =20 > should be useful also in many other applications. For example it gives a= =20 > straightforward proof of Blakers-Massey. > > Best wishes, > David > --=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/4e1cf0e3-a5b0-4014-b144-0a5bb98b01e3n%40googlegroups.com= . ------=_Part_4045_1241474095.1682076492356 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Congratulations, that's really great!

And i= ndeed, this is going to be very useful in general: for instance, together w= ith Tom de Jong and Egbert Rijke, we used your work as an input to give a s= hort constructive proof of the non-triviality of the Higman group. I'll tal= k about this in Vienna on Sunday.

Best wishes,
Ulrik


On Friday, April 21, 2023 at 12:04:20=E2= =80=AFPM UTC+2 cod...@gmail.com wrote:
Dear all,

I'm happy to announce a solution to one of the oldest open problems= in=20
synthetic homotopy theory: the free higher group on a set is a set.

The proof proceeds by describing path types of pushouts as sequential= =20
colimits of pushouts, much like the James construction. This descriptio= n=20
should be useful also in many other applications. For example it gives = a=20
straightforward proof of Blakers-Massey.

Best wishes,
David

--
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.c= om/d/msgid/HomotopyTypeTheory/4e1cf0e3-a5b0-4014-b144-0a5bb98b01e3n%40googl= egroups.com.
------=_Part_4045_1241474095.1682076492356-- ------=_Part_4044_1832388778.1682076492356--