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:
[x] Fundamental James Splitting: ΣΩΣX ≃ ΣX ∨ (X ∧ ΣΩΣX).
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).
[X] The pushout of X ← X ∨ Y → X is contractible.
[X] Σ(X ⋀ Y) ≃ X join Y.
[x] the fiber of X ∨ Y → X × Y is Σ(ΩX ∧ ΩY).
[X] 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:
[X] Suspension is equivalent to pushout of 1 ← X → 1, but the 1 is Unit* because of universe level shenanigans.
[X] Pushout of 1 ← 1 → X is X; Pushout of 1 ← X = X is 1.
[X] The pasting lemma for pushouts. Seems like it is already in #1133, so I'm basing my work off of that.
I'm making some headway in formalizing the paper
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:
(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!Unit*because of universe level shenanigans.