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:

• [x] 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