Sequential colimits

[VojtechStep]

Definitions and proofs:

• Define sequential diagrams
• Define dependent sequential diagrams
• Define constantly dependent sequential diagrams
• Show that constantly dependent sequential diagrams correspond to regular sequential diagrams
• Define morphisms of sequential diagrams
• Define equivalences of sequential diagrams
• Characterize equality of sequential diagrams
• Characterize equality of dependent sequential diagrams
• Characterize equality of morphisms of sequential diagrams
• Define cocones under sequential diagrams and their homotopies
• Define dependent cocones under sequential diagrams and their homotopies
• Define the universal property of sequential colimits
• Define the dependent universal property of sequential colimits
• Show they are logically equivalent
• Define standard sequential colimits Standard sequential colimit and its functoriality #868
• Functoriality of morphisms of sequential diagrams Standard sequential colimit and its functoriality #868
• Diagram shifting preserves colimits Standard sequential colimit and its functoriality #868
• Flattening lemma Flattening lemma for sequential colimits #869

Meta:

• Prose
• "Sequential diagram" or "Cotower"? I'm keeping "sequential diagram"
• Should -sequential-diagram be written at the very end of names or not?

[EgbertRijke]

Whoah, that summary of your PR is epic! 🤯

[EgbertRijke]

Btw it would be totally ok (read: preferred) if you wrap this PR up when you showed that the universal property and dependent universal property are equivalent.

I'm a big fan of not trying to do everything in a PR. So you don't have to do the whole theory of sequential colimits in one go. That will also give us a chance to check in with how you're doing things before you go all the way.

[VojtechStep]

Btw it would be totally ok (read: preferred) if you wrap this PR up when you showed that the universal property and dependent universal property are equivalent.

Makes sense, I'll do that; I actually wrote down a short (read: two A4s) cheatsheet for adding new diagrams and (co)limits to the library, I should probably note down somewhere "try to split it into manageable chunks" 😅.

[fredrik-bakke]

• "Sequential diagram" or "Cotower"?

I'm still rooting for cotower 😬🤞

[EgbertRijke]

• "Sequential diagram" or "Cotower"?

I'm still rooting for cotower 😬🤞

Lol I really prefer sequential diagram

[EgbertRijke]

Btw it would be totally ok (read: preferred) if you wrap this PR up when you showed that the universal property and dependent universal property are equivalent.

Makes sense, I'll do that; I actually wrote down a short (read: two A4s) cheatsheet for adding new diagrams and (co)limits to the library, I should probably note down somewhere "try to split it into manageable chunks" 😅.

Sounds like a good thing to write up as an issue

[VojtechStep]

I think I prefer cotower, but I'm already used to sequential-diagram, and that balances out, so I'll let you two battle it out in the marketplace of ideas 😃

[EgbertRijke]

My reason to prefer sequential-diagram is that this terminology is intuitive to a wider audience than the readers of the nlab, and agda-unimath is about bringing univalent mathematics to a wider audience.

Your turn Fredrik :D

[fredrik-bakke]

I just don't see how cotower is so inaccessible. It's less wordy than sequential-diagram, which seems a little too generic to me, and cotower has a direct interpretation in relation to our now-established tower. I don't find cotower particularly unreadable, especially if one tries to determine what a tower should be first.

[fredrik-bakke]

How about we compromise by finding yet another name? For instance, we can call it a "well", "shaft" or "chasm"! 😁

[fredrik-bakke]

I also want to point out it is still undetermined what the dual of a "sequential diagram" would be called

[fredrik-bakke]

And I think the terminology should be consistent between the two notions.

That being said, I will give you the upper-hand since you wrote the literal source on colimits of sequential diagrams in HoTT. If you are still of the opinion that we should use this terminology, then I will concede

[EgbertRijke]

I also want to point out it is still undetermined what the dual of a "sequential diagram" would be called

I'd call it contravariant sequential diagram, but we can also call it tower:)

[EgbertRijke]

And I think the terminology should be consistent between the two notions.

That being said, I will give you the upper-hand since you wrote the literal source on colimits of sequential diagrams in HoTT. If you are still of the opinion that we should use this terminology, then I will concede

Aww is that how you battle? 🙃

[fredrik-bakke]

Aww is that how you battle? 🙃

We can also take it outside, of course. If you prefer

[EgbertRijke]

Aww is that how you battle? 🙃

We can also take it outside, of course. If you prefer

Romantic 🥰

[VojtechStep]

This PR should be functionally complete - I opened #868 and #869 for the unfinished checkboxes, and I'll start writing prose for what's formalized here.

[EgbertRijke]

Can you update and mark it ready for review whenever you're ready?

[VojtechStep]

Of course, I wanted to just give a short update - it should be ready for review by Monday.

[EgbertRijke]

Alright, I'll be patient:)

[VojtechStep]

Alright, this one's ready for review

[fredrik-bakke]

I just want to record this here before Egbert takes it back:

Now I think we can use cotower too:)

To the learning experience 🍻

#871 (comment)

🙂

[fredrik-bakke]

I see you've struck out standard sequential colimits. Are you leaving that for future work, or is there another reason for it?

[VojtechStep]

I see you've struck out standard sequential colimits. Are you leaving that for future work, or is there another reason for it?

I've opened new issues for the unfinished work, I'll link them in the PR description

[VojtechStep]

I plan on coming back to them, but Egbert suggested above that there's no need to have everything in one big PR and I agree.

[EgbertRijke]

💯% approve 🤘

[VojtechStep]

Thanks for wrapping it up, I unfortunately got preoccupied with work stuff 👍