Sequential limits

[fredrik-bakke]

Summary

• Defines towers of types, dependent towers of types, maps of towers, equivalences of towers, cones over towers, sequential limits, standard sequential limits, transfinite cocomposition
• Do some adjacent refactoring
• Characterize equality of towers, maps of towers, cones of towers, sequential limits
• Characterize equality in standard sequential limits

[VojtechStep]

I'm coincidentally working on the dual notion of sequential colimits

[VojtechStep]

Btw at some point I had a discussion with @EgbertRijke about (co)towers, and he suggested the names sequential-diagram for cotower and contravariant-sequential-diagram for tower; I'm using sequential-diagram at the moment, but I'm not opposed to switching to cotower.

[fredrik-bakke]

Oh! I was planning on doing cotowers next, by dualizing this PR

[fredrik-bakke]

I discussed the terminology with Egbert a moment ago as well. He was okay with Cotower, but we agreed on sequential-limit for the limit

[EgbertRijke]

Oh yeah I forgot that I suggested "sequential diagram" as terminology. So when I was discussing with Fredrik I forgot, and he won because I was only talking about sequences.

How about sequential diagrams, Fredrik?:)

[EgbertRijke]

I'm coincidentally working on the dual notion of sequential colimits

Make a draft PR, so that we can see that you're working on it

[EgbertRijke]

Oh! I was planning on doing cotowers next, by dualizing this PR

Actually I think this PR will be better if it only does towers and sequential limits. Don't try to do everything in a PR.

[fredrik-bakke]

No worries. I will do it.

I won't stop you, but I'd like to discuss with you at some point how useful such a thing is, to what extent it should be done, and when it is okay to remove/omit external links.

[VojtechStep]

Are you about to start adding various unrelated tables to this PR? 👀

[fredrik-bakke]

Are you about to start adding various unrelated tables to this PR? 👀

I am also adding a table about sequential limits. I wrote the table of fibers together with pullbacks, and then concluded they didn't fit together. I added the table as a separate one instead rather than deleting it, as I am not a fan of deleting work that is useful.

[fredrik-bakke]

Is there a convention for how to order the reference tables yet? I find that the alphabetic ordering may not be the best one. Let me know if you have objections to the current order I wrote them in.

[fredrik-bakke]

otherwise I think this PR is mostly done now

[EgbertRijke]

Is there a convention for how to order the reference tables yet? I find that the alphabetic ordering may not be the best one. Let me know if you have objections to the current order I wrote them in.

The convention is the alphabetic ordering. Why is it not the best convention?

[fredrik-bakke]

It seems to me like unrelated entries end up together, making the table somewhat harder to navigate. Maybe you can have a look at the diff of the commit reorder table entries and see if you dis-/agree with me?

[EgbertRijke]

It seems to me like unrelated entries end up together, making the table somewhat harder to navigate. Maybe you can have a look at the diff of the commit reorder table entries and see if you dis-/agree with me?

Your current ordering is fine with me 👍

[EgbertRijke]

Merged 🚀