*[HoTT] Free higher groups@ 2023-04-21 10:04 ` David Wärn2023-04-21 11:28 ` [HoTT] " Ulrik Buchholtz ` (2 more replies) 0 siblings, 3 replies; 17+ messages in thread From: David Wärn @ 2023-04-21 10:04 UTC (permalink / raw) To: homotopytypetheory [-- Attachment #1: Type: text/plain, Size: 817 bytes --] 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-77db-5cbf56da17f3%40gmail.com. [-- Attachment #2: po-paths.pdf --] [-- Type: application/pdf, Size: 314831 bytes --] ^ permalink raw reply [flat|nested] 17+ messages in thread

*[HoTT] Re: Free higher groups2023-04-21 10:04 ` [HoTT] Free higher groups David Wärn@ 2023-04-21 11:28 ` Ulrik Buchholtz2023-04-21 14:32 ` [HoTT] " Peter LeFanu Lumsdaine 2023-04-21 18:30 ` Jon Sterling 2 siblings, 0 replies; 17+ messages in thread From: Ulrik Buchholtz @ 2023-04-21 11:28 UTC (permalink / raw) To: Homotopy Type Theory [-- Attachment #1.1: Type: text/plain, Size: 1281 bytes --] Congratulations, that's really great! And indeed, this is going to be very useful in general: for instance, together with Tom de Jong and Egbert Rijke, we used your work as an input to give a short constructive proof of the non-triviality of the Higman group. I'll talk about this in Vienna on Sunday. Best wishes, Ulrik On Friday, April 21, 2023 at 12:04:20 PM UTC+2 cod...@gmail.com 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/4e1cf0e3-a5b0-4014-b144-0a5bb98b01e3n%40googlegroups.com. [-- Attachment #1.2: Type: text/html, Size: 1872 bytes --] ^ permalink raw reply [flat|nested] 17+ messages in thread

*Re: [HoTT] Free higher groups2023-04-21 10:04 ` [HoTT] Free higher groups David Wärn 2023-04-21 11:28 ` [HoTT] " Ulrik Buchholtz@ 2023-04-21 14:32 ` Peter LeFanu Lumsdaine2023-04-21 18:30 ` Jon Sterling 2 siblings, 0 replies; 17+ messages in thread From: Peter LeFanu Lumsdaine @ 2023-04-21 14:32 UTC (permalink / raw) To: homotopytypetheory [-- Attachment #1: Type: text/plain, Size: 2014 bytes --] Lovely — congratulations! I remember at the IAS special year discussing (with Guillaume Brunerie and others) the feeling that there should be a James construction style proof of Blakers–Massey, but we were never able to find it — fantastic to see that it can be made to work after all. And the timing is nice — it’s almost exactly 10 years since the final seminar of the special year, where Guillaume, Dan and I presented a survey of the results in synthetic homotopy theory so far, including Blakers–Massey and the James construction: https://www.ias.edu/video/univalent/1213/0411-HomotopyGroup Best, –Peter. On Fri, Apr 21, 2023 at 11:04 AM David Wärn <codwarn@gmail.com> 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-77db-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/CAAkwb-kzRC70p5Xpv8YANJqUgHbDMj2y5e6A2x4RX8WbAEseag%40mail.gmail.com. [-- Attachment #2: Type: text/html, Size: 3084 bytes --] ^ permalink raw reply [flat|nested] 17+ messages in thread

*Re: [HoTT] Free higher groups2023-04-21 10:04 ` [HoTT] Free higher groups David Wärn 2023-04-21 11:28 ` [HoTT] " Ulrik Buchholtz 2023-04-21 14:32 ` [HoTT] " Peter LeFanu Lumsdaine@ 2023-04-21 18:30 ` Jon Sterling2023-04-22 0:24 ` Nicolai Kraus 2 siblings, 1 reply; 17+ messages in thread From: Jon Sterling @ 2023-04-21 18:30 UTC (permalink / raw) To: David Wärn;+Cc:homotopytypetheory 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ärn 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-77db-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-A70A-51CB84BE4B6F%40jonmsterling.com. ^ permalink raw reply [flat|nested] 17+ messages in thread

*Re: [HoTT] Free higher groups2023-04-21 18:30 ` Jon Sterling@ 2023-04-22 0:24 ` Nicolai Kraus2023-04-25 0:02 ` Michael Shulman 0 siblings, 1 reply; 17+ messages in thread From: Nicolai Kraus @ 2023-04-22 0:24 UTC (permalink / raw) To: homotopytypetheory [-- Attachment #1: Type: text/plain, Size: 2527 bytes --] 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 PM Jon Sterling <jon@jonmsterling.com> 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ärn 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-77db-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-A70A-51CB84BE4B6F%40jonmsterling.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/CA%2BAZBBpPwgh1G9VZV0fgJFd8Mzqfchskc4-%2B-FXT42WQkzmC9w%40mail.gmail.com. [-- Attachment #2: Type: text/html, Size: 3731 bytes --] ^ permalink raw reply [flat|nested] 17+ messages in thread

*Re: [HoTT] Free higher groups2023-04-22 0:24 ` Nicolai Kraus@ 2023-04-25 0:02 ` Michael Shulman2023-04-25 0:37 ` Dan Christensen 0 siblings, 1 reply; 17+ messages in thread From: Michael Shulman @ 2023-04-25 0:02 UTC (permalink / raw) To: Nicolai Kraus;+Cc:homotopytypetheory [-- Attachment #1: Type: text/plain, Size: 3792 bytes --] 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. 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? On Fri, Apr 21, 2023 at 5:25 PM Nicolai Kraus <nicolai.kraus@gmail.com> wrote: > 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 PM Jon Sterling <jon@jonmsterling.com> 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ärn 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-77db-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-A70A-51CB84BE4B6F%40jonmsterling.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/CA%2BAZBBpPwgh1G9VZV0fgJFd8Mzqfchskc4-%2B-FXT42WQkzmC9w%40mail.gmail.com > <https://groups.google.com/d/msgid/HomotopyTypeTheory/CA%2BAZBBpPwgh1G9VZV0fgJFd8Mzqfchskc4-%2B-FXT42WQkzmC9w%40mail.gmail.com?utm_medium=email&utm_source=footer> > . > -- 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/CADYavpxM-_a_nM0qu7XBv66oP8VG852BaMwmzo3%2BNgGxijf8Rg%40mail.gmail.com. [-- Attachment #2: Type: text/html, Size: 5395 bytes --] ^ permalink raw reply [flat|nested] 17+ messages in thread

*Re: [HoTT] Free higher groups2023-04-25 0:02 ` Michael Shulman@ 2023-04-25 0:37 ` Dan Christensen2023-04-28 17:59 ` Michael Shulman 0 siblings, 1 reply; 17+ messages in thread From: Dan Christensen @ 2023-04-25 0:37 UTC (permalink / raw) To: homotopytypetheory 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) = (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. 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. Oh, what about whether the hypercomplete objects are the modal objects for a modality? I'm throwing this out there without much thought... Dan On Apr 24, 2023, Michael Shulman <shulman@sandiego.edu> wrote: > 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. > > 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? > > On Fri, Apr 21, 2023 at 5:25 PM Nicolai Kraus > <nicolai.kraus@gmail.com> wrote: > > 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 PM Jon Sterling > <jon@jonmsterling.com> 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ärn 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-77db-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-A70A-51CB84BE4B6F%40jonmsterling.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/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@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/87leigyeya.fsf%40uwo.ca. ^ permalink raw reply [flat|nested] 17+ messages in thread

*Re: [HoTT] Free higher groups2023-04-25 0:37 ` Dan Christensen@ 2023-04-28 17:59 ` Michael Shulman2023-04-29 17:37 ` Dan Christensen 0 siblings, 1 reply; 17+ messages in thread From: Michael Shulman @ 2023-04-28 17:59 UTC (permalink / raw) To: Dan Christensen;+Cc:homotopytypetheory [-- Attachment #1: Type: text/plain, Size: 5943 bytes --] The existence of hypercompletion is a good suggestion. 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 presumed to fail in HoTT. But it's nice to have one that involves higher types too. On Mon, Apr 24, 2023 at 5:37 PM Dan Christensen <jdc@uwo.ca> wrote: > 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) = (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. > > 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. > > Oh, what about whether the hypercomplete objects are the modal objects > for a modality? I'm throwing this out there without much thought... > > Dan > > On Apr 24, 2023, Michael Shulman <shulman@sandiego.edu> wrote: > > > 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. > > > > 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? > > > > On Fri, Apr 21, 2023 at 5:25 PM Nicolai Kraus > > <nicolai.kraus@gmail.com> wrote: > > > > 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 PM Jon Sterling > > <jon@jonmsterling.com> 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ärn 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-77db-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-A70A-51CB84BE4B6F%40jonmsterling.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/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@googlegroups.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 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/CADYavpxy1Qh97%2BPZ1%3DDaaKFH3RXo9wTwDhqbcoUFw5ZDP4oUrQ%40mail.gmail.com. [-- Attachment #2: Type: text/html, Size: 8522 bytes --] ^ permalink raw reply [flat|nested] 17+ messages in thread

*Re: [HoTT] Free higher groups2023-04-28 17:59 ` Michael Shulman@ 2023-04-29 17:37 ` Dan Christensen2023-04-29 18:37 ` Steve Awodey 0 siblings, 1 reply; 17+ messages in thread From: Dan Christensen @ 2023-04-29 17:37 UTC (permalink / raw) To: homotopytypetheory 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. 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 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 presumed to > fail in HoTT. But it's nice to have one that involves higher types too. > > On Mon, Apr 24, 2023 at 5:37 PM Dan Christensen <jdc@uwo.ca> wrote: > > 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) = (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. > > 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. > > Oh, what about whether the hypercomplete objects are the modal > objects > for a modality? I'm throwing this out there without much thought... > > Dan > > On Apr 24, 2023, Michael Shulman <shulman@sandiego.edu> wrote: > > > 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. > > > > 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? > > > > On Fri, Apr 21, 2023 at 5:25 PM Nicolai Kraus > > <nicolai.kraus@gmail.com> wrote: > > > > 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 PM Jon Sterling > > <jon@jonmsterling.com> 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ärn 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-77db-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-A70A-51CB84BE4B6F%40jonmsterling.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/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@googlegroups.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 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/87zg6qy4gx.fsf%40uwo.ca. ^ permalink raw reply [flat|nested] 17+ messages in thread

*Re: [HoTT] Free higher groups2023-04-29 17:37 ` Dan Christensen@ 2023-04-29 18:37 ` Steve Awodey2023-04-29 18:49 ` Ulrik Buchholtz 2023-04-29 18:57 ` Dan Christensen 0 siblings, 2 replies; 17+ messages in thread From: Steve Awodey @ 2023-04-29 18:37 UTC (permalink / raw) To: Dan Christensen;+Cc:homotopytypetheory good one! How about just covering a type by a 0-type? 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 presumably 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 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 presumed to >> fail in HoTT. But it's nice to have one that involves higher types too. >> >> On Mon, Apr 24, 2023 at 5:37 PM Dan Christensen <jdc@uwo.ca> wrote: >> >> 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) = (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. >> >> 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. >> >> Oh, what about whether the hypercomplete objects are the modal >> objects >> for a modality? I'm throwing this out there without much thought... >> >> Dan >> >> On Apr 24, 2023, Michael Shulman <shulman@sandiego.edu> wrote: >> >>> 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. >>> >>> 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? >>> >>> On Fri, Apr 21, 2023 at 5:25 PM Nicolai Kraus >>> <nicolai.kraus@gmail.com> wrote: >>> >>> 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 PM Jon Sterling >>> <jon@jonmsterling.com> 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ärn 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-77db-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-A70A-51CB84BE4B6F%40jonmsterling.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/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@googlegroups.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 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/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 email 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. ^ permalink raw reply [flat|nested] 17+ messages in thread

*Re: [HoTT] Free higher groups2023-04-29 18:37 ` Steve Awodey@ 2023-04-29 18:49 ` Ulrik Buchholtz2023-04-29 19:22 ` Steve Awodey 2023-04-29 18:57 ` Dan Christensen 1 sibling, 1 reply; 17+ messages in thread From: Ulrik Buchholtz @ 2023-04-29 18:49 UTC (permalink / raw) To: Steve Awodey;+Cc:Dan Christensen, homotopytypetheory [-- Attachment #1: Type: text/plain, Size: 8148 bytes --] > 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 recently is whether we can construct the modality for which the acyclic maps are the left class. (This exists in every Grothendieck higher topos. In infinity groupoids, and many, but not all, models, the right class are the hypoabelian maps.) Then there's the question whether every simply connected acyclic type is contractible. (This is open for Grothendieck 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 presumably 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 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 > presumed to > >> fail in HoTT. But it's nice to have one that involves higher types too. > >> > >> On Mon, Apr 24, 2023 at 5:37 PM Dan Christensen <jdc@uwo.ca> wrote: > >> > >> 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) = (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. > >> > >> 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. > >> > >> Oh, what about whether the hypercomplete objects are the modal > >> objects > >> for a modality? I'm throwing this out there without much thought... > >> > >> Dan > >> > >> On Apr 24, 2023, Michael Shulman <shulman@sandiego.edu> wrote: > >> > >>> 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. > >>> > >>> 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? > >>> > >>> On Fri, Apr 21, 2023 at 5:25 PM Nicolai Kraus > >>> <nicolai.kraus@gmail.com> wrote: > >>> > >>> 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 PM Jon Sterling > >>> <jon@jonmsterling.com> 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ärn 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-77db-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-A70A-51CB84BE4B6F%40jonmsterling.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/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@googlegroups.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 > 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/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 > email 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 "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/CAE-BQ1zWQHqUv9woQPw75Sqz1c7_M9F-nzX3RYYmXAxVxy8skQ%40mail.gmail.com. [-- Attachment #2: Type: text/html, Size: 12423 bytes --] ^ permalink raw reply [flat|nested] 17+ messages in thread

*Re: [HoTT] Free higher groups2023-04-29 18:37 ` Steve Awodey 2023-04-29 18:49 ` Ulrik Buchholtz@ 2023-04-29 18:57 ` Dan Christensen2023-04-29 19:06 ` Jasper Hugunin 1 sibling, 1 reply; 17+ messages in thread From: Dan Christensen @ 2023-04-29 18:57 UTC (permalink / raw) To: Steve Awodey;+Cc:homotopytypetheory 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 <steveawodey@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 <jdc@uwo.ca> wrote: >> >> 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. >> >> 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 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 presumed to >>> fail in HoTT. But it's nice to have one that involves higher types too. >>> >>> On Mon, Apr 24, 2023 at 5:37 PM Dan Christensen <jdc@uwo.ca> wrote: >>> >>> 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) = (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. >>> >>> 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. >>> >>> Oh, what about whether the hypercomplete objects are the modal >>> objects >>> for a modality? I'm throwing this out there without much thought... >>> >>> Dan >>> >>> On Apr 24, 2023, Michael Shulman <shulman@sandiego.edu> wrote: >>> >>>> 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. >>>> >>>> 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? >>>> >>>> On Fri, Apr 21, 2023 at 5:25 PM Nicolai Kraus >>>> <nicolai.kraus@gmail.com> wrote: >>>> >>>> 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 PM Jon Sterling >>>> <jon@jonmsterling.com> 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ärn 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-77db-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-A70A-51CB84BE4B6F%40jonmsterling.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/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@googlegroups.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 >> 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/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 email to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/87r0s2y0rp.fsf%40uwo.ca. ^ permalink raw reply [flat|nested] 17+ messages in thread

*Re: [HoTT] Free higher groups2023-04-29 18:57 ` Dan Christensen@ 2023-04-29 19:06 ` Jasper Hugunin2023-05-02 8:35 ` 'Thorsten Altenkirch' via Homotopy Type Theory 0 siblings, 1 reply; 17+ messages in thread From: Jasper Hugunin @ 2023-04-29 19:06 UTC (permalink / raw) To: Homotopy Type Theory [-- Attachment #1.1: Type: text/plain, Size: 7687 bytes --] Another example constructible in HTS but maybe not in HoTT is the large type of semi-simplicial types (On the Role of Semisimplicial Types - Nicolai Kraus <http://www.cs.nott.ac.uk/~psznk/docs/on_semisimplicial_types.pdf>). 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 have). On Saturday, April 29, 2023 at 11:57:36 AM UTC-7 Dan Christensen 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: > > https://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: > >> > >> 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. > >> > >> Dan > >> > >> On Apr 28, 2023, Michael Shulman <shu...@sandiego.edu> wrote: > >> > >>> The existence of hypercompletion is a good suggestion. > >>> > >>> 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 > presumed to > >>> fail in HoTT. But it's nice to have one that involves higher types too. > >>> > >>> On Mon, Apr 24, 2023 at 5:37 PM Dan Christensen <j...@uwo.ca> wrote: > >>> > >>> 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) = (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. > >>> > >>> 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. > >>> > >>> Oh, what about whether the hypercomplete objects are the modal > >>> objects > >>> for a modality? I'm throwing this out there without much thought... > >>> > >>> Dan > >>> > >>> On Apr 24, 2023, Michael Shulman <shu...@sandiego.edu> wrote: > >>> > >>>> 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. > >>>> > >>>> 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? > >>>> > >>>> On Fri, Apr 21, 2023 at 5:25 PM Nicolai Kraus > >>>> <nicola...@gmail.com> wrote: > >>>> > >>>> 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 PM Jon Sterling > >>>> <j...@jonmsterling.com> 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ärn 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 > >>>> HomotopyTypeThe...@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 "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 > >>>> > >>> > https://groups.google.com/d/msgid/HomotopyTypeTheory/D102F774-D134-46B9-A70A-51CB84BE4B6F%40jonmsterling.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 > >>> HomotopyTypeThe...@googlegroups.com. > >>>> To view this discussion on the web visit > >>>> > >>> > https://groups.google.com/d/msgid/HomotopyTypeTheory/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 HomotopyTypeThe...@googlegroups.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 > >> 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 > >> > 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 email 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. [-- Attachment #1.2: Type: text/html, Size: 13646 bytes --] ^ permalink raw reply [flat|nested] 17+ messages in thread

*Re: [HoTT] Free higher groups2023-04-29 18:49 ` Ulrik Buchholtz@ 2023-04-29 19:22 ` Steve Awodey2023-04-30 0:43 ` Michael Shulman 0 siblings, 1 reply; 17+ messages in thread From: Steve Awodey @ 2023-04-29 19:22 UTC (permalink / raw) To: Ulrik Buchholtz;+Cc:Dan Christensen, homotopytypetheory [-- Attachment #1: Type: text/plain, Size: 8900 bytes --] Glad I asked - thanks! > On Apr 29, 2023, at 2:49 PM, Ulrik Buchholtz <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 recently is whether we can construct the modality for which the acyclic maps are the left class. (This exists in every Grothendieck higher topos. In infinity groupoids, and many, but not all, models, the right class are the hypoabelian maps.) > > Then there's the question whether every simply connected acyclic type is contractible. (This is open for Grothendieck 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 <mailto:jdc@uwo.ca>> wrote: >> > >> > 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. >> > >> > Dan >> > >> > On Apr 28, 2023, Michael Shulman <shulman@sandiego.edu <mailto:shulman@sandiego.edu>> wrote: >> > >> >> The existence of hypercompletion is a good suggestion. >> >> >> >> 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 presumed to >> >> fail in HoTT. But it's nice to have one that involves higher types too. >> >> >> >> On Mon, Apr 24, 2023 at 5:37 PM Dan Christensen <jdc@uwo.ca <mailto:jdc@uwo.ca>> wrote: >> >> >> >> 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) = (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. >> >> >> >> 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. >> >> >> >> Oh, what about whether the hypercomplete objects are the modal >> >> objects >> >> for a modality? I'm throwing this out there without much thought... >> >> >> >> Dan >> >> >> >> On Apr 24, 2023, Michael Shulman <shulman@sandiego.edu <mailto:shulman@sandiego.edu>> wrote: >> >> >> >>> 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. >> >>> >> >>> 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? >> >>> >> >>> On Fri, Apr 21, 2023 at 5:25 PM Nicolai Kraus >> >>> <nicolai.kraus@gmail.com <mailto:nicolai.kraus@gmail.com>> wrote: >> >>> >> >>> 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 PM Jon Sterling >> >>> <jon@jonmsterling.com <mailto:jon@jonmsterling.com>> 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ärn 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 <mailto:HomotopyTypeTheory%2Bunsubscribe@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 "Homotopy Type Theory" group. >> >>> To unsubscribe from this group and stop receiving emails from >> >>> it, send an email to >> >>> HomotopyTypeTheory+unsubscribe@googlegroups.com <mailto:HomotopyTypeTheory%2Bunsubscribe@googlegroups.com>. >> >>> To view this discussion on the web visit >> >>> >> >> https://groups.google.com/d/msgid/HomotopyTypeTheory/D102F774-D134-46B9-A70A-51CB84BE4B6F%40jonmsterling.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 <mailto:HomotopyTypeTheory%2Bunsubscribe@googlegroups.com>. >> >>> To view this discussion on the web visit >> >>> >> >> https://groups.google.com/d/msgid/HomotopyTypeTheory/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@googlegroups.com <mailto:HomotopyTypeTheory%2Bunsubscribe@googlegroups.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 Groups "Homotopy Type Theory" group. >> > To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com <mailto:HomotopyTypeTheory%2Bunsubscribe@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 email to HomotopyTypeTheory+unsubscribe@googlegroups.com <mailto:HomotopyTypeTheory%2Bunsubscribe@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 "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/5D0912E6-075B-47EE-87B8-8B5118DDF07C%40gmail.com. [-- Attachment #2: Type: text/html, Size: 13229 bytes --] ^ permalink raw reply [flat|nested] 17+ messages in thread

*Re: [HoTT] Free higher groups2023-04-29 19:22 ` Steve Awodey@ 2023-04-30 0:43 ` Michael Shulman0 siblings, 0 replies; 17+ messages in thread From: Michael Shulman @ 2023-04-30 0:43 UTC (permalink / raw) To: Steve Awodey;+Cc:Ulrik Buchholtz, Dan Christensen, homotopytypetheory [-- Attachment #1: Type: text/plain, Size: 1049 bytes --] Bringing this thread back to David's original announcement of his new result, one thing that intrigues me about it is that proceeds by constructing successive approximations to the desired path space and then taking a sequential colimit. This reminds me of some other sequential constructions that also achieved surprising (to me) things, like Egbert's join construction for building propositional truncation out of nonrecursive HITs, and the splitting of a quasi-idempotent by a sequential (co)limit that Lurie used in higher category theory and I then adapted to HoTT. I wonder if there are other surprising applications of this principle. -- 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/CADYavpzinvAW_PgLUPbp4NyykJxhEbmBsQSC6rQroZWCcFg9xw%40mail.gmail.com. [-- Attachment #2: Type: text/html, Size: 1375 bytes --] ^ permalink raw reply [flat|nested] 17+ messages in thread

*Re: [HoTT] Free higher groups2023-04-29 19:06 ` Jasper Hugunin@ 2023-05-02 8:35 ` 'Thorsten Altenkirch' via Homotopy Type Theory2023-05-02 8:48 ` 'Thorsten Altenkirch' via Homotopy Type Theory 0 siblings, 1 reply; 17+ messages in thread From: 'Thorsten Altenkirch' via Homotopy Type Theory @ 2023-05-02 8:35 UTC (permalink / raw) To: Jasper Hugunin, Homotopy Type Theory [-- Attachment #1: Type: text/plain, Size: 9324 bytes --] One option would be the solution to the coherence problem for Categories with Families (CWFs). Define a wild CWF as a CWF-algebra with no truncation. The question is whether the usual set-truncated initial CWF is weakly initial for wild CWFs. By initial I mean given a set of generating types and terms (otherwise everything is empty). We don’t yet have a construction for this even using 2LTT but we think it should be possible using semi-simplicial types. On the other hand we should be able to encode semi-simplicial types in the initial CWF (ok we may need some Pi-types) and hence the solution to the coherence pro0blem would imply the constructability of semi-simplicial types. Thorsten From: homotopytypetheory@googlegroups.com <homotopytypetheory@googlegroups.com> on behalf of Jasper Hugunin <jasper@hugunin.net> Date: Saturday, 29 April 2023 at 20:08 To: Homotopy Type Theory <homotopytypetheory@googlegroups.com> Subject: Re: [HoTT] Free higher groups Another example constructible in HTS but maybe not in HoTT is the large type of semi-simplicial types (On the Role of Semisimplicial Types - Nicolai Kraus<http://www.cs.nott.ac.uk/~psznk/docs/on_semisimplicial_types.pdf>). 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 have). On Saturday, April 29, 2023 at 11:57:36 AM UTC-7 Dan Christensen 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: https://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: >> >> 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. >> >> Dan >> >> On Apr 28, 2023, Michael Shulman <shu...@sandiego.edu> wrote: >> >>> The existence of hypercompletion is a good suggestion. >>> >>> 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 presumed to >>> fail in HoTT. But it's nice to have one that involves higher types too. >>> >>> On Mon, Apr 24, 2023 at 5:37 PM Dan Christensen <j...@uwo.ca> wrote: >>> >>> 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) = (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. >>> >>> 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. >>> >>> Oh, what about whether the hypercomplete objects are the modal >>> objects >>> for a modality? I'm throwing this out there without much thought... >>> >>> Dan >>> >>> On Apr 24, 2023, Michael Shulman <shu...@sandiego.edu> wrote: >>> >>>> 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. >>>> >>>> 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? >>>> >>>> On Fri, Apr 21, 2023 at 5:25 PM Nicolai Kraus >>>> <nicola...@gmail.com> wrote: >>>> >>>> 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 PM Jon Sterling >>>> <j...@jonmsterling.com> 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ärn 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 >>>> HomotopyTypeThe...@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 "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 >>>> >>> https://groups.google.com/d/msgid/HomotopyTypeTheory/D102F774-D134-46B9-A70A-51CB84BE4B6F%40jonmsterling.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 >>> HomotopyTypeThe...@googlegroups.com. >>>> To view this discussion on the web visit >>>> >>> https://groups.google.com/d/msgid/HomotopyTypeTheory/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 HomotopyTypeThe...@googlegroups.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 >> 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 >> 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 email to HomotopyTypeTheory+unsubscribe@googlegroups.com<mailto: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<https://groups.google.com/d/msgid/HomotopyTypeTheory/73121272-421b-4dba-943f-b81f32854862n%40googlegroups.com?utm_medium=email&utm_source=footer>. This message and any attachment are intended solely for the addressee and may contain confidential information. If you have received this message in error, please contact the sender and delete the email and attachment. Any views or opinions expressed by the author of this email do not necessarily reflect the views of the University of Nottingham. Email communications with the University of Nottingham may be monitored where permitted by law. -- 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/PAXPR06MB78693F3A96A29DB127C274E9CD6F9%40PAXPR06MB7869.eurprd06.prod.outlook.com. [-- Attachment #2: Type: text/html, Size: 16361 bytes --] ^ permalink raw reply [flat|nested] 17+ messages in thread

*2023-05-02 8:35 ` 'Thorsten Altenkirch' via Homotopy Type TheoryRe: [HoTT] Free higher groups@ 2023-05-02 8:48 ` 'Thorsten Altenkirch' via Homotopy Type Theory0 siblings, 0 replies; 17+ messages in thread From: 'Thorsten Altenkirch' via Homotopy Type Theory @ 2023-05-02 8:48 UTC (permalink / raw) To: Jasper Hugunin, Homotopy Type Theory [-- Attachment #1: Type: text/plain, Size: 10901 bytes --] Actually it is sufficient to construct a morphism to tge wild CWF of types. Sent from Outlook for iOS<https://aka.ms/o0ukef> ________________________________ From: 'Thorsten Altenkirch' via Homotopy Type Theory <HomotopyTypeTheory@googlegroups.com> Sent: Tuesday, May 2, 2023 9:35:55 AM To: Jasper Hugunin <jasper@hugunin.net>; Homotopy Type Theory <homotopytypetheory@googlegroups.com> Subject: Re: [HoTT] Free higher groups One option would be the solution to the coherence problem for Categories with Families (CWFs). Define a wild CWF as a CWF-algebra with no truncation. The question is whether the usual set-truncated initial CWF is weakly initial for wild CWFs. By initial I mean given a set of generating types and terms (otherwise everything is empty). We don’t yet have a construction for this even using 2LTT but we think it should be possible using semi-simplicial types. On the other hand we should be able to encode semi-simplicial types in the initial CWF (ok we may need some Pi-types) and hence the solution to the coherence pro0blem would imply the constructability of semi-simplicial types. Thorsten From: homotopytypetheory@googlegroups.com <homotopytypetheory@googlegroups.com> on behalf of Jasper Hugunin <jasper@hugunin.net> Date: Saturday, 29 April 2023 at 20:08 To: Homotopy Type Theory <homotopytypetheory@googlegroups.com> Subject: Re: [HoTT] Free higher groups Another example constructible in HTS but maybe not in HoTT is the large type of semi-simplicial types (On the Role of Semisimplicial Types - Nicolai Kraus<http://www.cs.nott.ac.uk/~psznk/docs/on_semisimplicial_types.pdf>). 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 have). On Saturday, April 29, 2023 at 11:57:36 AM UTC-7 Dan Christensen 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: https://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: >> >> 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. >> >> Dan >> >> On Apr 28, 2023, Michael Shulman <shu...@sandiego.edu> wrote: >> >>> The existence of hypercompletion is a good suggestion. >>> >>> 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 presumed to >>> fail in HoTT. But it's nice to have one that involves higher types too. >>> >>> On Mon, Apr 24, 2023 at 5:37 PM Dan Christensen <j...@uwo.ca> wrote: >>> >>> 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) = (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. >>> >>> 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. >>> >>> Oh, what about whether the hypercomplete objects are the modal >>> objects >>> for a modality? I'm throwing this out there without much thought... >>> >>> Dan >>> >>> On Apr 24, 2023, Michael Shulman <shu...@sandiego.edu> wrote: >>> >>>> 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. >>>> >>>> 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? >>>> >>>> On Fri, Apr 21, 2023 at 5:25 PM Nicolai Kraus >>>> <nicola...@gmail.com> wrote: >>>> >>>> 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 PM Jon Sterling >>>> <j...@jonmsterling.com> 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ärn 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 >>>> HomotopyTypeThe...@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 "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 >>>> >>> https://groups.google.com/d/msgid/HomotopyTypeTheory/D102F774-D134-46B9-A70A-51CB84BE4B6F%40jonmsterling.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 >>> HomotopyTypeThe...@googlegroups.com. >>>> To view this discussion on the web visit >>>> >>> https://groups.google.com/d/msgid/HomotopyTypeTheory/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 HomotopyTypeThe...@googlegroups.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 >> 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 >> 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 email to HomotopyTypeTheory+unsubscribe@googlegroups.com<mailto: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<https://groups.google.com/d/msgid/HomotopyTypeTheory/73121272-421b-4dba-943f-b81f32854862n%40googlegroups.com?utm_medium=email&utm_source=footer>. This message and any attachment are intended solely for the addressee and may contain confidential information. If you have received this message in error, please contact the sender and delete the email and attachment. Any views or opinions expressed by the author of this email do not necessarily reflect the views of the University of Nottingham. Email communications with the University of Nottingham may be monitored where permitted by law. -- 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<mailto:HomotopyTypeTheory+unsubscribe@googlegroups.com>. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/PAXPR06MB78693F3A96A29DB127C274E9CD6F9%40PAXPR06MB7869.eurprd06.prod.outlook.com<https://groups.google.com/d/msgid/HomotopyTypeTheory/PAXPR06MB78693F3A96A29DB127C274E9CD6F9%40PAXPR06MB7869.eurprd06.prod.outlook.com?utm_medium=email&utm_source=footer>. This message and any attachment are intended solely for the addressee and may contain confidential information. If you have received this message in error, please contact the sender and delete the email and attachment. Any views or opinions expressed by the author of this email do not necessarily reflect the views of the University of Nottingham. Email communications with the University of Nottingham may be monitored where permitted by law. -- 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/PAXPR06MB78695C1CF6057EC48042EC03CD6F9%40PAXPR06MB7869.eurprd06.prod.outlook.com. [-- Attachment #2: Type: text/html, Size: 17665 bytes --] ^ permalink raw reply [flat|nested] 17+ messages in thread

end of thread, other threads:[~2023-05-02 8:49 UTC | newest]Thread overview:17+ messages (download: mbox.gz / follow: Atom feed) -- links below jump to the message on this page -- [not found] <AQHZesxzxECCXAdlIUadD6wxcH+RXA==> 2023-04-21 10:04 ` [HoTT] Free higher groups David Wärn 2023-04-21 11:28 ` [HoTT] " Ulrik Buchholtz 2023-04-21 14:32 ` [HoTT] " Peter LeFanu Lumsdaine 2023-04-21 18:30 ` Jon Sterling 2023-04-22 0:24 ` Nicolai Kraus 2023-04-25 0:02 ` Michael Shulman 2023-04-25 0:37 ` Dan Christensen 2023-04-28 17:59 ` Michael Shulman 2023-04-29 17:37 ` Dan Christensen 2023-04-29 18:37 ` Steve Awodey 2023-04-29 18:49 ` Ulrik Buchholtz 2023-04-29 19:22 ` Steve Awodey 2023-04-30 0:43 ` Michael Shulman 2023-04-29 18:57 ` Dan Christensen 2023-04-29 19:06 ` Jasper Hugunin 2023-05-02 8:35 ` 'Thorsten Altenkirch' via Homotopy Type Theory 2023-05-02 8:48 ` 'Thorsten Altenkirch' via Homotopy Type Theory

This is a public inbox, see mirroring instructions for how to clone and mirror all data and code used for this inbox; as well as URLs for NNTP newsgroup(s).