From e8c125ba0776602f64716526114842e1fea70cb7 Mon Sep 17 00:00:00 2001
From: Nathan van Doorn <nvd1234@gmail.com>
Date: Wed, 13 Nov 2024 10:30:04 +0100
Subject: [PATCH 1/2] 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
---
 src/Algebra/Structures.agda | 19 ++++++++++++++++---
 1 file changed, 16 insertions(+), 3 deletions(-)

diff --git a/src/Algebra/Structures.agda b/src/Algebra/Structures.agda
index b58245e6df..f534858c6d 100644
--- a/src/Algebra/Structures.agda
+++ b/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
 

From 4b100df5f690399888c83916ee31983dc2992262 Mon Sep 17 00:00:00 2001
From: Nathan van Doorn <nvd1234@gmail.com>
Date: Mon, 9 Dec 2024 09:39:05 +0100
Subject: [PATCH 2/2] Add changelog note

---
 CHANGELOG.md | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 98fe1576f9..6372350487 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -19,6 +19,13 @@ Bug-fixes
 Non-backwards compatible changes
 --------------------------------
 
+* 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
 ------------------