Devalapurkar & Haine

[Trebor-Huang]

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]

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

[Trebor-Huang]

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

[Trebor-Huang]

(replying to @aljungstrom on another issue) It's this line and/or possibly other similar lines. Agda is checking the middle function of the two squares agree, so that we can apply the pasting lemma. Strangely when I evaluated each field of the commSquare record they returned instantly, but it gets stuck for a couple seconds and a few GB of memory when I try to evaluate the entire record.

[Trebor-Huang]

See the comments slightly above for a commutative diagram of what's happening.

[ecavallo]

@aljungstrom Do you have any ideas to get this compiling? I played with it a while but with no success. Evidently Agda is stalling out trying to understand that bottomSquare is the same as pushoutD .fst.

[ecavallo]

In case it wasn't clear, pushoutAB checks fine on my machine but the later pushoutCD hangs, which is the one I was talking about above. For me it's specifically the proofs that these are commutative squares that are problematic, the other components check instantly:

      test : pushoutD .fst .sp ≡ bottomSquare .sp
      test = refl -- instant

      test₁ : pushoutD .fst .inlP ≡ bottomSquare .inlP
      test₁ = refl -- instant

      test₂ : pushoutD .fst .inrP ≡ bottomSquare .inrP
      test₂ = refl -- instant

      test₃ : pushoutD .fst .commSquare.comm ≡ bottomSquare .commSquare.comm
      test₃ = {!refl!} -- hangs

[ecavallo]

Moving the equivalence involved in the definition of wedgePushout into an opaque block seems to work! Have to check that it doesn't break anything later on though.

[Trebor-Huang]

This is interesting. If I remember correctly all these equations should be true purely formally, so some strategic opaque blocks should solve the issue. I wonder if the extendPushoutSquare lemma should make the commutativity witness opaque by default.

[ecavallo]

Yeah, bottomSquare is really exactly pushoutD .fst, just after unpacking to give arguments to PushoutPasteDown and then repacking. The definition of the commutativity square in extendPushoutSquare itself is simple, but I think it's triggering a comparison of the (underlying function of) this complicated equivalence to itself. So my guess (not knowing too much about Agda internals...) is that making the equivalence opaque is the simplest solution.

It could be annoying if you later want to use what the SuspProduct equivalence actually does, though.

[ecavallo]

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.

[Trebor-Huang]

Yes, this looks great!

[ecavallo]

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