[ design ] Re-exports from `Algebra.Properties.X`

[jamesmckinna]

Reading over #2695 and its antecedent PRs #2688 and #2692 , I have the feeling that we still haven't quite got the API right for Properties modules:

• it's not obvious that we do, but I think we should, reexport the axioms from the underlying isX : IsX ... substructure, otherwise we are left in the (slightly?) uneasy position of having to make multiple re-imports to get the 'widest possible' API (so perhaps the design question is more: "how wide should the API be?")
• we certainly don't consistently re-export Algebra.Properties.Y y for each sub-bundle y :Y which is re-exported publicly by bundle X, but again, I think that we should (which, if nothing else, would encourage us to improve consistency in naming such properties)

Group is the first really intricate version of the phenomenon, where some recent retrofitting #2251 manages to re-export the underlying Loop and Quasigroup properties, but we still don't re-export the Monoid (and hence Semigroup) properties for the underlying monoid object.

We should improve our documentation of what we (think that we should) do, and try to ensure that we do, indeed, do it!

[MatthewDaggitt]

I agree with both of those suggestions. The only question is whether this is a breaking change because if people have opened both IsX and Properties.X will they get clashes if Properties.X also exports IsX fields? I suspect we probably will...

[jamesmckinna]

Happy to badge this as v3.0, not least because that would give us longer to discuss/reflect.

I think my instincts in this context are to make the API as wide as possible cf. #2762 but perhaps there are possibilities to offer users 'narrow' and 'wide' versions (for Structures), and to refactor Properties in similar fashion?

But yes, I think you're right that trying to amalgamate Properties 'in one place' will end up being breaking...