Open mohamed-barakat opened 1 year ago
The reason why I chose to generate the colimit operations from the limit operations in https://github.com/homalg-project/CAP_project/pull/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".
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.