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,MAILING_LIST_MULTI,RCVD_IN_DNSWL_NONE, T_SCC_BODY_TEXT_LINE autolearn=ham autolearn_force=no version=3.4.4 Received: (qmail 9427 invoked from network); 29 Apr 2023 18:38:10 -0000 Received: from mail-il1-x13f.google.com (2607:f8b0:4864:20::13f) by inbox.vuxu.org with ESMTPUTF8; 29 Apr 2023 18:38:10 -0000 Received: by mail-il1-x13f.google.com with SMTP id e9e14a558f8ab-32f23e2018fsf115414845ab.0 for ; Sat, 29 Apr 2023 11:38:10 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1682793488; cv=pass; d=google.com; s=arc-20160816; b=AVXly4s5hzdukOtF3eo+hv6DkuNEpIxUdCEJh2xjRw5GxxIONTIdQYqveglhg4xSrE QnD0xVLZTSpbnU0mozXBPGk0tWmWWAWlIBiVURKBouvFXMRKvTed6Z6N8AwjBNgXh2oa +5fALOUBBg6aG8vCvAETMvKxVK3H9ZMBujD/+AnF7caY0u5k9BbYoddbQECi0uleVmmv dqvkK9IY90wKI9FSYUA/e1u40Cy8W5OMQMjk6y1yBT+a7rzZYIUg1qNqqYdC1EWC3o3B 3seA7WhSMIg3Z/j0Z1Y4uZ3hhmaUIQSTOlKRu1ePVKW+UN160Akw6ZdQCgwha2EnN1Id wu9w== 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:references:message-id :content-transfer-encoding:cc:date:in-reply-to:from:subject :mime-version:sender:dkim-signature:dkim-signature; bh=NWlIu9gcEPfm89ESpd6h8JkD6XNFpHtpqUX3O3zSEyY=; b=sfUDRj8atb6eIbIq1WgDep0E1tCtfrVFq9HpCpppOCtjcfuNsZnYqcEfKNRiqclowX dpqnXGndWQfKM+cznVZuwAtG0cnw3XHna8QVatYVbjqUF7wVoSxl2VZaiBBhwprT3tUa b16+zX8nCZuM9YDGHwvlCDM0AMIqqsKqb3EM3yD1lKAWe8pplRUg15t+dh663EFgb4LV 0Fk6z4MtUNrO7V8qU27JpkB6MiepXQti8UYdRR3RPZQGVyg3GepR3cNdiGSsh7yII6EB 7vh58Qcm8JokOk1R3gy8KxU21WrY9OjW0KqU+MVMGFkxqDwt0UpGSKG340fsyDEU/DgC 3Mvw== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20221208 header.b=a8oVGl+N; spf=pass (google.com: domain of steveawodey@gmail.com designates 2607:f8b0:4864:20::72f as permitted sender) smtp.mailfrom=steveawodey@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=1682793488; x=1685385488; h=list-unsubscribe:list-subscribe:list-archive:list-help:list-post :list-id:mailing-list:precedence:x-original-authentication-results :x-original-sender:to:references:message-id :content-transfer-encoding:cc:date:in-reply-to:from:subject :mime-version:sender:from:to:cc:subject:date:message-id:reply-to; bh=NWlIu9gcEPfm89ESpd6h8JkD6XNFpHtpqUX3O3zSEyY=; b=P49nonFnb4+tJ5gDgtP1IQl8OIuczQR/9YC3t2u+LjcdAcWrGwID8lCCiaA/00gAgX dqA4nqJiaoJJMyPCfhzR8SN6mZQEiPoGiY3G2OgaT1Mf3tl5jl3jS4weTAUc6UbjSmtK x/chAMGcpPLcMeNtwUnKbecjE4Rk+DZJDwtUC/pPUg7sjsNFFKIJiynBiul/iMAblvbV C9ZjsVrRcfcNJrZpCRCO+tC/tVuliE/fX9LIun8BKX37CvR/JRuENT5SKp1+P/RMZ2P8 vD9FMKrX91z5goBkUjd3KbY8Bqktx6AgRtBml5gG6kzLDTzIWF5gxZCtLuwVoCqhQ8gE KY9A== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20221208; t=1682793488; x=1685385488; h=list-unsubscribe:list-subscribe:list-archive:list-help:list-post :list-id:mailing-list:precedence:x-original-authentication-results :x-original-sender:to:references:message-id :content-transfer-encoding:cc:date:in-reply-to:from:subject :mime-version:from:to:cc:subject:date:message-id:reply-to; bh=NWlIu9gcEPfm89ESpd6h8JkD6XNFpHtpqUX3O3zSEyY=; b=syxgHcHsAlgXY8P6pWiS3N9YERUq6gqNO93b+SpybuERdJlwDqBczZIAKw5g4qtHLZ f8Thtd6mB0Cfv8iGFoKXT7RMO+b9aGPfVsvyO7uA3G9PtmgoTV0MdPIXomyco2vEE1mm gUwXalYQHzh19fzg4/bP/lscvBX/+m+FXAs9AfdFsFQBeFNPh6br1FQv8+eVf0Nc3tQ2 tykW50buj8hntonI1m69tWIsP7vu6WpcHShccCJZ609nBIAKZHE14kyWM3zpLNrBZWtN jYoIsyXdk4/2UPG8qmIwdR/GoCR1MIiVW0SZJobEsWVjcvmnbUhrXj9rfdz5i6WzbtkB 3aHg== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20221208; t=1682793488; x=1685385488; 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:references :message-id:content-transfer-encoding:cc:date:in-reply-to:from :subject:mime-version:x-beenthere:x-gm-message-state:sender:from:to :cc:subject:date:message-id:reply-to; bh=NWlIu9gcEPfm89ESpd6h8JkD6XNFpHtpqUX3O3zSEyY=; b=iVsnk17XcbZCBLZHjD0TAtIM0peYR2wOF2QNqQZxH8695Kjld+J3x4rkgOKwDApmVs QryV1VB0U5Frsrn5meVDiZxs6xa4/67yd8makDXoJObPHpcYaOTF6t35jlSHe5dkqCrI mUdlGRbQvBigVlI1dfIZAJ1khsxz+XRNpFFQyORCJbxmCN/XaKamFOwf5Bz0yI3ar4sS XjrOv5WLWvoBTd9xJblOlJaCJ9z6TQeolK16B9h4ZlVuHxCumI2pVcjjfMS1bzQjCc33 YjdCkGgQVsOmdYdR2jcK0fNxplN4xF3xM/9OfYcDyLGJOmxlC6v6hOIyMd2xHyrzBEhl noDg== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AC+VfDyRAlXP9TYLBRU9TFxIhmLTMYRq0UeT3vxG/hdNIwSZUAmjqSBI FfNnEa4Z8UoWYeLWo1OwP5s= X-Google-Smtp-Source: ACHHUZ6jL1utJCuM1qzKX69J/ZmQIU/lsZl2d8RDqq3kKpp2Kt1pZuntLHbwBGvrZrIzycQCGw3/QA== X-Received: by 2002:a92:b09:0:b0:32c:b806:d4a3 with SMTP id b9-20020a920b09000000b0032cb806d4a3mr5162527ilf.1.1682793487898; Sat, 29 Apr 2023 11:38:07 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a92:cdac:0:b0:32c:c37c:51ab with SMTP id g12-20020a92cdac000000b0032cc37c51abls2200191ild.8.-pod-prod-gmail; Sat, 29 Apr 2023 11:38:06 -0700 (PDT) X-Received: by 2002:a92:b04:0:b0:32b:4cdc:d0cf with SMTP id b4-20020a920b04000000b0032b4cdcd0cfmr6130969ilf.3.1682793486520; Sat, 29 Apr 2023 11:38:06 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1682793486; cv=none; d=google.com; s=arc-20160816; b=b0NGw85U5c5RU/uzEuJRCwiDktqaSwgf6p85km2+CGGcru4aqy4vi4spBlbYTJJw26 bMfa9OOEiOPfPkWw8kSGr8hqqLn7zWWH/dFMJntDPQDQWDEfl1s3rCEJmSvHJ3tNMOu1 ckoQDhB3zufU7NIA0++uLKNKitGQFz5fSpE/W7zJcjVLkGeuexetFVjXqKxXIVpFo8uJ SSuUz2zCDFih+L/rPzbNZUx3yownZyMnT2yWEOwEmNKQwLhPKAIBfsdqRyUb8YvXnWlw dK6NjbqaqHEoEBP5GOXo39g3xvUD4oorpu1oNPaV5/tgtJVrvGwMD+9r09pqQN59C3ST LAVA== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=to:references:message-id:content-transfer-encoding:cc:date :in-reply-to:from:subject:mime-version:dkim-signature; bh=U2980NlBnUdQ37aANiRY7MUwlpHZJ66EgvJJnMd6Vhg=; b=twg/aROhXPD2G5RI2ldHufdgn6GfGU06fDKFyeLDb7Oc0sgHFL1gMdsZtTq14qWy98 BrUErdBYhXcCy7ooDU4vA5f6CYxybZ2gydiRqdwB+POVaksdKpXCCGFFrhqFljkG+ptT yCo8PU+2gGrzIxSgshh6uL8j1Gktks6aowxt3oTbaEjPSJKdvbixM7IDF08plL4LzYGp Ebpkco/nS5FIYTLnrXZyulK+yjOcNjVXAS8DTceA32owimJ0+qwE6bLdK3SjOM8+IEf5 sB85iJd1D3gTDHG5zhtWspRpnlsSyFs4cd64HaE/OMhEABTdJ4LiWa+GfbFlcqH0YW1Z knBg== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20221208 header.b=a8oVGl+N; spf=pass (google.com: domain of steveawodey@gmail.com designates 2607:f8b0:4864:20::72f as permitted sender) smtp.mailfrom=steveawodey@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-qk1-x72f.google.com (mail-qk1-x72f.google.com. [2607:f8b0:4864:20::72f]) by gmr-mx.google.com with ESMTPS id bi13-20020a05663819cd00b00409125e3b19si1815357jab.2.2023.04.29.11.38.06 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Sat, 29 Apr 2023 11:38:06 -0700 (PDT) Received-SPF: pass (google.com: domain of steveawodey@gmail.com designates 2607:f8b0:4864:20::72f as permitted sender) client-ip=2607:f8b0:4864:20::72f; Received: by mail-qk1-x72f.google.com with SMTP id af79cd13be357-74e00fcdec6so51626085a.1 for ; Sat, 29 Apr 2023 11:38:06 -0700 (PDT) X-Received: by 2002:ac8:5cd1:0:b0:3ef:3c30:9838 with SMTP id s17-20020ac85cd1000000b003ef3c309838mr16196339qta.23.1682793485839; Sat, 29 Apr 2023 11:38:05 -0700 (PDT) Received: from smtpclient.apple ([2607:fb90:379:3c42:d9ae:2067:d3ee:fd2c]) by smtp.gmail.com with ESMTPSA id o10-20020a05620a110a00b007513b8254easm1787844qkk.68.2023.04.29.11.38.04 (version=TLS1_2 cipher=ECDHE-ECDSA-AES128-GCM-SHA256 bits=128/128); Sat, 29 Apr 2023 11:38:05 -0700 (PDT) Content-Type: text/plain; charset="UTF-8" Mime-Version: 1.0 (Mac OS X Mail 16.0 \(3731.500.231\)) Subject: Re: [HoTT] Free higher groups From: Steve Awodey In-Reply-To: <87zg6qy4gx.fsf@uwo.ca> Date: Sat, 29 Apr 2023 14:37:54 -0400 Cc: "homotopytypetheory@googlegroups.com" Content-Transfer-Encoding: quoted-printable Message-Id: <21ED9406-6C3A-4B26-A74B-34C2821C97B6@gmail.com> References: <87leigyeya.fsf@uwo.ca> <87zg6qy4gx.fsf@uwo.ca> To: Dan Christensen X-Mailer: Apple Mail (2.3731.500.231) X-Original-Sender: steveawodey@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20221208 header.b=a8oVGl+N; spf=pass (google.com: domain of steveawodey@gmail.com designates 2607:f8b0:4864:20::72f as permitted sender) smtp.mailfrom=steveawodey@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: , good one! How about just covering a type by a 0-type? Steve > On Apr 29, 2023, at 1:37 PM, Dan Christensen wrote: >=20 > Another set-level statement is whether there are enough injective > abelian groups. It's true in Grothendieck oo-toposes, but presumably is > not provable in HoTT. >=20 > Dan >=20 > On Apr 28, 2023, Michael Shulman wrote: >=20 >> The existence of hypercompletion is a good suggestion. >>=20 >> Also I realized there are set-level statements that are already known to= be >> true in all Grothendieck 1-toposes but not all elementary 1-toposes, suc= h as >> WISC and Freyd's theorem that a small complete category is a preorder. = So >> those will be true in any Grothendieck oo-topos too, and can be presumed= to >> fail in HoTT. But it's nice to have one that involves higher types too. >>=20 >> On Mon, Apr 24, 2023 at 5:37=E2=80=AFPM Dan Christensen wro= te: >>=20 >> A not-so-interesting answer to Mike's question is the type of deloopings >> of S^3. The reason this isn't so interesting is that it's in the image >> of the natural functor from Spaces to any oo-topos, so it's true just >> because it is true for Spaces. Similarly, a statement asserting that >> pi_42(S^17) =3D (insert what it is) is true in any oo-topos. Another >> reason these aren't interesting is that I expect that they are provable >> in HoTT with enough work. >>=20 >> So, I'll second Mike's question, with the extra condition that it would >> be good to have a type for which there is some reason to doubt that it >> is provably inhabited in HoTT. >>=20 >> Oh, what about whether the hypercomplete objects are the modal >> objects >> for a modality? I'm throwing this out there without much thought... >>=20 >> Dan >>=20 >> On Apr 24, 2023, Michael Shulman wrote: >>=20 >>> 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. >>>=20 >>> 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? >>>=20 >>> On Fri, Apr 21, 2023 at 5:25=E2=80=AFPM Nicolai Kraus >>> wrote: >>>=20 >>> Hi David, >>>=20 >>> 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? >>>=20 >>> Best, >>> Nicolai >>>=20 >>> On Fri, Apr 21, 2023 at 8:30=E2=80=AFPM Jon Sterling >>> wrote: >>>=20 >>> Dear David, >>>=20 >>> 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. >>>=20 >>> Best wishes, >>> Jon >>>=20 >>> On 21 Apr 2023, at 12:04, David W=C3=A4rn wrote: >>>=20 >>>> Dear all, >>>>=20 >>>> 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. >>>>=20 >>>> 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. >>>>=20 >>>> Best wishes, >>>> David >>>>=20 >>>> --=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 >>>=20 >> https://groups.google.com/d/msgid/HomotopyTypeTheory/f2af459c-53a6-e7b9-= 77db-5cbf56da17f3%40gmail.com. >>=20 >>>=20 >>> --=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 >>>=20 >> https://groups.google.com/d/msgid/HomotopyTypeTheory/D102F774-D134-46B9-= A70A-51CB84BE4B6F%40jonmsterling.com. >>=20 >>>=20 >>> --=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 >>>=20 >> https://groups.google.com/d/msgid/HomotopyTypeTheory/CA%2BAZBBpPwgh1G9VZ= V0fgJFd8Mzqfchskc4-%2B-FXT42WQkzmC9w%40mail.gmail.com. >>=20 >> --=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/msgid/HomotopyTypeTheory/87leigyeya.fsf%40uw= o.ca. >=20 > --=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/87zg6qy4gx.fsf%40uwo.ca. --=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/21ED9406-6C3A-4B26-A74B-34C2821C97B6%40gmail.com.