Re: [HoTT] Free higher groups

[Peter LeFanu Lumsdaine <p.l.lumsdaine@gmail.com>]

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