[ design ] Should `Reasoning.Binary.Setoid setoid` be part of the public API exported by `Algebra.Properties.X`?

[jamesmckinna]

... should this be part of the API exported by Algebra.Properties.X? Do we ever invoke algebraic properties not in a context where we have access to equational reasoning wrt that algebra?

Originally posted by @jamesmckinna in #2855 (comment)

If we do this, and with #2804 in mind, we could do this right at the bottom with Algebra.Properties.Magma, and then re-export it right up through the hierarchy...

[JacquesCarette]

Interesting question. When importing Algebra.Properties.X, what are you putting in the scope? Having both tools for reasoning (over an X) as well as a bunch of properties about X does make sense. And Algebra.Properties.X are already "fat" modules, so this further broadening of the API size does not bother me so much. [Although I'll probably want to re-compose some Algebra.Properties.X from smaller pieces in the future, once findability is under control.]

[jamesmckinna]

NB. I'm not clear whether or not adding the Reasoning infrastructure would in fact be a breaking change?

[JacquesCarette]

I'd say that normally it would not be, but if doing so causes a lot of ambiguous names downstream (because now things are imported twice), then it would be.