An interchange law for squares and cleanups to Cubical/PathSquare.v

[marcbezem]

As asked by @Alizter .

One simplification added, using the library (experimental is not used, but reminds me of the plan). I'm still thinking what should be remember-ed to get from h0j back to sq01.

[marcbezem]

I guess I need some help. I added some missing definitions, as indicated by Dan (sq_concat_v_1s and some more, see the diff). Now I can easily reduce interchange to ... Eckman-Hilton, funnily. However, this goes via a proof by path induction on h0j = 1 and vj0 = 1. So we know that these are 1 by reflexivity, and this should imply that sq01, sq10 are 1-squares. Then the instance of E-H is trivial. I do not manage to remember enough information to do this last step, see an attempt of rememberin a comment. Of course, I could simply be mistaken, but for the moment I prefer to think that the problem is my lack of RoQC-skill to pick the right induction tactic.

[jdchristensen]

I figured out that you can write induction principles for square that only require one of the edges to be free. They make this proof trivial, and probably make other proofs trivial too. So the file can probably be rearranged so that these are earlier and they are used more often. They depend on the Kan fillers, but those have no dependencies, so could appear near the start of the file. I have to run and will be busy for a day or two, so feel free to keep working on these things.

[jdchristensen]

I also made the notations available if you want to use them. BTW, you should read the commits separately, as the changes will be easier to understand that way.

[marcbezem]

Thanks, Dan, this is real progress. Let me add the 3+2 missing cases and think a bit more.

[marcbezem]

The new pathsquare_ind_? functions are very powerful. Surprisingly, only one suffices!

[jdchristensen]

The new pathsquare_ind_? functions are very powerful.

Thanks for adding the other versions.

Surprisingly, only one suffices!

Oh, nice observation. In fact, you can get by with only two of the four squares being eliminated:

  destruct sq11; simpl.
  destruct vi2, h2i, vi1, h1i; simpl.
  revert vj0 sq10; rapply pathsquare_ind_l; simpl.
  by destruct vi0.

But the proof is a bit longer than what you came up with, so I prefer yours. My proof destructs one extra edge (10 instead of 9), but one fewer square. Edit: Actually, yours destructs 11 edges and 3 squares, while mine destructs 10 edges and 2 squares.

[Alizter]

FTR we had a discussion before about using the equivalent definition of a square using paths directly and the transition mainly went smoothly. The only proof I recall getting stuck at was the T=S1xS1 proof in Homotopy/Torus. This was my original motivation for introducing these kinds of squares originally. I'm thinking that these single edge induction principles might help out with the Torus proof actually, but I won't dwell too much on it here.

[jdchristensen]

FTR we had a discussion before about using the equivalent definition of a square using paths directly and the transition mainly went smoothly.

What do you mean by "the transition"? PathSquare doesn't yet use the path definition, so you must be talking about somewhere else in the library?

[Alizter]

Sorry I wasn't clear in my message. I meant that when I tried to redefine PathSquare using the path definition.

[marcbezem]

I did some clean up and feel we could update from draft PR to full PR. Feel free to clean up a bit more.

I'm planning a follow up, but have still to think about it. Also, I'm unsure where to put it.
It's about formalizing a sketch by Ulrik Buchholtz of an alternative proof of Lemma 2.7(3) from his joint paper with Dan et al. https://arxiv.org/pdf/2301.02636, using squares.

[jdchristensen]

I'll do a bunch of clean-up before we mark this as non-draft. I'll also squash and then unsquash a bit, to have a clean history. This will involve force-pushing, so don't make any other changes in the meantime, @marcbezem .

[jdchristensen]

I'm planning a follow up, but have still to think about it. Also, I'm unsure where to put it.
It's about formalizing a sketch by Ulrik Buchholtz of an alternative proof of Lemma 2.7(3) from his joint paper with Dan et al. https://arxiv.org/pdf/2301.02636, using squares.

This is in Homotopy/HSpace/Core.v (search for "2301" in that file). The current proof is quite short, but does unnecessarily rely on function extensionality. It would be nice to have a proof that doesn't use Funext, but I'm not sure that squares will be easier than just doing this directly. If you want to try, that would be interesting to see. I guess that same HSpace/Core.v file would be the right place.

[jdchristensen]

@Alizter This is ready for review now. I broke it up into logical commits. One of the commits changes lots of comments, and another moves something, so it's best if you view the commits separately when reviewing. @marcbezem If you can give this a quick look, that would be great.

[jdchristensen]

(Force pushed again just to fix typo in commit message.)

[Alizter]

This is looking much better, thank you both for your work.

[Alizter]

Here is a diagram that may aid readers:

        h0i          h0j
   a00 ━━━━━━━━ a01 ━━━━━━━━ a02
    ┃            ┃            ┃
    ┃  sq00      ┃  sq01      ┃
vi0 ┃        vi1 ┃            ┃ vi2
    ┃            ┃            ┃
    ┃   h1i      ┃   h1j      ┃
   a10 ━━━━━━━━ a11 ━━━━━━━━ a12
    ┃            ┃            ┃
    ┃  sq10      ┃  sq11      ┃
vj0 ┃        vj1 ┃            ┃ vj2
    ┃            ┃            ┃
    ┃   h2i      ┃   h2j      ┃
   a20 ━━━━━━━━ a21 ━━━━━━━━ a22

[jdchristensen]

Nice! I've added that, including the unicode, with << >> markers. Let's see how it looks in the generated documentation. @Alizter Can you remind me where I can find the coqdoc/alectryon documentation that the CI generates?

[Alizter]

It's not possible to view it in the CI for a PR (online), but the main CI will upload and host the artefacts. Links to the hosted docs are on the wiki https://github.com/HoTT/Coq-HoTT/wiki

[Alizter]

If you go to the specific CI job there is an upload artifact step which gives you a link to download the produced docs. That's technically one way you can view it.

[Alizter]

I don't see the diagram in the recent commit btw, did you push it?

[jdchristensen]

Whoops, I only commited part of the changes I made. I just force pushed to fix the last commit.

[jdchristensen]

We can just merge this once @marcbezem takes a look, and then check the documentation at that point.

[jdchristensen]

Since I changed the title, I'll say explicitly that this finishes the work started in #2325, which was not actually merged.

[marcbezem]

Looks good to me!

[jdchristensen]

For the record, the documentation looks fine.

[marcbezem]

Thanks! Shall I delete the interchange branch now?

[jdchristensen]

Thanks! Shall I delete the interchange branch now?

Yep!