Names and definitions in the `+-IsAbelianGroup` instance of `IsRing`

[jamesmckinna]

Hi Three ~~Two~~ issues arising around (Is)Ring (and friends):

• #2195 do we really want the names

    ; inverse                 to -‿inverse
    ; inverseˡ                to -‿inverseˡ
    ; inverseʳ                to -‿inverseʳ

in the +-IsAbelianGroup instance of IsRing. Why not more simply +-inverse etc.?

Originally posted by @jamesmckinna in https://github.com/agda/agda-stdlib/issues/2195#issuecomment-1825142036

UPDATED: so far, the use of these things is almost completely confined to 'internal' definitions in Algebra.{Module.}Structures and Algebra.{Module.}Construct, so I'll leave well alone for now...

• should we enrich the manifest signature of IsAbelianGroup with an explicit subtraction operator? UPDATED: this already happens in IsGroup, though I might have expected the Group operation to admit two forms, and only collapse to 'subtraction' in the IsAbelianGroup case... (?):

infixl 6 _-_
_-_ : Op₂ A
x - y = x ∙ (y ⁻¹)

UPDATED though if I were to, I'd define, in IsGroup see #2251 (and UPDATED to reflect the discussion there):

infixl 6 _//_
infixr 6 _\\_
_//_ : Op₂ A
x // y = x ∙ (y ⁻¹)
_\\_ : Op₂ A
x \\  y = (x ⁻¹) ∙ y

and rename the first into _-_ in IsAbelianGroup and prove the two operations extensionally equal in Algebra.Properties.AbelianGroup (or somewhere else?)). Not sure about the infix/associativity declarations, though! Tempting instead, perhaps though, to define the Mal'cev operation and specialise it appropriately...

• this is a separate issue; which might also take in the trans (sym ...) ... analogous operation (not defined anywhere, AFAIK?) for the IsEquivalence (Is)Groupoid operations (with (Is)Groupoid not defined anywhere, either AFAIK?) cf. #2249

[JacquesCarette]

I agree that -‿inverse feels like overkill and that +-inverse would be more appropriate.

I also agree that doing the obvious conservative extension of defining subtraction is worthwhile. People can always choose to redefine and/or hide it if they have a more efficient version for their own instance.

[jamesmckinna]

Question (perhaps for the agda-categoriesmaintainer(s)): what is / would be the relationship between IsEquivalence and a hypothetical definition of IsGroupoid in stdlib?

[JacquesCarette]

The relationship is non-trivial because IsGroupoid is mostly about sym since the 'rest' is in Category already. And there's the issue that IsEquivalence does not talk about equivalences-of-equivalences but E-Groupoids do. So IsEquivalence is a non-trivial truncation of Groupoid.

Whether this means that StrictGroupoid is the better thing to look at (I doubt it) or 0-Groupoids (most likely) is probably the right question to ask.

[jamesmckinna]

OK, thanks for the steer towards a more refined analysis/understanding. I'm not about to propose adding *Groupoid to stdlib right now (I though that the agda-categories gang might do that... ;-)), but good to see how the more 'humble' (because truncated) IsEquivalence/Setoid fits into a bigger picture...

[jamesmckinna]

Of the three points raised here, happy to close this with a successful merge of #2251 ...