Zigzags of sequential diagrams

UniMath / agda-unimath

The agda-unimath library

https://unimath.github.io/agda-unimath/

MIT License

219 stars 70 forks source link

Zigzags of sequential diagrams #1129

Closed VojtechStep closed 4 months ago

VojtechStep commented 5 months ago

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 commented 5 months ago

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 commented 5 months ago

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