Zigzags of sequential diagrams

[VojtechStep]

In this PR I

• compute the maps induced by functoriality on inclusion morphisms of shifts of sequential diagrams
• define zigzags between sequential diagrams
• show that both maps of colimits induced by a zigzag are equivalences

[VojtechStep]

This PR is ready for review. A big chunk of the added lines is prose and diagrams, so it seems bigger than it is. Again, the commits are self-contained, so the PR should be reviewable commit-by-commit if it makes it easier.

[VojtechStep]

Thanks for the review. I tried to address all your comments either in code, or in the conversations