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

Adj_mode_theory Bitrot? #2

Open
Trebor-Huang opened this issue Mar 27, 2024 · 1 comment
Open

Adj_mode_theory Bitrot? #2

Trebor-Huang opened this issue Mar 27, 2024 · 1 comment

Comments

@Trebor-Huang
Copy link

There doesn't seem to be such a file, despite the claims in the comment of mode_theory.ml. I can sort of guess the implementation though. Is it deleted at some point or never written?

@jozefg
Copy link
Collaborator

jozefg commented Mar 30, 2024

Deleted I think. It refers to an earlier version of mitten which dealt with non-preordered mode theories where the adjoint mode theory was quite interesting. I think I have the code deciding the adjoint mode theory laying around somewhere if you're curious, but the rough idea is to capitalize on the equivalence between the walking adjunction and certain 2-categories of finite sets (see "The Free Adjunction" by Schanuel and Street)

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