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

Remove Algebra.Definitions.Core(1/2) #1970

Closed
MatthewDaggitt opened this issue May 15, 2023 · 2 comments
Closed

Remove Algebra.Definitions.Core(1/2) #1970

MatthewDaggitt opened this issue May 15, 2023 · 2 comments
Labels
breaking bug library-design status: duplicate The main contents of the issue or PR already exists in another issue or PR.
Milestone

Comments

@MatthewDaggitt
Copy link
Contributor

The module parameter setup just doesn't work. When you write

open import Function.Definitions

you still get e.g. Surjective in scope with two equality parameters instead of one.

I think the best plan is to ditch the module parameters in Function.Definitions entirely, and fold Core1 and Core2 into it.

@jamesmckinna
Copy link
Contributor

How is this affected by @alexarice 's PR #1156 for a 'better' notion of Surjective, which IIUC, does use the two equality relations?

@MatthewDaggitt
Copy link
Contributor Author

Ack, you're right. That would also fix it. Okay, lets merge that instead!

@MatthewDaggitt MatthewDaggitt added the status: duplicate The main contents of the issue or PR already exists in another issue or PR. label May 16, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
breaking bug library-design status: duplicate The main contents of the issue or PR already exists in another issue or PR.
Projects
None yet
Development

No branches or pull requests

2 participants