[ refactor ] `Algebra.Properties.Monoid`

[jamesmckinna]

Hmmm... possible (downstream?) refactoring opportunity for Algebra.Properties.Monoid to replace

ε-comm : ∀ a → a ∙ ε ≈ ε ∙ a
ε-comm a = trans (identityʳ a) (sym (identityˡ a))

with

ε-central : Central _∙_ ε
ε-central = Consequences.identity⇒central identity

instead?

Originally posted by @jamesmckinna in #2873 (comment)

[jamesmckinna]

UPDATED Moved from #2883 , and re-opening to consider also:

• Opportunity also here to reconsider the cancel names? eg. to 'implicational' form inverse⇒cancelʳ etc. cf. [Add] Consequences of identity for monoids #2692 and Algebra property reexports #2851 where the current choice of names breaks new code, and [ add ] Algebra.Construct.Centre.X of an algebra X, following #2863 #2885 for specimen usage.
• Also: reconsider the implicit/explicit parametrisation wrt _∙_ in [ add ] Algebra.Definitions.Central plus Consequences for Identity and Zero #2873 ?