Mess around with IsSemiringWithoutOne reexports

[Taneb]

It was missing several and had some duplicated, which was causing problems when trying to use those names

I don't know how to changelog this

[MatthewDaggitt]

I don't know how to changelog this

I would document this as a bug fix. Noting the removal of the Carrier export and then listing the new exports.

[jamesmckinna]

As the author of the prior, now offending, commit, I drew attention in the discussion comments on the relevant PR to the possibility of having introduced such a bug...

... having said that, the setoid export was for a reason, and I think that the revisions here revert the relevant consequence (namely to export negated equality...), so I think I'd prefer it if instead

• either Carrier is part of an explicit hiding directive when exporting setoid (open world assumption)
• or, that the exports are specifically restricted via a using directive (closed world assumption, which I think @JacquesCarette favours?)

There's a meta-issue here:

• the offending commit passed an approving review by the author of the present PR
• the originating history of the offending commit does not seem to have been referred back to for context/rationale/explanation

This is not to throw shade either on me (for a buggy commit), or @Taneb for the fix here, but to point out that, wittingly or unwittingly, reverting prior commits may have further subsequent negative downstream consequences.

Happy to be corrected if I've misconstrued the situation here!

[jamesmckinna]

Allow me to correct myself, after yesterday's splurge/rant, for which I apologise. I did some more digging through the history, and the various import/export dependencies...

Summary:

• indeed, I think the setoid export is a mistake, both on its face, but also because it is an example of a Structure exporting a sub-Bundle, which as @Taneb points out, happens nowhere else in the library (so is definitely a bug! sorry for introducing it...)
• the relevant exports of _≉_ are already handled in Algebra.Bundles via their Raw sub-bundles, so my objections above don't stand up, either.

Hope this helps! Apologies for interruptions in the smooth running of things...

[jamesmckinna]

Suggest removing the export of setoid completely... but not (yet) sure what the knock-on consequences of that might be...

Ugh. Worse that I thought: the uniqueness properties of inverse, defined as manifest fields, in Algebra.Structures.IsGroup, rely on Algebra.Consequences.Setoid, which depends, as the name suggests, on having a Bundled Setoid, rather than the underlying IsEquivalence for access to the properties of equality. So following my suggestion (to have IsMagma not export a setoid field) would actually have a larger scale knock-on effect.

Nevertheless, I think deleting the setoid export from IsSemiringWithoutOne should be harmless?

[MatthewDaggitt]

Gah these algebra imports, re-exports are always nightmarish. I'm not across the exact details, but my understanding aligns with both @jamesmckinna and @Taneb in that we try to avoid structures exporting bundles.