[ refactor ] deprecate Algebra.Structures.IsGroup.{uniqueˡ-⁻¹|uniqueʳ-⁻¹}
#2571
Conversation
| ) | ||
|
|
||
| open AbelianGroupProperties record { isAbelianGroup = +ᴹ-isAbelianGroup } public | ||
| using () renaming (inverseˡ-unique to uniqueˡ‿-ᴹ; inverseʳ-unique to uniqueʳ‿-ᴹ) |
There was a problem hiding this comment.
If uniqueˡ-⁻¹ didn't belong in Algebra.Structures, then morally these shouldn't belong in Algebra.Module.Structures? If the Properties file already exists then they could be transferred there? Otherwise we could leave a comment?
There was a problem hiding this comment.
Thanks! I think this represents a wobble/failure of nerve on my part, while not trying to solve the problem of violating the meta-level principle 'Structures shouldn't depend on Bundles'.
But in a certain sense that is already a bigger problem: that Algebra.Properties.X shouldn't be parameterised on a Bundle x : X, but rather on the underlying Structure isX : IsX which supplies the 'axiomatisation' of Xs...
There was a problem hiding this comment.
But on that basis, I'd be happy to put this back in DRAFT, or even to close this PR, against a wider rethink of these issues...
There was a problem hiding this comment.
No, no I think that this is an improvement over what we currently have.
This is a v2.3-compatible non-
breakingfix for theGroupuniqueness of inverses part of #2502 , avoiding the larger-scale v3.0 structural changes proposed there.NB. the wrinkle is that an
Bundles.AbelianGrouphas to be created on the fly in order to exploit itsProperties, but that can (perhaps!?) be eliminated as part of a downstream refactoring.