Unbundling limit-y things

[4e554c4c]

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]

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: 4e554c4c@319c9f4#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]

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.