fix: add correct fixities (#2584)

Author: jamesmckinna

CHANGELOG.md

@@ -13,6 +13,10 @@ Bug-fixes
   to `#-sym` in order to avoid overloaded projection.
   `irrefl` and `cotrans` are similarly renamed for the sake of consistency.
 
+* In `Algebra.Definitions.RawMagma` and `Relation.Binary.Construct.Interior.Symmetric`,
+  the record constructors `_,_` incorrectly had no declared fixity. They have been given
+  the fixity `infixr 4 _,_`, consistent with that of `Data.Product.Base`.
+
 Non-backwards compatible changes
 --------------------------------
 

src/Algebra/Definitions/RawMagma.agda

@@ -25,6 +25,7 @@ open RawMagma M renaming (Carrier to A)
 ------------------------------------------------------------------------
 -- Divisibility
 
+infixr 4 _,_
 infix 5 _∣ˡ_ _∤ˡ_ _∣ʳ_ _∤ʳ_ _∣_ _∤_ _∥_ _∦_
 
 -- Divisibility from the left.

src/Relation/Binary/Construct/Interior/Symmetric.agda

@@ -24,6 +24,8 @@ private
 ------------------------------------------------------------------------
 -- Definition
 
+infixr 4 _,_
+
 record SymInterior (R : Rel A ℓ) (x y : A) : Set ℓ where
   constructor _,_
   field