Make use of the opposite category to automatically generate code for opposite derivations

[mohamed-barakat]

As discussed with Fabian it would be desirable to write half of the derivations and automatically generate the opposite versions using CompilerForCAP and the current infrastructure.

Background: I have written code to derive finite limits from products and binary equalizers and I would like to generate the code for colimits automatically. The current code for finite colimits calls the category constructor Opposite inside the derivations which is a hack.

[zickgraf]

As far as I can tell, nothing significant is blocking this, see https://github.com/zickgraf/CAP_project/tree/opposite_derivations for a demo. One has to:

1. Make Opposite applicable twice (see the commented line on the above branch, something similar has to be done for objects and morphisms and put behind a switch).
2. Write a wrapper CategoryAsOppositeOfOppositeOfCategory.
3. For each derivation: Create a dummy category with the opposite requirements, apply CategoryAsOppositeOfOppositeOfCategory, compile the opposite operation.
4. Write the result as a derivation for the opposite operation to a file.

[zickgraf]

This would also fix #917.

[zickgraf]

For CAP this is done in #1468. The system could easily be extended to more cases (e.g. include derivations including multiple categories), final derivations, and other packages.

[mohamed-barakat]

Excellent.