Re: [HoTT] Free higher groups

[Michael Shulman <shulman@sandiego.edu>]

[-- 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 --]