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.