Implementation of consequences and lemmas for Groups

[jmougeot]

As I have already started with Semigroups in PR #2688 and Monoids in PR #2692, the next step seems to be Groups.

I’m considering whether we should define specific left and right inverse properties within the Monoid structure and then generalize these in the Group structure.

[jamesmckinna]

Consider looking first at Quasigroup (without identity; so the the left- and right- operations are definable, but not necessarily 'inverse's) and then Loop (with; so then we do get "left and right inverse properties") although I'm not entirely sure how much more is provable for each of those than is already covered under their existing Properties modules ...

... But NB I have already once refactored Group to make use of Loop properties, and initially that's counterintuitive because the signature of Loop is 'richer' than that of Group (precisely because the axiomatisation is weaker!)... and we should be striving to build these successive layers of Properties in order of strength of axiomatisation...

... but don't forget Commutative as another important axis of variation in the axiomatisation...

...to go back to the thread, there is the general question of considering Solver-like normal forms within each structure, relative to the associated Free instance of the structure, some of which depend on decidability and/or commutativity of the underlying Carrier to be effective : (I'm hazy on how well this all works out in practice)

• List.NonEmpty for Semigroup / non-empty lists-with-natural number multiplicity (run-length encoding, in the decidable case)
• List for Monoid / run-length encoded lists
• Signed lists, for Group/ integer-run-length-encoding (free Z-module on the generators...)
• ...

Others with greater expertise might care to weigh in here...

[jamesmckinna]

@Taneb 's #2729 could indeed benefit from this, not least because Algebra.Properties.Group currently does not include Algebra.Properties.{Semigroup|Monoid} for the relevant sub-bundles...
... NB. possible clash/cognitive of names cancelʳ (from Monoid) and ∙-cancelʳ (from Group) etc.?

[JacquesCarette]

This is both a good direction to take, and feels like it is going to get derailed right away. Basically because Agda's features with respect to concrete Universal Algebra constructions are sub-optimal. You run into namespace management issues for theory presentations quite quickly down this path.