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 14908 invoked from network); 22 Apr 2023 00:25:10 -0000 Received: from mail-wr1-x43f.google.com (2a00:1450:4864:20::43f) by inbox.vuxu.org with ESMTPUTF8; 22 Apr 2023 00:25:10 -0000 Received: by mail-wr1-x43f.google.com with SMTP id ffacd0b85a97d-2fe3fb8e32asf872003f8f.1 for ; Fri, 21 Apr 2023 17:25:10 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1682123109; cv=pass; d=google.com; s=arc-20160816; b=pCw86fu8LrSs2qCT3o1eUZxgpnstVoel96egrSXOqjmcByczX9K9Lrzh+e7j/ThUjt X/+jdcPGwRC9/xYHovDVG5ciVvRSOKCcgwNykNNIVGlAEtLHL4+FyOtyNk5/577v2J0L XWAxCeyg9RiCtsUozvrFwddmk7BSdaCoPXLucnv2BnxGFHDRe7lxZJNA34cHFcVLLUTN IvP7l5Ja5kYUULVaVC2vHwZF/bcnxaoYPUR7t4ZBtHPI+penQwniZDa+ekrO8NvRTy/S DBhRXsNfcy65wBDvNF87Gib2TTbx/d3P4MpwFZjjNFcuouGr1tUB7h244QuFdYjt11Rj Fhbw== 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=N0GRvDUFBGFKnDTXDi7hHSfht5WRymq8TmXuS75mYUk=; b=VJfenljs+ePwJhCGIkaPE4en6gkgPYUFK/4iRD8mdMnPS6eK15GYLoVq7UOEZEgJf5 4io1L1tFbeXGXjhBFWXg99uiD1quA85uE8drftYQxDP9DiXivyLCm0Yx2AF92mphPIw0 r0yFwV0PRP0sEyS1JQ3gpCHYWLdKG2fTcRaEZibVu4K09AZfW9OdWFYCndbAQb5QmCV8 ZWr1BoKQYa9BtDBnHwih0qB9LqgZkCrN5MMIDasLZpMScaXbeNYS57oFFQRiHMLge/6M V2g0lAeq7Y7b6g5m+WQYTRQBdtMb1oebamhjBQp6qS3q12AKuz/ayR1fcF1668M/khJp EVGA== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20221208 header.b="Ow/wep06"; spf=pass (google.com: domain of nicolai.kraus@gmail.com designates 2a00:1450:4864:20::52b as permitted sender) smtp.mailfrom=nicolai.kraus@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=1682123109; x=1684715109; 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=N0GRvDUFBGFKnDTXDi7hHSfht5WRymq8TmXuS75mYUk=; b=VjrWBlZHwyWJlVXn0C13wRLw8pp6F50LDkm1JX3INV+xdxuvW7UAvC1/NNBE0Q4SKE RjyGchxgMz/eHjtOhqnmnpAOxSMrgFhGYiJ58ZbSReknDWObyfO98yzluWmmWNanMWFE idqnppg4ySdwAt+VB5CEp/TLHepEniXausV9S1mWHwZXoOOF2CIdXnz40qsaoD4Gc3xj TZPdQqrj1hozkrZPCMBbdgj3Z1mmHAbgl5Ml+z5/KKT3r9dh6B8QBwRBzsPFrWTfK2j+ Zpu99V4Epmp7I4z4aTIkU/lUArj1uN2ToOf9VK3QbpF8ICv+wjBjU4Dpn0onOgaTUtwo +33g== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20221208; t=1682123109; x=1684715109; 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=N0GRvDUFBGFKnDTXDi7hHSfht5WRymq8TmXuS75mYUk=; b=aPsue87F0uUGVU/n/cQY0hhMGopNsgWv7SxCmHygo7uFu1S2n2QgNCv2b5EtDw1sJl d0Q+QXie72TmputRSSRQHLh9qAl6JMmIreHheyXhVtAoVLQUjCRneCBmDpN904319SeR LZYifWG9GEgrI/lhH7dHjCAyhbcTaNbBN2RggANkVoCbXks9zrM0PL4qn9GfBYO366qb SG2PWrVvQ6A6m7tCDKyLyCRJrINuYO6Iq/tVGZryC1WqMHWIzitdv05+2BC+GHcvYykd WzsMvBD/G/h7prXjCT5+pWGFqC82s5rIzeBFGAhhERBpwaYV7UNVReK16g7b8TkCsT/D oumA== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20221208; t=1682123109; x=1684715109; 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=N0GRvDUFBGFKnDTXDi7hHSfht5WRymq8TmXuS75mYUk=; b=fYvyvQeOdxr4d0M5CVPRRWGRBxDML8K5RMxEpXrIAKoRcwg2t/Sg64LnkQ7Bcsu04F LTfWCTBAiuf9O9+jHA8VDYG08zpUEj/K2bp78M3BpK9m4g4yYB1WCEfvslOLM5wWUn8W IqL/4/wvfqGhnq7bzF0RQXKi0wcfd7wQ2IhlWaIYQDkTIFOyZYP3chI9Q8KFib5S7EwQ 7xw3zfd3uuzECCrJ7H8YKJsMC+RUqD9WJQk80tGMhCSiFkBc9mYSLFmpV94zPsiyHx+8 Cj1jIhsiLxiet9U8TK8HrgYcw3ZMTPCqC0XVgd70SIAg9e6cQZLfnH6+euL4AumpWKMU 8vNA== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AAQBX9eISglcpeGaWCZIIr6TbJLjI4MDuAPF096EOBOsZAdgPwQB9wX9 yWM4A/xjbghIwfsK77j8mD4= X-Google-Smtp-Source: AKy350aW3Xy6ulGU/fSc3NUGeOjxwTxBksiDQmzfqec5fHK4Tiu//3AxD+2epqXOW+otPl+yg/EZ+Q== X-Received: by 2002:adf:fa42:0:b0:2ef:b5a2:50cb with SMTP id y2-20020adffa42000000b002efb5a250cbmr1145601wrr.0.1682123109481; Fri, 21 Apr 2023 17:25:09 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a5d:4d8a:0:b0:2f4:1b04:ed8f with SMTP id b10-20020a5d4d8a000000b002f41b04ed8fls9153019wru.1.-pod-prod-gmail; Fri, 21 Apr 2023 17:25:06 -0700 (PDT) X-Received: by 2002:a05:6000:1c9:b0:2ff:a878:2de9 with SMTP id t9-20020a05600001c900b002ffa8782de9mr4854052wrx.21.1682123106669; Fri, 21 Apr 2023 17:25:06 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1682123106; cv=none; d=google.com; s=arc-20160816; b=ZnE7EHugqRhW+Ixi/Y3lg7J2X/HSeLSavOmhilBd0xfQif7kdd9UOaj+H7umNdHXSb 78VCjTFidCKhgITaClc3ZnZ97aiT/y7l9Sr5z9CeHNO+UwccbjFlmcaOj24Uhf6Cdrhq sA4QmNF9IAb2VMix4gxsWE/9X8dvNKkjKwD4+ryc6XylxHPF7FOB+x6rfznxNyDCE8jd 4WeKmJM1+iZ/bXX0ULPtTIRh/btYcuUyQTKnBnmIIZtdDfIYneI64VkQ3dCw0b8Z/Obg kdvlXyef0UpbF+noTfcYspWHDzAsvYl8Px7ueZlkv8ApdKVLj1qR/bchCFaKnoPEkLon QaBA== 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=8LUTDdi723xrepCBok5314ABB1Qh73sB4iE7nnULZdU=; b=xzzVn3oUaOWUqOiEyquNgSVaVVmcdjQcnbYXZeeX/ji937vjtGTBsAVGOW+N26zqIK iYnp0TO93KHBI3mUrdiCmqYDx94kmy3mFcOKUSBZ+FBFkvjmoSxFNkn2jyv7VsZEteW5 eEwI6ehNZhfSsLvngKQJzODQI2XjWE39MN9hvN3vyOI5CLlJuX3Nlb7tPKEDhV6zHXaD C1c4h3PeZ5hxJuvxCVi9E843Y8MCUMXArZHS/EsEpZvscY73b5ttSULtnNzZDRDwJvhk 0065RnsKGjANnoiROQVjzZebgFsmuLiJFWvzsIKlM39SHF0Zrx2rb/xg2og668lyD/xJ yv9A== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20221208 header.b="Ow/wep06"; spf=pass (google.com: domain of nicolai.kraus@gmail.com designates 2a00:1450:4864:20::52b as permitted sender) smtp.mailfrom=nicolai.kraus@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-ed1-x52b.google.com (mail-ed1-x52b.google.com. [2a00:1450:4864:20::52b]) by gmr-mx.google.com with ESMTPS id p12-20020a05600c1d8c00b003f17514c7b3si138233wms.1.2023.04.21.17.25.06 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Fri, 21 Apr 2023 17:25:06 -0700 (PDT) Received-SPF: pass (google.com: domain of nicolai.kraus@gmail.com designates 2a00:1450:4864:20::52b as permitted sender) client-ip=2a00:1450:4864:20::52b; Received: by mail-ed1-x52b.google.com with SMTP id 4fb4d7f45d1cf-506b20efd4cso3807421a12.3 for ; Fri, 21 Apr 2023 17:25:06 -0700 (PDT) X-Received: by 2002:aa7:c316:0:b0:508:4cd8:aa64 with SMTP id l22-20020aa7c316000000b005084cd8aa64mr6292103edq.31.1682123105790; Fri, 21 Apr 2023 17:25:05 -0700 (PDT) MIME-Version: 1.0 References: In-Reply-To: From: Nicolai Kraus Date: Sat, 22 Apr 2023 02:24:54 +0200 Message-ID: Subject: Re: [HoTT] Free higher groups To: homotopytypetheory@googlegroups.com Content-Type: multipart/alternative; boundary="0000000000003071dd05f9e1ce22" X-Original-Sender: nicolai.kraus@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20221208 header.b="Ow/wep06"; spf=pass (google.com: domain of nicolai.kraus@gmail.com designates 2a00:1450:4864:20::52b as permitted sender) smtp.mailfrom=nicolai.kraus@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: , --0000000000003071dd05f9e1ce22 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable 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 > . > --=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/CA%2BAZBBpPwgh1G9VZV0fgJFd8Mzqfchskc4-%2B-FXT42WQkzmC9w%= 40mail.gmail.com. --0000000000003071dd05f9e1ce22 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Hi David,

Congratulations (again)! I fi= nd it very interesting that this question has a positive=C2=A0answer. I had= suspected that it might separate HoTT from Voevodsky's=C2=A0HTS (aka 2= LTT with a fibrancy assumption on strict Nat). Since this isn't the cas= e, do we know of another type in=C2=A0HoTT that is inhabited in HTS, while = we don't know whether we can construct=C2=A0an inhabitant in HoTT?
=
Best,
Nicolai
=C2=A0
On Fri, = Apr 21, 2023 at 8:30=E2=80=AFPM Jon Sterling <jon@jonmsterling.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%2BAZBBpPwgh1G9VZV0fgJFd8Mz= qfchskc4-%2B-FXT42WQkzmC9w%40mail.gmail.com.
--0000000000003071dd05f9e1ce22--