Mess around with IsSemiringWithoutOne reexports (#2499)

* Mess around with IsSemiringWithoutOne reexports

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

* Add changelog note

Author: Taneb

CHANGELOG.md

@@ -23,6 +23,13 @@ Non-backwards compatible changes
 
 * In `Data.List.Relation.Binary.Sublist.Propositional.Properties` the implicit module parameters `a` and `A` have been replaced with `variable`s. This should be a backwards compatible change for the overwhelming majority of uses, and would only be non-backwards compatible if you were explicitly supplying these implicit parameters for some reason when importing the module. Explicitly supplying the implicit parameters for functions exported from the module should not be affected.
 
+* The names exposed by the `IsSemiringWithoutOne` record have been altered to
+  better correspond to other algebraic structures. In particular:
+  * `Carrier` is no longer exposed.
+  * Several laws have been re-exposed from `IsCommutativeMonoid +` renaming
+    them to name the operation `+`.
+  * `distribˡ` and `distribʳ` are defined in the record.
+
 Minor improvements
 ------------------
 

src/Algebra/Structures.agda

@@ -415,15 +415,22 @@ record IsSemiringWithoutOne (+ * : Op₂ A) (0# : A) : Set (a ⊔ ℓ) where
     zero                  : Zero 0# *
 
   open IsCommutativeMonoid +-isCommutativeMonoid public
-    using (setoid)
+    using (setoid; isEquivalence)
     renaming
-    ( comm                   to +-comm
+    ( ∙-cong                 to +-cong
+    ; ∙-congˡ                to +-congˡ
+    ; ∙-congʳ                to +-congʳ
+    ; assoc                  to +-assoc
+    ; identity               to +-identity
+    ; identityˡ              to +-identityˡ
+    ; identityʳ              to +-identityʳ
+    ; comm                   to +-comm
     ; isMonoid               to +-isMonoid
     ; isCommutativeMagma     to +-isCommutativeMagma
     ; isCommutativeSemigroup to +-isCommutativeSemigroup
     )
 
-  open Setoid setoid public
+  open IsEquivalence isEquivalence public
 
   *-isMagma : IsMagma *
   *-isMagma = record
@@ -444,6 +451,12 @@ record IsSemiringWithoutOne (+ * : Op₂ A) (0# : A) : Set (a ⊔ ℓ) where
     ; ∙-congʳ to *-congʳ
     )
 
+  distribˡ : * DistributesOverˡ +
+  distribˡ = proj₁ distrib
+
+  distribʳ : * DistributesOverʳ +
+  distribʳ = proj₂ distrib
+
   zeroˡ : LeftZero 0# *
   zeroˡ = proj₁ zero