search

agda / cubical

An experimental library for Cubical Agda
https://agda.github.io/cubical/Cubical.README.html
Other
459 stars 141 forks source link

Devalapurkar & Haine #1157

Open Trebor-Huang opened 2 months ago

Trebor-Huang commented 2 months ago

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.

Trebor-Huang commented 2 months ago

Oh wait, should I rebase on #1133?

Trebor-Huang commented 2 months ago

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

Trebor-Huang commented 2 months ago

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