Names and definitions in the +-IsAbelianGroup instance of IsRing

[jamesmckinna]

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

• Redundant zero in IsRing #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 #2195 (comment)

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. Add derived (pre-)groupoid operations to Relation.Binary.Is(Partial)Equivalence #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 ...