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,T_SCC_BODY_TEXT_LINE autolearn=ham autolearn_force=no version=3.4.4 Received: (qmail 11591 invoked from network); 29 Apr 2023 19:22:32 -0000 Received: from mail-oa1-x3b.google.com (2001:4860:4864:20::3b) by inbox.vuxu.org with ESMTPUTF8; 29 Apr 2023 19:22:32 -0000 Received: by mail-oa1-x3b.google.com with SMTP id 586e51a60fabf-192517edb39sf8122fac.2 for ; Sat, 29 Apr 2023 12:22:32 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1682796150; cv=pass; d=google.com; s=arc-20160816; b=e+ZJTqH27G4PKi8OL/0c+NBnmgf23MyfIGgBtFqzmdZm0bafGc+D3/mRCL8r2LJ7dA bcbocfXGcCf1Wc/wka4kqZPomouo/V38F2/ZsOkzW+6ferb8048BSEWBaACRJe9wvfJM LJiSJq/ZfY2a1n3m2Lkc6GxgQN0gmMHVqSevAMwvOU7Yy12JR7vOnp1z99SDQWYriL+x HB8VcVDGxnRRthPX4a2+UyGRxz4JgKmnrD7sTn3yDm+SKr3MgJzEccJXuHPXr5knngkA u3NCCyKHYCVSBiih0JKrCiPU4189fTUgSYyEl1tbxETldVdK2nkq86Vz2NwCq+/3qEnu 4fSw== 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:references:to:cc:in-reply-to:date :subject:mime-version:message-id:from:sender:dkim-signature :dkim-signature; bh=H5Z9pIDOF13Ut6nY0q9a88UcQJvVtuDM1KGR2rwFZ04=; b=TDsCHlYlIIhYaLG+MoiEcDuk93VS0ZZk8vRKndvS/5JSMo/ml0NS2A14gdi3TKAIZx 2baPVIolinrh3x8/tC7xG6LMWdgxP8Fws7vrDnB7+IHIZTwPbKYYoYGKWIjV2CIv3CWk t7w9z9WPybtmtR5QhGBtRfny8DFwo2C82hNtT5G7ofID9TtCY91NZm8aQk3vk/hD0Iqo Au5zk/GLyOhzjo/O7fLjKhTZHVgFGEjhfZQpadZWW9we1tmVPhnKUIDljU4rATMx38mk FPcwaZWhKTawL4WWhLrS75TVruiX1dvdTjtsBoA16lTbthqRMyqSXWU4F0L4hJvI8qR1 UmQw== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20221208 header.b=ZUeqXia4; spf=pass (google.com: domain of steveawodey@gmail.com designates 2607:f8b0:4864:20::734 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=1682796150; x=1685388150; h=list-unsubscribe:list-subscribe:list-archive:list-help:list-post :list-id:mailing-list:precedence:x-original-authentication-results :x-original-sender:references:to:cc:in-reply-to:date:subject :mime-version:message-id:from:sender:from:to:cc:subject:date :message-id:reply-to; bh=H5Z9pIDOF13Ut6nY0q9a88UcQJvVtuDM1KGR2rwFZ04=; b=YfWplz6UmL8wUMOAFxhXsQrmqyiJHtI5eEncWWRsW06KeQPrP17c5rAPuz4lnqS+6q mt4tKl80Gde5fXHoJul69RtEF6hM1JJLVUAB7ecNDCDKi4PnYohxtM6RzdzTJ2FDMIFG YDWEw2ieuIrV5Uw5A3BO0mXVv7D8I1t5WnNTWR6JkFAgbb+LJpdD3ufoCRmUZBbH20oZ EZKPZpXTVvdHpcT+XAp+caLLvDfVD2r59e6ZJIYdsszApiqkXFeZHepcyQqYDV7k0Va/ O0iQyLJ+cB7iKCAfWxnIoUElUwEKAwv8H7aWwqD4gYJbz3B5FRploIBOw5aMps47lHqN utbg== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20221208; t=1682796150; x=1685388150; h=list-unsubscribe:list-subscribe:list-archive:list-help:list-post :list-id:mailing-list:precedence:x-original-authentication-results :x-original-sender:references:to:cc:in-reply-to:date:subject :mime-version:message-id:from:from:to:cc:subject:date:message-id :reply-to; bh=H5Z9pIDOF13Ut6nY0q9a88UcQJvVtuDM1KGR2rwFZ04=; b=QtOLJvqmIXKCPNl7Xxp+YXeJuWKxuE0EjabSl1Xjsxs009E5MDl1DvsyWqFcGIr17y X9azwnbJCiHpUInEZPBnYK1ndSiHDQq+/krh0Nfwfb1JPKZVPF0l7BL6TkrJrLrJ3hZG DQp2lEYGEjvHoFMHZ/vfa3JUdbnsIyBJ8RHNozZ6fmLrQb7NoN1qlse/VRnLZ0rL8VKQ 6kkd8SwHNoXIkAvNbjJGXxGECOwTctisXCzG0E3qJIUVQOTcWPbKXths33gIWei0LUJ0 4SbZPzcTrIyqUXidzDM98Fhdl+JN8noAaME7yA48CUm026rTPk6upbE9TZc4sR7YfBc+ 14xw== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20221208; t=1682796150; x=1685388150; 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:references:to :cc:in-reply-to:date:subject:mime-version:message-id:from :x-beenthere:x-gm-message-state:sender:from:to:cc:subject:date :message-id:reply-to; bh=H5Z9pIDOF13Ut6nY0q9a88UcQJvVtuDM1KGR2rwFZ04=; b=HbcBaCiNdIO3O+drrz7mlkWRvunBwrPR/4Nmf66SP4DIjYI8EI2T4NQcYd31CTFFFx UIdDIRXb446qM0VXzg2zVz3XwVhhkFquwgeTLmRqQrJEvX+TUyFcmAA6lWYUtAAo/n46 f4i95acOYxNFnAabrEnN8UMi21Fw5TeejxNDSX8s4daFX1EFfa9t8CXLTs0KKI5As6DX cgXdItuQWkZyiMOonfUTZMm1jUcFjIkjXVh+tSZJ+J3tD2ZY5vwJj9YDsQJY8abW1ohq 6nYbc4BaSXGEsnQVAmqMCAqY40Ql7DXu6kYOYr8UxOK3R1N/2Tt4ytlZbxSxat+gfTHa kkxA== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AC+VfDwfalnHkzAWQT+yFQ1qIgqoXLwnbrtYb9p/dOu+Na33P/Lg9SPf WCgqnPqMu8VE9NZ2HpEDX80= X-Google-Smtp-Source: ACHHUZ7pNL0wo01XUEvmnBDmqzkIoZIeDCYxHtJOKuXWGjkMozIiuk91uoVrApfeSTBxY/QCiKbT7w== X-Received: by 2002:a05:6870:12cf:b0:18e:34ac:fcda with SMTP id 15-20020a05687012cf00b0018e34acfcdamr2089890oam.6.1682796149630; Sat, 29 Apr 2023 12:22:29 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a05:6870:9b08:b0:16d:c495:95f9 with SMTP id hq8-20020a0568709b0800b0016dc49595f9ls2278819oab.0.-pod-prod-gmail; Sat, 29 Apr 2023 12:22:28 -0700 (PDT) X-Received: by 2002:a05:6870:1d0e:b0:184:af3:910d with SMTP id pa14-20020a0568701d0e00b001840af3910dmr6299434oab.32.1682796148518; Sat, 29 Apr 2023 12:22:28 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1682796148; cv=none; d=google.com; s=arc-20160816; b=FTgzqXtAnpGg4GNFYNQYpUDAZvV/m1FdJ78IKgkefhOAI5g4b5YE0alqB3gXDxRrXo yYxOq4x7laUCzhjwMdX5AVIiLKY/yTR9rraWBfa2c4E4f4Sp1lz6RpylihQ1TinBGIt4 V1/FC7KayF/8s8YYDU7ZjIUlz8GZDZ25SX9x1xYmnGg+J/ZshQy19pghrXGZJj9VtF3g yINoW6cw0d68qfi4NCo8Cq2bkrcF3BxwMq7TnnCOKY+dDU+u6ZbVPV4gQYy1T00drNSb PZPFB0j3WUZf3s6CZXCOl0fWWdf+xzU5076MQH/O9vyQAfd40Gg+kyHjM9qT64IGGN2s 64fA== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=references:to:cc:in-reply-to:date:subject:mime-version:message-id :from:dkim-signature; bh=LvNmaWyTz8vuZuqnyDx/wk/KG1RolpdBkm4HYYmcl/0=; b=L1bGU3imEqqOEfu85yMvnp0U0zL97bIv2wH8HPou4p14EKRQJ20p69HSk+TWK6JBSJ LhzgCBUrdarnPbuW935nrj86v7undRPhMRi3j6eOnW5LCWbDmKXCODZ7K7PuGxlbGQHI GR2vyKOoEWEIZ9zNmkg0EntN0XmdrzWS8+Vx2OS2u36Sd84o06Z0aliDmUHF5DAwPaSc sz1q7qWhw4SxczCWVSP83wWC6YlSahMR2blqiwd9pkxw3XO45PeB3G8hiJxqnFqiCnCp gXn2j5JVMHv6hUPKIY1xuDsDz+sisA3ZCEcL2h+QJhXXJBQ/Suq78hbSg77ZGEFhTMdY n5Jg== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20221208 header.b=ZUeqXia4; spf=pass (google.com: domain of steveawodey@gmail.com designates 2607:f8b0:4864:20::734 as permitted sender) smtp.mailfrom=steveawodey@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-qk1-x734.google.com (mail-qk1-x734.google.com. [2607:f8b0:4864:20::734]) by gmr-mx.google.com with ESMTPS id bm7-20020a056830374700b006a42f0f76f4si2014195otb.2.2023.04.29.12.22.28 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Sat, 29 Apr 2023 12:22:28 -0700 (PDT) Received-SPF: pass (google.com: domain of steveawodey@gmail.com designates 2607:f8b0:4864:20::734 as permitted sender) client-ip=2607:f8b0:4864:20::734; Received: by mail-qk1-x734.google.com with SMTP id af79cd13be357-74fc1452fbdso88162785a.2 for ; Sat, 29 Apr 2023 12:22:28 -0700 (PDT) X-Received: by 2002:a05:622a:5cc:b0:3ef:3d98:ce78 with SMTP id d12-20020a05622a05cc00b003ef3d98ce78mr14121929qtb.66.1682796147752; Sat, 29 Apr 2023 12:22:27 -0700 (PDT) Received: from smtpclient.apple ([2607:fb90:37c:ea26:cc4b:eeb5:9b0e:9b25]) by smtp.gmail.com with ESMTPSA id ey19-20020a05622a4c1300b003ef324c6fa3sm7479826qtb.52.2023.04.29.12.22.26 (version=TLS1_2 cipher=ECDHE-ECDSA-AES128-GCM-SHA256 bits=128/128); Sat, 29 Apr 2023 12:22:27 -0700 (PDT) From: Steve Awodey Message-Id: <5D0912E6-075B-47EE-87B8-8B5118DDF07C@gmail.com> Content-Type: multipart/alternative; boundary="Apple-Mail=_74E4A905-9946-45BA-BB1F-7A8F733D6D38" Mime-Version: 1.0 (Mac OS X Mail 16.0 \(3731.500.231\)) Subject: Re: [HoTT] Free higher groups Date: Sat, 29 Apr 2023 15:22:15 -0400 In-Reply-To: Cc: Dan Christensen , "homotopytypetheory@googlegroups.com" To: Ulrik Buchholtz References: <87leigyeya.fsf@uwo.ca> <87zg6qy4gx.fsf@uwo.ca> <21ED9406-6C3A-4B26-A74B-34C2821C97B6@gmail.com> 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=ZUeqXia4; spf=pass (google.com: domain of steveawodey@gmail.com designates 2607:f8b0:4864:20::734 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: , --Apple-Mail=_74E4A905-9946-45BA-BB1F-7A8F733D6D38 Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset="UTF-8" Glad I asked - thanks! > On Apr 29, 2023, at 2:49 PM, Ulrik Buchholtz w= rote: >=20 >> How about just covering a type by a 0-type? >=20 > We have countermodels for this, see: https://ncatlab.org/nlab/show/n-type= s+cover#InModels >=20 > A question that came up for me recently is whether we can construct the m= odality for which the acyclic maps are the left class. (This exists in ever= y Grothendieck higher topos. In infinity groupoids, and many, but not all, = models, the right class are the hypoabelian maps.) >=20 > Then there's the question whether every simply connected acyclic type is = contractible. (This is open for Grothendieck higher toposes, AFAIK.) >=20 > These are mentioned in the talk I mentioned up-thread, which also contain= ed the short new proof that the Higman group presentation is non-trivial an= d aspherical (as well as acyclic). The slides are here: https://ulrikbuchho= ltz.dk/hott-uf-2023.pdf >=20 > Cheers, > Ulrik >=20 >>=20 >> Steve >>=20 >>=20 >> > 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, = such 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 presu= med to >> >> fail in HoTT. But it's nice to have one that involves higher types t= oo. >> >>=20 >> >> On Mon, Apr 24, 2023 at 5:37=E2=80=AFPM Dan Christensen > wrote: >> >>=20 >> >> A not-so-interesting answer to Mike's question is the type of deloopi= ngs >> >> of S^3. The reason this isn't so interesting is that it's in the ima= ge >> >> 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 provab= le >> >> in HoTT with enough work. >> >>=20 >> >> So, I'll second Mike's question, with the extra condition that it wou= ld >> >> be good to have a type for which there is some reason to doubt that i= t >> >> 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. A= s >> >>> 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 proo= f >> >>> 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 i= n >> >>> 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 i= f >> >>> 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-e7= b9-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-46= B9-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%2BAZBBpPwgh1G= 9VZV0fgJFd8Mzqfchskc4-%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, sen= d >> >> an email to HomotopyTypeTheory+unsubscribe@googlegroups.com . >> >> To view this discussion on the web visit >> >> https://groups.google.com/d/msgid/HomotopyTypeTheory/87leigyeya.fsf%4= 0uwo.ca. >> >=20 >> > --=20 >> > 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/m= sgid/HomotopyTypeTheory/87zg6qy4gx.fsf%40uwo.ca. >>=20 >> --=20 >> You received this message because you are subscribed to the Google Group= s "Homotopy Type Theory" group. >> To unsubscribe from this group and stop receiving emails from it, send a= n email to HomotopyTypeTheory+unsubscribe@googlegroups.com . >> To view this discussion on the web visit https://groups.google.com/d/msg= id/HomotopyTypeTheory/21ED9406-6C3A-4B26-A74B-34C2821C97B6%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/5D0912E6-075B-47EE-87B8-8B5118DDF07C%40gmail.com. --Apple-Mail=_74E4A905-9946-45BA-BB1F-7A8F733D6D38 Content-Transfer-Encoding: quoted-printable Content-Type: text/html; charset="UTF-8" Glad I asked - thanks!
On Apr 29, 2023, at 2:49 PM, Ulrik Buchhol= tz <ulrikbuchholtz@gmail.com> wrote:

How about just covering a type by a 0-type?

=
We have countermodels for this, see: https://ncatlab.org/nlab/show/n-types+cover= #InModels

A question that came up for me recen= tly is whether we can construct the modality for which the acyclic maps are= the left class. (This exists in every Grothendieck higher topos. In infini= ty groupoids, and many, but not all, models, the right class are the hypoab= elian maps.)

Then there's the question whether eve= ry simply connected acyclic type is contractible. (This is open for Grothen= dieck higher toposes, AFAIK.)

These are mentioned = in the talk I mentioned up-thread, which also contained the short new proof= that the Higman group presentation is non-trivial and aspherical (as well = as acyclic). The slides are here: https://ulrikbuchholtz.dk/hott-uf-2023.pdf

=
Cheers,
Ulrik


Steve


> On Apr 29, 2023, at 1:37 PM, Dan Christensen <jdc@uwo.ca> wrote:
>
> Another set-level statement is whether there are enough injective
> abelian groups.  It's true in Grothendieck oo-toposes, but presum= ably is
> not provable in HoTT.
>
> Dan
>
> On Apr 28, 2023, Michael Shulman <shulman@sandiego.edu> wrote:
>
>> The existence of hypercompletion is a good suggestion.
>>
>> Also I realized there are set-level statements that are already kn= own to be
>> true in all Grothendieck 1-toposes but not all elementary 1-topose= s, such as
>> WISC and Freyd's theorem that a small complete category is a preor= der.  So
>> those will be true in any Grothendieck oo-topos too, and can be pr= esumed to
>> fail in HoTT.  But it's nice to have one that involves higher= types too.
>>
>> On Mon, Apr 24, 2023 at 5:37=E2=80=AFPM Dan Christensen <jdc@uwo.ca> wrote:
>>
>> A not-so-interesting answer to Mike's question is the type of delo= opings
>> 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 j= ust
>> because it is true for Spaces.  Similarly, a statement assert= ing 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 pro= vable
>> in HoTT with enough work.
>>
>> 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 tha= t it
>> is provably inhabited in HoTT.
>>
>> Oh, what about whether the hypercomplete objects are the modal
>> objects
>> for a modality?  I'm throwing this out there without much tho= ught...
>>
>> Dan
>>
>> On Apr 24, 2023, Michael Shulman <shulman@sandiego.edu> wrote:
>>
>>> This is fantastic, especially the simplicity of the constructi= on.  As
>>> Peter said, a wonderful way to commemorate the 10th anniversar= y of
>> the
>>> special year and the release of the HoTT Book.
>>>
>>> Relatedly to Nicolai's question, this question also has an eas= y 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 interpreta= tion in
>>> any Grothendieck infinity-topos is known to be inhabited, but = which
>>> isn't known to be inhabited in HoTT?
>>>
>>> On Fri, Apr 21, 2023 at 5:25=E2=80=AFPM Nicolai Kraus
>>> <nicolai.kraus@gmail.com> wrote:
>>>
>>>    Hi David,
>>>
>>>    Congratulations (again)! I find it very interesti= ng that this
>>>    question has a positive answer. I had suspected t= hat it might
>>>    separate HoTT from Voevodsky's HTS (aka 2LTT with= a fibrancy
>>>    assumption on strict Nat). Since this isn't the c= ase, 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 Ho= TT?
>>>
>>>    Best,
>>>    Nicolai
>>>
>>>    On Fri, Apr 21, 2023 at 8:30=E2=80=AFPM Jon Sterl= ing
>>>    <jon@jonmsterling.com> wrote:
>>>
>>>        Dear David,
>>>
>>>        Congratulations on your beautiful r= esult; I'm looking forward
>>>        to understanding the details. Recen= tly I had been wondering if
>>>        anyone had proved this, and I am de= lighted 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 theo= ry: the free higher group
>>>        on a set is a set.
>>>>
>>>> The proof proceeds by describing path types of pushouts as=
>>>        sequential colimits of pushouts, mu= ch like the James
>>>        construction. This description shou= ld 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 th= e
>>>        Google Groups "Homotopy Type Theory= " group.
>>>> To unsubscribe from this group and stop receiving emails >>>        from it, send an email to
>>>        HomotopyTypeTheory+unsu= bscribe@googlegroups.com.
>>>> To view this discussion on the web visit
>>>
>> https://groups.google.com/d/msgid/HomotopyTypeTheory/f2af459c-5= 3a6-e7b9-77db-5cbf56da17f3%40gmail.com.
>>
>>>
>>>        --
>>>        You received this message because y= ou 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+unsu= bscribe@googlegroups.com.
>>>        To view this discussion on the web = visit
>>>
>> https://groups.google.com/d/msgid/HomotopyTypeTheory/D102F= 774-D134-46B9-A70A-51CB84BE4B6F%40jonmsterling.com.
>>
>>>
>>>    --
>>>    You received this message because you are subscri= bed 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/Homotop= yTypeTheory/CA%2BAZBBpPwgh1G9VZV0fgJFd8Mzqfchskc4-%2B-FXT42WQkzmC9w%40mail.= gmail.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@googlegroup= s.com.
>> To view this discussion on the web visit
>> https://groups.= google.com/d/msgid/HomotopyTypeTheory/87leigyeya.fsf%40uwo.ca.
>
> --
> 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/= 87zg6qy4gx.fsf%40uwo.ca.

--
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.

--
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/msg= id/HomotopyTypeTheory/5D0912E6-075B-47EE-87B8-8B5118DDF07C%40gmail.com.=
--Apple-Mail=_74E4A905-9946-45BA-BB1F-7A8F733D6D38--