Zigzag construction of identity types of pushouts

[VojtechStep]

There are still two holes left to fill, but they seem to be conceptually easy enough that I'm confident publishing this draft PR now — in particular they don't have any important coherence content, and they should be provable from very general path algebra; essentially I need to (freely) give a homotopy which fits into a coherence diagram with various is-section-map-inv-equivs, is-retraction-map-inv-equivs, preserves-trs etc.

What needs to be done:

• Fill the two holes
• Factoring out general lemmas — functoriality-stuff and stuff-over have a lot of ad-hoc development
• Naming — goes with the above
• Marking things abstract/opaque, general optimizations — the new stuff takes about as much time to typecheck as the rest of the library. I would be surprised if the CI didn't error on insufficient memory. This is fixable, but will take some time
• Prose

Ideally I'd also like to avoid relying on the computation of map-eq-transpose-equiv', which at least compute-square-over-zigzag-square-over-colimit-id does

[VojtechStep]

I just pushed the solution to the the last hole, making this the first complete proof of correctness of the zigzag construction. 🎉

As noted in the PR description there's still quite some work necessary to make it mergeable, but the formal result is 100% there.

I'll be a little self indulgent and give this the 🏆 milestone 🏆 label.

[VojtechStep]

As expected, the CI fails on insufficient memory