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,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 11048 invoked from network); 29 Apr 2023 19:08:46 -0000 Received: from mail-yb1-xb3f.google.com (2607:f8b0:4864:20::b3f) by inbox.vuxu.org with ESMTPUTF8; 29 Apr 2023 19:08:46 -0000 Received: by mail-yb1-xb3f.google.com with SMTP id 3f1490d57ef6-b9a7d92d0f7sf1801098276.1 for ; Sat, 29 Apr 2023 12:08:46 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20221208; t=1682795326; x=1685387326; h=list-unsubscribe:list-subscribe:list-archive:list-help:list-post :list-id:mailing-list:precedence:x-original-sender:mime-version :subject:references:in-reply-to:message-id:to:from:date:sender:from :to:cc:subject:date:message-id:reply-to; bh=fWitUqeJNjapTi4FdiqjiIiNkB0UdXtLyOMpe/c5sK4=; b=I1GUDl96KIJoxnxg3En4iTn7rkYMsvi7gh1e2sWTbHL04uivn/GcyKw7xIQlvkDRPf +1RVxDJ/rP9P4sTqShhl5gSkUf5AxJJasEz6XQtQPBhc/h+VOGa5JWuM7kQbK+cHPBwT 7o4YhuNOXIUj9xLA34z5GuASAjdIUxle6BZXh8mhzfS9aeH9VaDxA8jEN5zJFuQM41OM C7Mx6THMUaj4kG05w9MmJmNGpSKOzutm3gx9gx16YZNXmqadlXaB/Lw3+zYYpYqDjOR3 X9mMbNUVFcFP4cOCnfOgZ4St/9oBACz8uHm1YOY57PbojHVM/ZV9sW9Mt7M+xGig8yx4 f4bg== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=hugunin-net.20221208.gappssmtp.com; s=20221208; t=1682795326; x=1685387326; h=list-unsubscribe:list-subscribe:list-archive:list-help:list-post :list-id:mailing-list:precedence:x-original-sender:mime-version :subject:references:in-reply-to:message-id:to:from:date:from:to:cc :subject:date:message-id:reply-to; bh=fWitUqeJNjapTi4FdiqjiIiNkB0UdXtLyOMpe/c5sK4=; b=dtTMOROJfmBE3WewFgPi92QxiS6WW/SLZ92bvs7jCV3GofQhmZ+Ju9QN+Dj1TWWeBQ CC1EQ/B2Sldek2by1unvZqTs8rNleLQ7NCqJdD9qzQ5KwQ28Ralxzl3bntnSU4fIrT8u q/KbEsVMgde5rl+nleFApmwIN+DjRVomO1K6/keprwhXTBUEXjEuLQaNozH6LDzTQZPx 4Kb4Rv0D8k9fUB+DL2Mp2jwqVvq6rg1IVJyuC5RKOGzW3r6miqZZYBO6HTXV6er3uNNc Y2tJVLxcbaCCOXoVILkWWCrS+hdy8CkRrVXZqtevwAujL7NkxW96gXc2ZsLAvz9jgCA+ Mzrw== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20221208; t=1682795326; x=1685387326; h=list-unsubscribe:list-subscribe:list-archive:list-help:list-post :list-id:mailing-list:precedence:x-original-sender:mime-version :subject:references:in-reply-to:message-id:to:from:date:x-beenthere :x-gm-message-state:sender:from:to:cc:subject:date:message-id :reply-to; bh=fWitUqeJNjapTi4FdiqjiIiNkB0UdXtLyOMpe/c5sK4=; b=BoR0iMW15vkJCEU/p1Tn6++hdwg/uEtZQk2mbHllJxwkoAvwEP0N442cduc1Lr9Iv9 KrLlMTg1CB6pvtWWw4qebpM5w77wz4fxB0WDhoOTPZ9Y3iLc/BkmV4dX1MhFtIdXfOIn cAxsZ3NFDgY9T4gcJ38Ge79elGZx8ctNz7jmdboWv85pWO9bpfJbEUTIbLjzOucnNVcq QQHag9xbOj6aTx4TyARDDCTtgcZewwXpXUS4M11w85Q/KJpz0vXyUQSRt3qnsfJQTE+S G3uGJBaRWXffhqMW8rNjOzStx67X2xlL/VCEHVzluFvQmtNMfDemt+Zso51NGWqXLZ6a Qo/w== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AC+VfDx34zdCvTYTInUy5OABukRY3RYxWKVAiqOakVabaUsRy2gDcTcj StdAqEZ/eEiWiFGTFKyfjP8= X-Google-Smtp-Source: ACHHUZ5A8AXyxNHVUklwJ1nmNI/QAVkdZaR/1kk7fZHC1Cb8jT+BURP4ylNtwW37prYaPWUWdDaEBA== X-Received: by 2002:a25:4245:0:b0:b97:8207:443b with SMTP id p66-20020a254245000000b00b978207443bmr3331057yba.5.1682795325704; Sat, 29 Apr 2023 12:08:45 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a81:f10a:0:b0:556:a9c4:6c91 with SMTP id h10-20020a81f10a000000b00556a9c46c91ls4602159ywm.6.-pod-prod-gmail; Sat, 29 Apr 2023 12:08:44 -0700 (PDT) X-Received: by 2002:a81:ae0c:0:b0:559:d8ad:560d with SMTP id m12-20020a81ae0c000000b00559d8ad560dmr1841633ywh.5.1682795324710; Sat, 29 Apr 2023 12:08:44 -0700 (PDT) Received: by 2002:a05:690c:dc4:b0:54f:badf:f99 with SMTP id 00721157ae682-558858cc15ams7b3; Sat, 29 Apr 2023 12:06:57 -0700 (PDT) X-Received: by 2002:a05:6902:4a6:b0:b9d:b399:64b0 with SMTP id r6-20020a05690204a600b00b9db39964b0mr768220ybs.10.1682795216228; Sat, 29 Apr 2023 12:06:56 -0700 (PDT) Date: Sat, 29 Apr 2023 12:06:55 -0700 (PDT) From: Jasper Hugunin To: Homotopy Type Theory Message-Id: <73121272-421b-4dba-943f-b81f32854862n@googlegroups.com> In-Reply-To: <87r0s2y0rp.fsf@uwo.ca> References: <87leigyeya.fsf@uwo.ca> <87zg6qy4gx.fsf@uwo.ca> <21ED9406-6C3A-4B26-A74B-34C2821C97B6@gmail.com> <87r0s2y0rp.fsf@uwo.ca> Subject: Re: [HoTT] Free higher groups MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_7770_2127295636.1682795216000" X-Original-Sender: jasper@hugunin.net 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: , ------=_Part_7770_2127295636.1682795216000 Content-Type: multipart/alternative; boundary="----=_Part_7771_696110088.1682795216000" ------=_Part_7771_696110088.1682795216000 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Another example constructible in HTS but maybe not in HoTT is the large=20 type of semi-simplicial types (On the Role of Semisimplicial Types -=20 Nicolai Kraus=20 ). This one might be a bit tricky because I don't know how to internally=20 express that a particular large type is the type of semi-simplicial types= =20 either (what universal property it should have). On Saturday, April 29, 2023 at 11:57:36=E2=80=AFAM UTC-7 Dan Christensen wr= ote: > Sets don't cover in a general oo-topos. (You have to be a bit > careful about the internal notion vs the external notion, but > both fail in general.) There's a good summary here: > > https://ncatlab.org/nlab/show/n-types+cover/ > > Dan > > On Apr 29, 2023, Steve Awodey wrote: > > > 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 i= s > >> 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= =20 > to be > >>> true in all Grothendieck 1-toposes but not all elementary 1-toposes,= =20 > such as > >>> WISC and Freyd's theorem that a small complete category is a preorder= .=20 > So > >>> those will be true in any Grothendieck oo-topos too, and can be=20 > presumed to > >>> fail in HoTT. But it's nice to have one that involves higher types to= o. > >>>=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=20 > deloopings > >>> of S^3. The reason this isn't so interesting is that it's in the imag= e > >>> 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. 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 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 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 > >>>> HomotopyTypeThe...@googlegroups.com. > >>>>> To view this discussion on the web visit > >>>>=20 > >>>=20 > https://groups.google.com/d/msgid/HomotopyTypeTheory/f2af459c-53a6-e7b9-7= 7db-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 > >>>> HomotopyTypeThe...@googlegroups.com. > >>>> To view this discussion on the web visit > >>>>=20 > >>>=20 > https://groups.google.com/d/msgid/HomotopyTypeTheory/D102F774-D134-46B9-A= 70A-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 > >>> HomotopyTypeThe...@googlegroups.com. > >>>> To view this discussion on the web visit > >>>>=20 > >>>=20 > https://groups.google.com/d/msgid/HomotopyTypeTheory/CA%2BAZBBpPwgh1G9VZV= 0fgJFd8Mzqfchskc4-%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 HomotopyTypeThe...@googlegroups.com. > >>> To view this discussion on the web visit > >>>=20 > https://groups.google.com/d/msgid/HomotopyTypeTheory/87leigyeya.fsf%40uwo= .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 HomotopyTypeThe...@googlegroups.com. > >> To view this discussion on the web visit > >>=20 > https://groups.google.com/d/msgid/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/73121272-421b-4dba-943f-b81f32854862n%40googlegroups.com= . ------=_Part_7771_696110088.1682795216000 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Another example constructible in HTS but maybe no= t in HoTT is the large type of semi-simplicial types (On the Role of Semisimplicial Types - Nicolai Kr= aus).

This one might be a bit tricky because I don't= know how to internally express that a particular large type is the type of= semi-simplicial types either (what universal property it should=C2=A0have)= .

On Saturday, April 29, 2023 at 11:57:36=E2=80=AFAM UTC-7 Dan Christense= n wrote:
Sets= don't cover in a general oo-topos. (You have to be a bit
careful about the internal notion vs the external notion, but
both fail in general.) There's a good summary here:

htt= ps://ncatlab.org/nlab/show/n-types+cover/

Dan

On Apr 29, 2023, Steve Awodey <steve...@gmail.com> wrote:

> good one!
> How about just covering a type by a 0-type?
>
> Steve
>
>> On Apr 29, 2023, at 1:37 PM, Dan Christensen <j...@uwo.ca> wrote:
>>=20
>> Another set-level statement is whether there are enough inject= ive
>> 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 <shu...@sandiego.edu> wrote:
>>=20
>>> The existence of hypercompletion is a good suggestion.
>>>=20
>>> Also I realized there are set-level statements that are al= ready 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 categor= y is a preorder. So
>>> those will be true in any Grothendieck oo-topos too, and c= an 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 &l= t;j...@uwo.ca> wrote:
>>>=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&= #39;s true just
>>> because it is true for Spaces. Similarly, a statement ass= erting that
>>> pi_42(S^17) =3D (insert what it is) is true in any oo-topo= s. 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 co= ndition that it would
>>> be good to have a type for which there is some reason to d= oubt that it
>>> is provably inhabited in HoTT.
>>>=20
>>> Oh, what about whether the hypercomplete objects are the m= odal
>>> objects
>>> for a modality? I'm throwing this out there without m= uch thought...
>>>=20
>>> Dan
>>>=20
>>> On Apr 24, 2023, Michael Shulman <shu...@sandiego.edu> wrote:
>>>=20
>>>> This is fantastic, especially the simplicity of the co= nstruction. As
>>>> Peter said, a wonderful way to commemorate the 10th an= niversary of
>>> the
>>>> special year and the release of the HoTT Book.
>>>>=20
>>>> Relatedly to Nicolai's question, this question als= o 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 in= terpretation in
>>>> any Grothendieck infinity-topos is known to be inhabit= ed, but which
>>>> isn't known to be inhabited in HoTT?
>>>>=20
>>>> On Fri, Apr 21, 2023 at 5:25=E2=80=AFPM Nicolai Kraus
>>>> <nicola.= ..@gmail.com> wrote:
>>>>=20
>>>> Hi David,
>>>>=20
>>>> Congratulations (again)! I find it very interesting= that this
>>>> question has a positive answer. I had suspected tha= t it might
>>>> separate HoTT from Voevodsky's HTS (aka 2LTT wi= th 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, w= hile 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 Sterlin= g
>>>> <j...= @jonmsterling.com> wrote:
>>>>=20
>>>> Dear David,
>>>>=20
>>>> Congratulations on your beautiful result; I'= ;m looking forward
>>>> to understanding the details. Recently I had be= en wondering if
>>>> anyone had proved this, and I am delighted to s= ee 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 pus= houts 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 stra= ightforward
>>>> proof of Blakers-Massey.
>>>>>=20
>>>>> Best wishes,
>>>>> David
>>>>>=20
>>>>> --=20
>>>>> You received this message because you are subscrib= ed to the
>>>> Google Groups "Homotopy Type Theory" = group.
>>>>> To unsubscribe from this group and stop receiving = emails
>>>> from it, send an email to
>>>> Homo= topyTypeThe...@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<= /a>.
>>>=20
>>>>=20
>>>> --=20
>>>> You received this message because you are subsc= ribed to the
>>>> Google Groups "Homotopy Type Theory" = group.
>>>> To unsubscribe from this group and stop receivi= ng emails from
>>>> it, send an email to
>>>> Homo= topyTypeThe...@googlegroups.com.
>>>> To view this discussion on the web visit
>>>>=20
>>> https://group= s.google.com/d/msgid/HomotopyTypeTheory/D102F774-D134-46B9-A70A-51CB84BE4B6= F%40jonmsterling.com.
>>>=20
>>>>=20
>>>> --=20
>>>> You received this message because you are subscribe= d to the
>>> Google
>>>> Groups "Homotopy Type Theory" group.
>>>> To unsubscribe from this group and stop receiving e= mails from it,
>>>> send an email to
>>> HomotopyTypeThe= ...@googlegroups.com.
>>>> To view this discussion on the web visit
>>>>=20
>>> https://groups.google.com/d/msgid/HomotopyTypeTheo= ry/CA%2BAZBBpPwgh1G9VZV0fgJFd8Mzqfchskc4-%2B-FXT42WQkzmC9w%40mail.gmail.com= .
>>>=20
>>> --=20
>>> 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 f= rom it, send
>>> an email to Hom= otopyTypeThe...@googlegroups.com.
>>> To view this discussion on the web visit
>>> ht= tps://groups.google.com/d/msgid/HomotopyTypeTheory/87leigyeya.fsf%40uwo.ca<= /a>.
>>=20
>> --=20
>> You received this message because you are subscribed to the Go= ogle
>> Groups "Homotopy Type Theory" group.
>> To unsubscribe from this group and stop receiving emails from = it,
>> send an email to Ho= motopyTypeThe...@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 &= 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.c= om/d/msgid/HomotopyTypeTheory/73121272-421b-4dba-943f-b81f32854862n%40googl= egroups.com.
------=_Part_7771_696110088.1682795216000-- ------=_Part_7770_2127295636.1682795216000--