Shifts and unshifts of concepts around sequential colimits

[VojtechStep]

This PR formalizes shifts of sequential diagrams, morphisms of sequential diagrams, cocones of sequential diagrams, homotopies of cocones of sequential diagrams, and unshifts of the last two. This machinery is used to show that dropping any finite number of vertices from the beginning of a sequential diagram gives an equivalent sequential colimit.

It also adds a page for the formalization of the paper, with references to the formalized parts. See the attached screenshot.

The formalization page has a lot of TODOs left, which I am planning to formalize in the future #1080.

[VojtechStep]

I made the scope of this PR smaller so that we could potentially merge it sooner. I'm marking it ready for review.

[fredrik-bakke]

Here's a preliminary review. I did not look closer at the prose in the SRD20 module, and did not look at the formalization of shifts

[fredrik-bakke]

Some more comments :) (still an incomplete review)

[VojtechStep]

@EgbertRijke could I eventually get your input, mainly on the organization of the Papers section? Not to discourage you from looking at the rest of the PR.

[EgbertRijke]

@EgbertRijke could I eventually get your input, mainly on the organization of the Papers section? Not to discourage you from looking at the rest of the PR.

Yep! Tonight I have other plans, but I will have a look over the weekend.

[fredrik-bakke]

Although I would like to have this PR merged soon, I feel uneasy about merging this before we decide on the proper way to name the papers files, as otherwise, the credit to the original author of the file may be lost on potential subsequent renamings. Can we perhaps factor out the papers addition into a separate PR?

[VojtechStep]

I agree; on it