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,MAILING_LIST_MULTI,RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.4 Received: (qmail 2199 invoked from network); 21 Apr 2023 18:30:59 -0000 Received: from mail-lf1-x139.google.com (2a00:1450:4864:20::139) by inbox.vuxu.org with ESMTPUTF8; 21 Apr 2023 18:30:59 -0000 Received: by mail-lf1-x139.google.com with SMTP id 2adb3069b0e04-4edbdd8268bsf1090184e87.2 for ; Fri, 21 Apr 2023 11:30:59 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1682101859; cv=pass; d=google.com; s=arc-20160816; b=deuW6j+guXpSB99ZouDZGxuBOCBqHUYJen0KsXTzK1B0iONaWXJEvUUz0AEYG/HcrC bFGYsOq5mpbKBAjK7ilyN4t5r4hHFX3OaswrtvlSxXNQNYGRLWm+o4bcyHSisjlDSs1N r60zsgS7/g3LGumzNGKJOzNVbKZZU2LBO7QiDByUDbBMtxCGVHpAjxzD3KI0QmxmII60 wVAmMootltUfQUrYzZjr6eKJb+QgxMp+Jq1g6Ind7xHzmHUo1GeS8zXUUlfc7HMFtijw 4YOQd+sqRFBUhV+qKiTu/XhunzmG/jLhRnFPeYnWSlYUbwr2MPwZ79yPKyZep9BXHGdF vFGQ== 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:content-transfer-encoding :mime-version:references:in-reply-to:message-id:date:subject:cc:to :from:feedback-id:sender:dkim-signature; bh=JtU6vmTY4z6aoudKx/BZiDB+/Medwqra8uZsLg9umxE=; b=hqzRSIgek2SEU+cfcuXoGYIoUA7ID5O/TPisYNxsvp19WZAT7vEjmA1OkUVs0QttSk HFQztmftmwN2H/qHwaMbT9isbHAkpGcKxgrnqHVKkyrjrWs27d+id36j72BP39MzbqD3 NqUkEUzNU/rjkXrn0EoCIE2A4l/kee8bFO8VtK6r3myMChL9qq66DJ8KJCRqxzSrk795 sejobBmVBgTbZOOY89V00xJYsUblC5Ea6AehsngFse/XuHDRbP//5XjW1MjQ9ZJH1yPm 0LfKhGv8FV8v5AhdY34W5idJ/kQhkQSsVWSYOyyhE0yqg8vu3T/LKbTT/XwsfvZWrUXE hqSA== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@jonmsterling.com header.s=fm1 header.b=V1y1Osav; dkim=pass header.i=@messagingengine.com header.s=fm3 header.b=GzvjvubV; spf=pass (google.com: domain of jon@jonmsterling.com designates 64.147.123.19 as permitted sender) smtp.mailfrom=jon@jonmsterling.com DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20221208; t=1682101859; x=1684693859; h=list-unsubscribe:list-subscribe:list-archive:list-help:list-post :list-id:mailing-list:precedence:x-original-authentication-results :x-original-sender:content-transfer-encoding:mime-version:references :in-reply-to:message-id:date:subject:cc:to:from:feedback-id:sender :from:to:cc:subject:date:message-id:reply-to; bh=JtU6vmTY4z6aoudKx/BZiDB+/Medwqra8uZsLg9umxE=; b=Zdj2nP1gS1ZlPeXc4ZPoMHUuoMyBtAAJftqGX448FVou/2UaTV6rcuxbb+U/pbcWUu CWJjAklXJ7uj+klecxMtszABwT3BZF/UGyV5rsrB7E5V2zz8FScgcZfv2GzhS4ZSRQLB 2OR43zrvuNI4qn6uAgDax1/e/NmGsdO2Se9Udr+IciQK8ov1JfQS9y7ZMAV62gzVA5Gz p6nMI/EZwCday8i5l6YjJEW2duYgmZcmvdzwiqSyxePPPupHZmj1QdpnlAFyM6PGLPMu XNh7V3/4TwaYf+NaKa+O3xmmAuKJFEXbGebv7fCdSL/t3gGukTyf81uO6+H4zo7omEEO OoVw== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20221208; t=1682101859; x=1684693859; 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 :content-transfer-encoding:mime-version:references:in-reply-to :message-id:date:subject:cc:to:from:feedback-id:x-beenthere :x-gm-message-state:sender:from:to:cc:subject:date:message-id :reply-to; bh=JtU6vmTY4z6aoudKx/BZiDB+/Medwqra8uZsLg9umxE=; b=KbnOHWe8vVzTzYjCUw9EXIZjqBipW2NFQ7+0SlyjNlpJ+WIyYvgyKD/Ac1j7Mk5wiJ UJ2N42AXoA7rwlTNPbk4pRGVAfdFJ1eJDbQ2sIQfZknVTbw6jxO6RUEpo8/Gdcr1lljU FM94pXbp4QHo5hRGbY1YIXMjgz54l08OQvMNOg9AnvVoRUTyMtxdQh4woC4Ft/t7U7nc UXwkWD14qQOkmOSXItvpL1tWqf9V0jDX2raB0RidMFQqa72CStsXEo0WjasRzqPFRgmc WpdPJKO59EOuk8+di1LmAkZaAwsyGwwDdFwLMRwxpL0fbs9h7XBKVY+iYLQCiIGnC1Gd 6aCw== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AAQBX9dVvZz81UpJFB2M11aKfC7ks7Dnm0DwiodMu1d0yh2SENMX4LKJ ZI+uYVWVKDdRyaQnCUqCdOY= X-Google-Smtp-Source: AKy350Zfku5tUrKTWAPIuziApQrhwmX6y0kIxVL/IXztWPkS4d7reectdqec6PY7nZwn+iNhP6Cl0A== X-Received: by 2002:ac2:54b0:0:b0:4ec:825c:3d0f with SMTP id w16-20020ac254b0000000b004ec825c3d0fmr1485571lfk.2.1682101858953; Fri, 21 Apr 2023 11:30:58 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:ac2:5f5b:0:b0:4ed:c108:7214 with SMTP id 27-20020ac25f5b000000b004edc1087214ls3585823lfz.3.-pod-prod-gmail; Fri, 21 Apr 2023 11:30:56 -0700 (PDT) X-Received: by 2002:ac2:5198:0:b0:4b5:61e8:8934 with SMTP id u24-20020ac25198000000b004b561e88934mr1290049lfi.64.1682101855994; Fri, 21 Apr 2023 11:30:55 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1682101855; cv=none; d=google.com; s=arc-20160816; b=EqeqYqmghFvWXtL4d59aKBQBNlLxMgCm1gPCm/fyq2rFqHtWdJI0ofWDJbLSoue5Ur XtCnxRBv6Ep6sHWxZs4y4lTqAAY0lHl1lQlqDRBb1fmPd0SFnOz9pGFDa3+aa7pldykI RKkMEPNm7GKFSngSUVWjCd/1xXpBeALUxCjBfugzUkqaZcpD9KwNaiDXy1nFXGEoplJO 4PW81XMcx1fh9vrA+WuvY+X48IoI7Z6bPshnZEJFF/YuOoC3k2uoJJTh76F4obXXBOha S3jdUAaCu1J/V/uCa/fRZJqq2cNRj+N97UUY4gpahmdIDTa5M+yUOEHTaiyJl5AIgxUo 4P1Q== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-transfer-encoding:mime-version:references:in-reply-to :message-id:date:subject:cc:to:from:feedback-id:dkim-signature :dkim-signature; bh=EXuyQH/zT6RvKrbObEDO5t41X6t243HgGAPX3D12MBM=; b=XiJxNscRPCnj22W9rwigsIxW3Cm5H6071Iqp1jAu0dRU0GTVcH+oEEWDkOwxr/dVEk 6yJlo0K9OAH1nZLM4HgU6OFjl7603bsoByUNkUOdOcveZrJG20RTxACnT/cA7rtuYvK+ GfP6PIhOlCHMPhux+dnDNDlGdxXNnU/vD+93ujHPSoGkgUp/s/auU0kz/wFMm3HpLJbh BeRVmHk3zimw9oMM3bvS6FwEiOWwLx6bQtVTClk226HaQxbbFWBxmtwHfwvvDbKfJAJw pIMo9vFqBCdw8McM46d4Lp0NuVkNCgYqXBaB4G1XXT01smY9wVNhkxrZIZHdDBO9L09A gfWQ== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@jonmsterling.com header.s=fm1 header.b=V1y1Osav; dkim=pass header.i=@messagingengine.com header.s=fm3 header.b=GzvjvubV; spf=pass (google.com: domain of jon@jonmsterling.com designates 64.147.123.19 as permitted sender) smtp.mailfrom=jon@jonmsterling.com Received: from wout3-smtp.messagingengine.com (wout3-smtp.messagingengine.com. [64.147.123.19]) by gmr-mx.google.com with ESMTPS id b33-20020a0565120ba100b004dd8416c0d6si352221lfv.0.2023.04.21.11.30.55 for (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Fri, 21 Apr 2023 11:30:55 -0700 (PDT) Received-SPF: pass (google.com: domain of jon@jonmsterling.com designates 64.147.123.19 as permitted sender) client-ip=64.147.123.19; Received: from compute1.internal (compute1.nyi.internal [10.202.2.41]) by mailout.west.internal (Postfix) with ESMTP id 9C28E3200A92; Fri, 21 Apr 2023 14:30:53 -0400 (EDT) Received: from mailfrontend1 ([10.202.2.162]) by compute1.internal (MEProxy); Fri, 21 Apr 2023 14:30:53 -0400 X-ME-Sender: X-ME-Received: X-ME-Proxy-Cause: gggruggvucftvghtrhhoucdtuddrgedvhedrfedtgedguddvgecutefuodetggdotefrod ftvfcurfhrohhfihhlvgemucfhrghsthforghilhdpqfgfvfdpuffrtefokffrpgfnqfgh necuuegrihhlohhuthemuceftddtnecusecvtfgvtghiphhivghnthhsucdlqddutddtmd enogfuuhhsphgvtghtffhomhgrihhnucdlgeelmdenucfjughrpefhvfevufffoffkjghf gggtgfesthhqmhdtredtjeenucfhrhhomheplfhonhcuufhtvghrlhhinhhguceojhhonh esjhhonhhmshhtvghrlhhinhhgrdgtohhmqeenucggtffrrghtthgvrhhnpeduhfelhfeu geevvddttedvhedttdejuddutdevkeehgfdttdekleelveevheejudenucffohhmrghinh epghhoohhglhgvrdgtohhmnecuvehluhhsthgvrhfuihiivgeptdenucfrrghrrghmpehm rghilhhfrhhomhepjhhonhesjhhonhhmshhtvghrlhhinhhgrdgtohhm X-ME-Proxy: Feedback-ID: if544409e:Fastmail Received: by mail.messagingengine.com (Postfix) with ESMTPA; Fri, 21 Apr 2023 14:30:52 -0400 (EDT) From: Jon Sterling To: David =?utf-8?q?W=C3=A4rn?= Cc: homotopytypetheory@googlegroups.com Subject: Re: [HoTT] Free higher groups Date: Fri, 21 Apr 2023 20:30:39 +0200 X-Mailer: MailMate (1.14r5895) Message-ID: In-Reply-To: References: MIME-Version: 1.0 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable X-Original-Sender: jon@jonmsterling.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@jonmsterling.com header.s=fm1 header.b=V1y1Osav; dkim=pass header.i=@messagingengine.com header.s=fm3 header.b=GzvjvubV; spf=pass (google.com: domain of jon@jonmsterling.com designates 64.147.123.19 as permitted sender) smtp.mailfrom=jon@jonmsterling.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: , Dear David, Congratulations on your beautiful result; I'm looking forward to understand= ing the details. Recently I had been wondering if anyone had proved this, a= nd 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 sy= nthetic homotopy theory: the free higher group on a set is a set. > > The proof proceeds by describing path types of pushouts as sequential col= imits of pushouts, much like the James construction. This description shoul= d be useful also in many other applications. For example it gives a straigh= tforward 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= email to HomotopyTypeTheory+unsubscribe@googlegroups.com. > To view this discussion on the web visit https://groups.google.com/d/msgi= d/HomotopyTypeTheory/f2af459c-53a6-e7b9-77db-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/D102F774-D134-46B9-A70A-51CB84BE4B6F%40jonmsterling.com.