It'd be great to see this done! I've been wanting to see this for a while, but haven't gotten anyone to do it. One remark on that part of the video: the syllepsis gives the proof that the "Brunerie number" is 1 or 2, but it doesn't immediately let you exclude the possibility that it's 1. I think my student Nachiket Karnick and I do understand how to show that the number is 2 (with a much more direct calculation than what's in the second half of Brunerie's thesis, but still using the James construction). I have an outline of an even more direct proof, but the syllepsis is one of the calculations required to make this more direct approach work. Which is all to say that I'm very interested in seeing this result, especially if it meant that related calculations of similar difficulty could be done thereby giving much more direct calculations of the small homotopy groups of spheres. Best, Noah On Fri, Mar 5, 2021 at 1:40 PM Jamie Vicary wrote: > Hi Kristina, that's great. I don't know that anyone's done this before. > > > Given two higher paths p, q : 1_x = 1_x > > I guess you mean p,q:1_(1_x) = 1_(1_x) ? > > Best wishes, > Jamie > > -- > 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/CANr23v3E%2BkaPKgL-So_s_h95KUwSM5i1vPSqzQyEmKa%3D_D46iQ%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/CAO0tDg4oCaZ--OuOVDynT5sXK5jQh1%2BOTM2FNzpx-QLEUg73Ng%40mail.gmail.com.