cubical Devalapurkar & Haine

This is a formalization of results described in #1147, with the two main results being the stable James splitting ΣΩΣX ≃ ΣX ⋁ Σ(X ⋀ ΩΣX) and the Hilton–Milnor splitting Ω(X ⋁ Y) ≃ ΩX × ΩY × ΩΣ(ΩY ⋀ ΩX). ~~It still needs cleaning up and merging with #1151, but most of it is done.~~

I'm putting the HM splitting in the Homotopy folder, but the James splitting in the HITs.James folder, because the latter result is quite related to what's already in there.

Sep 19 '24 11:09 Trebor-Huang

Oh wait, should I rebase on #1133?

Sep 19 '24 11:09 Trebor-Huang

Another question is, should I add the public imports in Cubical.HITs.James and Cubical.HITs.Susp for the new lemmas?

Sep 19 '24 13:09 Trebor-Huang

This should be everything, so it's ready for review.

Sep 19 '24 15:09 Trebor-Huang

I went ahead and made some changes, particularly to prefer copatterns over record syntax where it's not too inconvenient and to make some type signatures more explicit. Does everything look OK to you? If so (and CI passes) I will merge.

Mar 20 '25 17:03 ecavallo

Yes, this looks great!

Mar 21 '25 05:03 Trebor-Huang

Thanks for the contribution (and sorry for the long wait)!

Mar 21 '25 05:03 ecavallo