Derive limit instead of colimit operations

[mohamed-barakat]

I suggest deriving the limit from the colimit operations rather than vice versa. At some point, we can derive most colimit operations from the towers and have less code to verify in Coq. Currently, our towers for the colimits are shorter than those for limits, where the latter are the ones that need several opposite-category constructors.

[zickgraf]

The reason why I chose to generate the colimit operations from the limit operations in #1468 was that limits seem to usually come first in CAP, so I expected their derivations to have less bugs. Additionally, the names for limits are usually shorter and easier to distinguish. For example, in a derivation involving Cokernel and Coequalizer one has to be really careful to not mix up the two when quickly reading the derivation, while Kernel and Equalizer are shorter and easy to distinguish.

But of course this does not contradict your point. Mathematics simply seems to have chosen the wrong "default".