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

[DRY] More redundant zero fields in Algebra.Structures #2396

Open
jamesmckinna opened this issue May 27, 2024 · 4 comments
Open

[DRY] More redundant zero fields in Algebra.Structures #2396

jamesmckinna opened this issue May 27, 2024 · 4 comments

Comments

@jamesmckinna
Copy link
Contributor

jamesmckinna commented May 27, 2024

Cf. #2195 and #2253

  • IsNonAssociativeRing admits enough properties to make the zero field redundant by exactly the same argument as for IsRingWithoutOne (so the redundancy is a bug, and removing it would be breaking)
  • correspondingly, the argument for IsRingWithoutOne makes no use of *-assoc...

Possible remedy: introduce a further refinement in which a new IsNonAssociativeRingWithoutOne would the 'right' home for such an argument, with each of the above two structures inheriting from that...?

See for example this blob and prior refactoring via Quasiring... for a possible solution.

lexvanderstoep pushed a commit to lexvanderstoep/agda-stdlib that referenced this issue Jun 16, 2024
The zero field in the IsNonAssociativeRing was redundant, and could
be replaced with a proof based on the other properties.
lexvanderstoep added a commit to lexvanderstoep/agda-stdlib that referenced this issue Jun 16, 2024
The zero field in the IsNonAssociativeRing was redundant, and could
be replaced with a proof based on the other properties.
lexvanderstoep added a commit to lexvanderstoep/agda-stdlib that referenced this issue Jun 16, 2024
The zero field in the IsNonAssociativeRing was redundant, and could
be replaced with a proof based on the other properties.
@jamesmckinna
Copy link
Contributor Author

@lexvanderstoep Are you planning a PR at any point in this direction?

@lexvanderstoep
Copy link
Contributor

Yes @jamesmckinna, there’s #2410 which was shelved at the time due to it being a breaking change.

What do you think? Is it a better time now?

@jamesmckinna
Copy link
Contributor Author

@lexvanderstoep apologies! I'd completely forgotten (and had draft:false turned on while looking back over open PRs... d'oh!).
We'll be discussing a new release, and the development path after that, in early January, so let's review this then. In the meantime, can you see whether your PR builds against the current version of master? Thanks!

lexvanderstoep added a commit to lexvanderstoep/agda-stdlib that referenced this issue Dec 18, 2024
The zero field in the IsNonAssociativeRing was redundant, and could
be replaced with a proof based on the other properties.
@lexvanderstoep
Copy link
Contributor

Done! Still works like a charm.

I'll leave the PR as a draft for now then. We can come back to it when we get around to the new release :)

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

No branches or pull requests

2 participants