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 24786 invoked from network); 21 Apr 2023 14:32:39 -0000 Received: from mail-wm1-x337.google.com (2a00:1450:4864:20::337) by inbox.vuxu.org with ESMTPUTF8; 21 Apr 2023 14:32:39 -0000 Received: by mail-wm1-x337.google.com with SMTP id 5b1f17b1804b1-3f080f46fb1sf7306115e9.0 for ; Fri, 21 Apr 2023 07:32:39 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1682087559; cv=pass; d=google.com; s=arc-20160816; b=IeCfWtKyDJUZMA/RR1ln4Mwyb4Mg+47UKiAlGp107CbCbXCZlM2G0yuE04dBy2Fk/c Zs7VzJW8piittYVDmAbBZNhWr3K6JveBB3TmxU4VmZaLGEM/R6UPq6vcuoTNYrhuGLqI 0Zl3UwXBE5HVuRHK9ApUoAdCwHWwnlEifrNAeuY6jereKk9+VBPqr+LQHnL2lep0iqQR jq5E5my2M2T/WDqv/mvl70s10rLMYYdtiweGRTcww8FBNUtBIUKvbtd6qTrnCR5mYms2 2UJpP0KKTyA/gQQNnu1EusbIeFa5aU02hsW10Sje0Fh+iIs+HnT8r+zwEzx2tVjpUgeT 0RDQ== 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:to:subject:message-id:date:from :in-reply-to:references:mime-version:sender:dkim-signature :dkim-signature; bh=kG8uAcqP2mUL0gPfoOK2GWQZ/EUe36Xy89srXxfvAts=; b=e2jC6cMevGdzo2vDPTqjo9fQ9hUdvk+2A1yQ2fCBIbcDmFBFmr4nPptDIl64q6fmlh wQVbGatRrtYffw/9ngyL5+zq396py1vecI2gOmOZco/wWHtr8BG6K0BsYZS5m39ecwWd 2GSSmvjRqHMJN6XAJ9/Uwb/ECHEb5v3DkjTUX6ggYc2/hesJx5v/wrkn5+PSoiH/pnei ujceCew6u4e7OOSfYWa+4mrNVDRO2ra1DYe1dIQKHmVf20BVcBEQfKtiAhryNlGvvRSU YHsdFVswELutQsSbF2nufHoNQKWpwg3CL+XBKLuoymhl9T+kNDFp9mWkDBc/jtauVWmb QZlg== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20221208 header.b=T5NUXp6c; spf=pass (google.com: domain of p.l.lumsdaine@gmail.com designates 2a00:1450:4864:20::633 as permitted sender) smtp.mailfrom=p.l.lumsdaine@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=1682087559; x=1684679559; h=list-unsubscribe:list-subscribe:list-archive:list-help:list-post :list-id:mailing-list:precedence:x-original-authentication-results :x-original-sender:to:subject:message-id:date:from:in-reply-to :references:mime-version:sender:from:to:cc:subject:date:message-id :reply-to; bh=kG8uAcqP2mUL0gPfoOK2GWQZ/EUe36Xy89srXxfvAts=; b=bWv+qpYGadGb8ghhr/LO54hVLni4vT4PHd0CyLel18+7BYl+UmUbP5TSrHl1vrS3lC h3qFugSdoTQOylg8fAAPPh3BbMJ1CYNGCNNXatQbZ2VjqVyzNSonsM65nFxubWaAodyc 8AB22CW9Hv+Wb4IQXj2EndTDPXeNQ5HkBHWCuPjeg1U/YWmErssmJEt9KQxeDL6e9j3U Q8qjcb5t6/cxBPUdQFKtq8Z7nGXf8mIKuwyi0M0MIEIydwkZRhcZuSr1D3sPFcFUjEFz UdwTk34jhvr4SuBN5P0DypaRB+A78biw6kwf0feD+geCjDUhB7y4As0DAMkTD6+Xu5Kp mEMw== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20221208; t=1682087559; x=1684679559; h=list-unsubscribe:list-subscribe:list-archive:list-help:list-post :list-id:mailing-list:precedence:x-original-authentication-results :x-original-sender:to:subject:message-id:date:from:in-reply-to :references:mime-version:from:to:cc:subject:date:message-id:reply-to; bh=kG8uAcqP2mUL0gPfoOK2GWQZ/EUe36Xy89srXxfvAts=; b=HRo66bKkwFdh2mzPInev6Z0n2i4f9et4aiWGQhlgk1hVgjFf7ue2Uqh4Bxvjj9XmDa 95oAuFktj49/ZBa7ASWgtIb9hVl2IDMdWcPxP5boWCquXR+ToOyy61b5sckYH2hu3VR2 Mjprvq0Yy+BqVmHZDMdHcjBjIDK/pjGL92ENDtCBu+ji4cn1n+hU+b5r9pswNQ2x8vZE /Mei5JmbCbMwmdwMdhztxql/JDn+5FW2m6H5RBIEyenGmkBNNq2Kf5cUXm7HLzoGWWEK 8l6nUmQT6yzw6VfnCjhAWwou8Nzt/Ap2EXap0aSsZCL2IKdI2mylaOlX8ZZmy1o+oVcC rkEQ== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20221208; t=1682087559; x=1684679559; 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: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=kG8uAcqP2mUL0gPfoOK2GWQZ/EUe36Xy89srXxfvAts=; b=PLnGycoag3lGsOwVvud12R1AeoylcM4RbqqGWyHl7TL+rJ+YDfToeoLSi6jEX2kniL xca37Dm4AurKY5Zg+IQSZZrNW7vJ7QEGwMgjlmtjjMfq/hyRglqGcKZ7kreXgwG9ORV1 fYZGRiwLcnTnopbOjot8gPp8brxtD1mSP9Imv0YuUDUrsqTfAZzr9yuCkvM97AsQl3qh GKeegilXpJFPHO7LFI7XvQx/E3ZJH0i/diM48UQzNP8x9yiB6yUObXT/yVb+0avYtaOZ FBAZrqQsO3lLszV7z9yg4qaYRktglwo1KvTWVLXIVB5E2g63f7HL+gusuikg97JcFTIN R1ZA== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AAQBX9fhy3doSxL7ojTRrMXcJBuYBiIFuAH5ylIr1D5cA4Zh42s4nnJm A6ISEkcnjlrT+zAza+qnqM0= X-Google-Smtp-Source: AKy350b7waoBuvxx8qtb8UJH3/TDbWG1HKy02KmDkRO5PB/dJDt5Q6bskV1yaAYLo/pq7YLesLGrgg== X-Received: by 2002:a1c:ed07:0:b0:3f1:72ec:401c with SMTP id l7-20020a1ced07000000b003f172ec401cmr510871wmh.1.1682087559016; Fri, 21 Apr 2023 07:32:39 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a05:600c:3148:b0:3f1:714d:c42c with SMTP id h8-20020a05600c314800b003f1714dc42cls2519693wmo.0.-pod-control-gmail; Fri, 21 Apr 2023 07:32:36 -0700 (PDT) X-Received: by 2002:a05:600c:3b1b:b0:3f1:89de:7e51 with SMTP id m27-20020a05600c3b1b00b003f189de7e51mr2066042wms.12.1682087556548; Fri, 21 Apr 2023 07:32:36 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1682087556; cv=none; d=google.com; s=arc-20160816; b=qDRpaxvtVWEJhxTDI1stE4xxgHBrQHd+8SAykOBJmdtcLMSwx+260uPdyolD7vvX+1 Imat5lTS43xk/c/dL2BGfNEy1wZfJ3PxdGVfn79euBfFqCCDlk/Y3s2i83JS3ay3oRwD FtRrRyvjjohS2wm8GYKplnxNqROS+KUaSOwS6nIT2egq1K28Q8Pkmoo5Luvaxx5OWCu2 yRGSakCoEDiKdOIu6vIW5Ai4zzavb4D23lb42RpUMZQUh++DXA05BM4y4FwmuwYTI9NE ZiQAub+odlFiXRci53VdkSpW+LsXF4NTn5KRa78ZiiQBDvNU/GlZ+6fkIVkVJJLOYn0l uvLA== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=to:subject:message-id:date:from:in-reply-to:references:mime-version :dkim-signature; bh=XUX9doo5Uu71lJTGtwJAA0E+nW3lWwwpCOFZf/eXx+I=; b=Ew8fvJHSGHxrLF+W4ZvRDES3zthp7uXPY9kP1s+Q4qyw0Zpy577wPCu43nK3Yccxcs DWb4UWwbJmXwYbe4Y38oYAfZm0e6f94184J8tWFx4DVeSsFJjZFjbKLVI121qpxQiQ+F KN9JiljKV7eIom+KTkvKbhU6uLHvxlF9T2QteBqOy29Zak90IUf9m5N6ZHOYDlcegaL5 +M+PFGprXh2YbTe9q5Rb2yYYCa3UaWlloj23v07PYBXRQIfb7OgAc60m9haSsAmTm97E atYTrKyHjj8GzA4v0Fx2z9q4gIPWIwXLopX+DoTPu0r5ImrU4s2NoF+bNid4avHq95xr VFig== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20221208 header.b=T5NUXp6c; spf=pass (google.com: domain of p.l.lumsdaine@gmail.com designates 2a00:1450:4864:20::633 as permitted sender) smtp.mailfrom=p.l.lumsdaine@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-ej1-x633.google.com (mail-ej1-x633.google.com. [2a00:1450:4864:20::633]) by gmr-mx.google.com with ESMTPS id p12-20020a05600c1d8c00b003f17514c7b3si82917wms.1.2023.04.21.07.32.36 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Fri, 21 Apr 2023 07:32:36 -0700 (PDT) Received-SPF: pass (google.com: domain of p.l.lumsdaine@gmail.com designates 2a00:1450:4864:20::633 as permitted sender) client-ip=2a00:1450:4864:20::633; Received: by mail-ej1-x633.google.com with SMTP id a640c23a62f3a-95369921f8eso250104666b.0 for ; Fri, 21 Apr 2023 07:32:36 -0700 (PDT) X-Received: by 2002:a17:907:75d7:b0:94f:1c20:6e19 with SMTP id jl23-20020a17090775d700b0094f1c206e19mr1191709ejc.11.1682087555475; Fri, 21 Apr 2023 07:32:35 -0700 (PDT) MIME-Version: 1.0 References: In-Reply-To: From: Peter LeFanu Lumsdaine Date: Fri, 21 Apr 2023 15:32:23 +0100 Message-ID: Subject: Re: [HoTT] Free higher groups To: homotopytypetheory@googlegroups.com Content-Type: multipart/alternative; boundary="00000000000039aa7b05f9d98744" X-Original-Sender: p.l.lumsdaine@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20221208 header.b=T5NUXp6c; spf=pass (google.com: domain of p.l.lumsdaine@gmail.com designates 2a00:1450:4864:20::633 as permitted sender) smtp.mailfrom=p.l.lumsdaine@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: , --00000000000039aa7b05f9d98744 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Lovely =E2=80=94 congratulations! I remember at the IAS special year discu= ssing (with Guillaume Brunerie and others) the feeling that there should be a James construction style proof of Blakers=E2=80=93Massey, but we were never= able to find it =E2=80=94 fantastic to see that it can be made to work after all. = And the timing is nice =E2=80=94 it=E2=80=99s almost exactly 10 years since the fin= al seminar of the special year, where Guillaume, Dan and I presented a survey of the results in synthetic homotopy theory so far, including Blakers=E2=80=93Mass= ey and the James construction: https://www.ias.edu/video/univalent/1213/0411-HomotopyGroup Best, =E2=80=93Peter. On Fri, Apr 21, 2023 at 11:04=E2=80=AFAM 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 > . > --=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/CAAkwb-kzRC70p5Xpv8YANJqUgHbDMj2y5e6A2x4RX8WbAEseag%40ma= il.gmail.com. --00000000000039aa7b05f9d98744 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Lovely =E2=80=94 congratulations!=C2=A0 I remember at the = IAS special year discussing (with Guillaume Brunerie and others) the feelin= g that there should be a James construction style proof of Blakers=E2=80=93= Massey, but we were never able to find it =E2=80=94 fantastic to see that i= t can be made to work after all. =C2=A0 And the timing is nice =E2=80=94 it= =E2=80=99s almost exactly 10 years since the final seminar of the special y= ear, where Guillaume, Dan and I presented a survey of the results in synthe= tic homotopy theory so far, including Blakers=E2=80=93Massey and the James = construction: =C2=A0https://www.ias.edu/video/univalent/1213/0411-HomotopyGrou= p

Best,
=E2=80=93Peter.





On= Fri, Apr 21, 2023 at 11:04=E2=80=AFAM David W=C3=A4rn <codwarn@gmail.com> 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 &= 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/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://gro= ups.google.com/d/msgid/HomotopyTypeTheory/CAAkwb-kzRC70p5Xpv8YANJqUgHbDMj2y= 5e6A2x4RX8WbAEseag%40mail.gmail.com.
--00000000000039aa7b05f9d98744--