prove twist hexagon in twist construction

[Alizter]

We finally prove the remaining hexagon consisting of only twists that was left as a WIP. It uses two instances of the 9-gon meaning it isn't equivalent to it in any way.

[Alizter]

ping @jdchristensen

[jdchristensen]

@Alizter I'm really sorry for forgetting about this. I will review it this week. Can you rebase so that it builds with Rocq 9.1?

[jdchristensen]

@Alizter This LGTM!

I've pushed a commit that just moves the preservations of squares section to what looks like a better spot in the file. Then I made a few other minor cleanups to MonoidalTwistConstruction.v, including noticing that essentially the same assertion was proved twice.

The long proof looks like the kind of thing that setoid rewriting would make a lot more readable. Thomas and I are finding it wonderful, so we hope to be able to move it into the main library soon. (ping @patrick-nicodemus :-) Also the lhs' and rhs' tactics can slightly simplify some of the steps here. No need to edit, though.

I also noticed that there are lots of results like moveL_fmap01_braidL with complicated proofs. Shouldn't they all be special cases of some general "we can move an equivalence across a 2-cell" result? (We have a couple of these specifically for 0-groupoids in ZeroGroupoid.v, and I added a couple more there in WIP.) But this comment is more an idea for future work, not for this PR.

PS: I'll be pretty busy for the rest of the month, but I will have more time next semester.

PPS: I'm giving a Zoom talk on Thursday at 16:25 UK time about formalization work in Coq-HoTT which you will probably be interested in: https://tdejong.com/mhe60/

[patrick-nicodemus]

Thank you for the reminder. I'll spend some more time looking into this this weekend.