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

[ refactor ] deprecate Algebra.Structures.IsGroup.{uniqueˡ-⁻¹|uniqueʳ-⁻¹} with knock-ons for Algebra.Module.* #2571

Merged
merged 17 commits into from
Mar 31, 2025

Conversation

jamesmckinna
Copy link
Contributor

@jamesmckinna jamesmckinna commented Feb 3, 2025

This is a v2.3-compatible non-breaking fix for the Group uniqueness of inverses part of #2502 , avoiding the larger-scale v3.0 structural changes proposed there.

NB. the wrinkle is that an Bundles.AbelianGroup has to be created on the fly in order to exploit its Properties, but that can (perhaps!?) be eliminated as part of a downstream refactoring. UPDATED have now managed to eliminate this thanks to the prompt from @MatthewDaggitt below!

@jamesmckinna
Copy link
Contributor Author

Latest commit e12f942 updates the PR to propagate 'corresponding' changes to Algebra.Module.Structures and Algebra.Module.Properties.*, with suitable additional modules in the latter hierarchy, and 'corresponding' name choices for Module as for Group...
... accordingly, re-requesting a review from @MatthewDaggitt

@jamesmckinna jamesmckinna changed the title [ refactor ] deprecate Algebra.Structures.IsGroup.{uniqueˡ-⁻¹|uniqueʳ-⁻¹} [ refactor ] deprecate Algebra.Structures.IsGroup.{uniqueˡ-⁻¹|uniqueʳ-⁻¹} with knock-ons for Algebra.Module.* Mar 26, 2025
Copy link
Contributor

@MatthewDaggitt MatthewDaggitt left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Apart from my single comment, looks good!

@jamesmckinna jamesmckinna marked this pull request as draft March 27, 2025 10:54
@jamesmckinna jamesmckinna marked this pull request as ready for review March 27, 2025 11:14
@jamesmckinna
Copy link
Contributor Author

Phew, I think that's all fixed now.

@MatthewDaggitt MatthewDaggitt added this pull request to the merge queue Mar 31, 2025
Merged via the queue into agda:master with commit 3b9f62b Mar 31, 2025
2 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

4 participants