Remove duplication in Ring-like structures

[Taneb]

Closes #1617

Currently various ring-like structures carry two different proofs that their underlying equivalence relation is an equivalence relation, because they're built out of a group for + and a monoid for * or similar. This changes the definitions so that they're only defined in terms of the + structure, with the * properties as extra laws. This makes their structure more linear and prevents the two isEquivalence proofs

[JacquesCarette]

This is one solution route.

Another is to notice that the current Setoid structure is internalized (in isMonoid etc). If we had a parallel isMonoid hierarchy that was parametrized over the carrier Setoid, then for something like NearSemiring, the + structure could be the one over the internalized Setoid, while the * structure over the parametrized version.

I've seen similar duplication of structures in the 1Lab, and it seemed to work nicely. I've done something like it in agda-categories to let me smoothly define "identity on objects" functors.

[MatthewDaggitt]

I have to confess I'm a tiny bit reluctant about this, as its a massive breaking change. It's not that I don't feel it's not an improvement, but I guess that @JacquesCarette's has got to me about having no good principled solution to the whole record mess.

Also you've missed out fixing:

• IsSemiringWithoutAnnihilatingZero
• IsSemiringWithoutOne
• IsNearSemiring

Having said that I don't really see an alternative solution. I see the appeal of your solution @JacquesCarette, but in my opinion I think we should probably avoid committing ourselves to maintaining a third parallel hierarchy of records. We have enough problems keeping 2 of them straight as it is.

[Taneb]

I have to confess I'm a tiny bit reluctant about this, as its a massive breaking change. It's not that I don't feel it's not an improvement, but I guess that @JacquesCarette's has got to me about having no good principled solution to the whole record mess.

When changing record fields needs to be done, I don't think Agda has a way of fixing things without there being big breaking changes. That said, there's a pretty easy migration path here, and the changes in stdlib were a lot less than I was expecting.

Also you've missed out fixing:

* `IsSemiringWithoutAnnihilatingZero`

* `IsSemiringWithoutOne`

* `IsNearSemiring`

Are you sure you're not just looking at the last commit?

Having said that I don't really see an alternative solution. I see the appeal of your solution @JacquesCarette, but in my opinion I think we should probably avoid committing ourselves to maintaining a third parallel hierarchy of records. We have enough problems keeping 2 of them straight as it is.

I'm pretty against adding a third record hierarchy here. It's a lot more effort and as far as I can tell doesn't have much benefit for either the definers of these structures, the implementors of specific rings, or people trying to use them.

There's a variation on what I've done that I flip-flopped between for a while, which is to build some of the structures out of smaller ring-like structures rather than group-like structures.

[JacquesCarette]

I actually agree that adding a full-fledged third record hierarchy has a very poor weight-to-benefit ratio. But I wanted to make sure to explore the design space more thoroughly.

Fundamentally I think a good solution will need non-trivial changes to Agda itself (along the lines of what Arend does). So not until stdlib 3.0, I'm afraid.

[MatthewDaggitt]

When changing record fields needs to be done, I don't think Agda has a way of fixing things without there being big breaking changes.

I'd second that. I guess it's a feature not a bug of theorem provers that implementation matters.

Are you sure you're not just looking at the last commit?

Ah yes, I am! Apologies.

There's a variation on what I've done that I flip-flopped between for a while, which is to build some of the structures out of smaller ring-like structures rather than group-like structures.

Okay, what we can do to ease the pain for people is to add old versions of the structures to Algebra.Structures.Biased, along with conversion functions, just like we did with the left and right versions. That way they only have to add in a function application, rather than fully rewrite their records.