Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

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

Open
mohamed-barakat opened this issue Sep 30, 2022 · 4 comments

Comments

@mohamed-barakat
Copy link
Member

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.

@mohamed-barakat mohamed-barakat added the help wanted tasks suited for external help label Sep 30, 2022
@zickgraf
Copy link
Member

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
Copy link
Member

This would also fix #917.

@zickgraf
Copy link
Member

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
Copy link
Member Author

Excellent.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants