Formalizing Devalapurkar & Haine

[Trebor-Huang]

I'm making some headway in formalizing the paper

• Devalapurkar and Haine, On the James and Hilton–Milnor splittings, & the metastable EHP sequence.

And I'd like to contribute this to the cubical library. But before that I want to confirm I'm not repeating work, and that these are suitable for the library. Here's a list of things to prove:

• Main results:
  • Fundamental James Splitting: ΣΩΣX ≃ ΣX ∨ (X ∧ ΣΩΣX).
  • Fundamental Hilton–Milnor Splitting: Ω(X ∨ Y) ≃ ΩX × ΩY × ΩΣ(ΩX ∧ ΩY).
  • These both have infinitary versions, but the proof in Devalapurkar and Haine reduces them to presheaf toposes, which are hypercomplete. I wonder if it is provable in HoTT without additional assumptions.
  • Metastable EHP: I think this is out of reach.
• Funny intermediary results:
  • Mather's cube theorems (I think the HoTT-flavored version is the flattening lemma, which is much easier to use than fiddling with cubes).
  • The pushout of X ← X ∨ Y → X is contractible.
  • Σ(X ⋀ Y) ≃ X join Y.
  • the fiber of X ∨ Y → X × Y is Σ(ΩX ∧ ΩY).
  • If A is the fiber of B → C, and ΩB → ΩC has a section, then ΩB is equivalent to ΩA × ΩC. (I tried to prove it directly but it seems to require a large coherence result between 2-paths.) @ecavallo found a very succint proof, nice!
  • The dual statement for suspensions.
• Little lemmas:
  • Suspension is equivalent to pushout of 1 ← X → 1, but the 1 is Unit* because of universe level shenanigans.
  • Pushout of 1 ← 1 → X is X; Pushout of 1 ← X = X is 1.
  • The pasting lemma for pushouts. Seems like it is already in Connected CW complexes #1133, so I'm basing my work off of that.