search

agda / agda-categories

A new Categories library for Agda
https://agda.github.io/agda-categories
MIT License
366 stars 68 forks source link

Unbundling limit-y things #419

Open 4e554c4c opened 4 months ago

4e554c4c commented 4 months ago

Something I've noticed, especially when dealing with limits, colimits and ends is that you occasionally want to state that a particular thing is the limit (/colimit/end) of a diagram, instead of merely stating that an end exists. This exists for the very specific limits Terminal and Initial (in the form of IsTerminal and IsInitial) but I think it would make sense for all limit-y things.

This is especially important when converting between different kinds of limit-y objects. E.g. limits -> ends, initial objects -> colimits, etc.

4e554c4c commented 4 months ago

For an example of why this might be important, see a recent commit of mine that proves that initial objects are strict initial in a cartesian closed category: https://github.com/4e554c4c/agda-categories/commit/319c9f47c25debfba939e5afa78004c02e8e558c#diff-0261bd0924a764ad5ad50b05434d00e33a2929173a1477af974fd091e90cd941R92

In particular this proof relies on the coapex of a colimit being (definitionally equal to) a particular thing, but cannot state this assumption.

JacquesCarette commented 4 months ago

Yes, absolutely. It so happens that it wasn't much needed up to now, but as we want to 'say more things', it very much becomes needed. So I'd welcome PRs that do this.