Descent data for sequential colimits and its version of the flattening lemma

[VojtechStep]

Sorry, this is bigger than I anticipated...

This PR

• defines morphisms and equivalences between dependent sequential diagrams
• defines morphisms and equivalences of cocones under morphisms and equivalences of sequential diagrams
• defines equifibered sequential diagrams
• defines descent data for sequential colimits
• shows the descent property of sequential colimits
• proves a version of the flattening lemma expressed with families with associated descent data
• collects various helpers for converting between sequential stuff and coequalizer stuff into one file
• adds some auxiliary infrastructure along the way

I took care to properly separate the work into commits, so it might be more digestible to review it commit by commit.

This is progress towards #1080

[fredrik-bakke]

I looked over pentagons again, and the comments that were left unresolved, and it looks good to me now aside from the new comments I added