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.