Tidy up Algebra.Definitions.RawMagma (again), plus reconcile all the uses of _,_ as a constructor

[jamesmckinna]

Variations on the theme of uncoupling from Data.Product.Base, lifted out from #2579 : cf. #207

• bug: we don't give fixities to the various uses of _,_ as a constructor which since Fix #2216 by making divisibility definitions records #2217 supersede the prior use of Data.Product.Base._,_, so it's possible to get some odd parsing errors
• breaking mutual divisibility currently still defined as a Data.Product.Base._×_,, but since [ new ] symmetric core of a binary relation #2071 , it might be better to redefine it using Relation.Binary.Construct.Interior.Symmetric, and then be able to exploit the generic properties of such relations...
• bug: the constructor _,_ of Relation.Binary.Construct.Interior.Symmetric.SymInterior also doesn't have a fixity declaration either

Propose:

• give each use of _,_ as a constructor the same fixity declaration, namely infixr 4 _,_ that of Data.Product.Base._,_ [ fix ] Add correct fixities for constructor uses of _,_ #2584
• redefine _∥_ and refactor the proofs of its various properties as we go up the hierarchy to Algebra.Properties.Semiring.Divisibility (downstream PR)

It's possible that these should be two issue: the #207 bug fixes , and then the divisibility refactoring.

[JacquesCarette]

Note: I believe that Agda chokes badly if an operator (like _,_) has multiple fixities because of overloading. So we really really do have to give them the same fixity.

Also, I guess I didn't notice the constructor until now: why _,_ ? I think I would have preferred to pun (and that's not so great either).

I'm often a fan of doing things in small doses, especially when it comes to bug fixes and refactoring. [I've been convinced that adding new functionality is better done in "decently complete" steps.]

[jamesmckinna]

So _,_ was used in #2217 for the sake of backwards compatibility with the previous use(s) of Data.Product.Base.{∃|_×_) to represent divisibility... but not with an explicit fixity declaration. So this is a bug which needs fixing (in two places!)

But, you're right that the issue as it stands mixes up two strands of (interconnected) definitions, the connection being my desire to refactor one to use the other! (But also: they are all concerned with the conceptual modelling of divisibility)

[JacquesCarette]

The desire for progress collides with backwards compatibility, again. #2584 is the right thing to do given the current state. The better thing to do (for v3.0) would be to figure out decent names.

[jamesmckinna]

... The better thing to do (for v3.0) would be to figure out decent names.

I welcome suggestions, esp. in the context of candidate breaking approaches to #2115 ...