[Add] Consequences of identity for monoids

[jmougeot]

Introduce reasoning combinators for monoids.

This PR is intended to focus on the Monoid.Reasoning filr as the discussion regarding the Semigroup.reasonig file is in the PR : #2688

I went with the names from agda-categories since they seemed to make sense.

[jamesmckinna]

Probably the 'best' thing to do is to mark this as blocked (on #2688 ), otherwise you'll end up with merge conflicts when that PR gets merged, and indeed to start afresh with this PR being on a branch based on jmougeot/semigroup (or else: rebase this one against that branch). That keeps both the locality of each PR smaller, but also the (sequential) dependency between them.

[jamesmckinna]

Suggest corresponding title change for the PR in the spirit of that for #2688 ...

[MatthewDaggitt]

Given that this is not properly rebased, and the naming scheme is different from the semigroup PR and that I need to make a release candidate tomorrow, I'm going to remove this from the v2.3 milestone tomorrow @JacquesCarette. If you would like this to urgently get in then please bring it up to date.

[JacquesCarette]

I will try.

[JacquesCarette]

I think this is in excellent shape now.

[JacquesCarette]

@jmougeot pushed through the work (thanks!)

Yes, the naming scheme here is quite different. However, I claim that the names in this PR make sense. The ones for original semigroup PR didn't (i.e. the ones based on push and pull which are quite arbitrary). When you read a proof that uses the names here, you get a 'semantic sense' of what the proof does. They've also been used a lot in agda-categories and adopted in other libraries as well. And we've agreed that the current names in semigroup are an unsatisfying compromise, i..e the names are at best 'not wrong'.

I'm fine if this doesn't make it in to v2.3 -- but it shouldn't be because of the names!

[jamesmckinna]

I'm (qualified) happy with this, but would like us to revisit the names before v3.0, when we can break/deprecate to improve matters. My concern would be that we choose bad names, use them, extensively even, and then have more knock-on viscosity once we find the 'right' ones... but that is, here, I think outweighed by having them available for experiment, so their utility (and memorability!) can be experimented with...
... but as I'm on cell signal, I'll defer the heavy lifting and final approval to the release manager... ;-)

[jamesmckinna]

Happy to merge as is, but indeed I now find I prefer the superscript form, even if only for (internal) consistency of naming...

[jamesmckinna]

Although I've previously approved these, I'd like us to reconsider the Fairbairn penalty for having left/right intro/elim pairs with the one being the sym of the other , and likewise with insert/cancel...
... just as with #2688 not all uses of sym were eliminated (and another one, where the sym is disguised by flipping the arguments)

Suggestion: a follow-up PR to prune out the redundancies? (Ideally: before the v2.3 CHANGELOG is set in stone...)
But here: we need to commit to which we prefer, intro over elim (or vice versa), insert over cancel?
@JacquesCarette or would you argue the Fairbairn cost is worth paying?

[JacquesCarette]

In this particular case, I will definitely argue that that Fairbairn cost is worth paying, again largely because of readability. When you seem something being eliminated, it's nice to see the proof say that. When the proof says 'intro' but it reads as the opposite, it takes a while to see that for this one line, the reasoning is backwards.

I think that intro / elim and insert / cancel are the only times when I feel that way! So I'm not about to advocate for the multiplication of named symmetric combinators.

[Taneb]

Can we name these with ε rather than id?

[JacquesCarette]

Makes sense.

[Taneb]

Do we want to (can we please) reexport these for rings with suitable renamings?

[JacquesCarette]

Do we want to (can we please) reexport these for rings with suitable renamings?

I'd be happy to!

[JacquesCarette]

@Taneb I've done the renaming. I'll do the Ring part in a different PR, so as to not block this one.

[Taneb]

Changelog needs fleshing out but otherwise looks good!