From ad622b238cee1029d81c0bd56f6f9c76b3baeb59 Mon Sep 17 00:00:00 2001
From: Lex van der Stoep <lex.vanderstoep@gmail.com>
Date: Sun, 16 Jun 2024 19:37:18 +0200
Subject: [PATCH 1/4] Fix #2396 by removing redundant zero in
 IsNonAssociativeRing

The zero field in the IsNonAssociativeRing was redundant, and could
be replaced with a proof based on the other properties.
---
 src/Algebra/Structures.agda | 16 +++++++++-------
 1 file changed, 9 insertions(+), 7 deletions(-)

diff --git a/src/Algebra/Structures.agda b/src/Algebra/Structures.agda
index 1aae80d1cc..4f74515f06 100644
--- a/src/Algebra/Structures.agda
+++ b/src/Algebra/Structures.agda
@@ -805,7 +805,6 @@ record IsNonAssociativeRing (+ * : Op₂ A) (-_ : Op₁ A) (0# 1# : A) : Set (a
     *-cong           : Congruent₂ *
     *-identity       : Identity 1# *
     distrib          : * DistributesOver +
-    zero             : Zero 0# *
 
   open IsAbelianGroup +-isAbelianGroup public
     renaming
@@ -833,18 +832,21 @@ record IsNonAssociativeRing (+ * : Op₂ A) (-_ : Op₁ A) (0# 1# : A) : Set (a
     ; isGroup                 to +-isGroup
     )
 
-  zeroˡ : LeftZero 0# *
-  zeroˡ = proj₁ zero
-
-  zeroʳ : RightZero 0# *
-  zeroʳ = proj₂ zero
-
   distribˡ : * DistributesOverˡ +
   distribˡ = proj₁ distrib
 
   distribʳ : * DistributesOverʳ +
   distribʳ = proj₂ distrib
 
+  zeroˡ : LeftZero 0# *
+  zeroˡ = Consequences.assoc∧distribʳ∧idʳ∧invʳ⇒zeˡ setoid +-cong *-cong +-assoc distribʳ +-identityʳ -‿inverseʳ
+
+  zeroʳ : RightZero 0# *
+  zeroʳ = Consequences.assoc∧distribˡ∧idʳ∧invʳ⇒zeʳ setoid +-cong *-cong +-assoc distribˡ +-identityʳ -‿inverseʳ
+
+  zero : Zero 0# *
+  zero = zeroˡ , zeroʳ
+
   *-isMagma : IsMagma *
   *-isMagma = record
     { isEquivalence = isEquivalence

From 07cae123b3c9d1eecb8669925da2950038a7b6b6 Mon Sep 17 00:00:00 2001
From: Lex van der Stoep <lex.vanderstoep@gmail.com>
Date: Sun, 16 Jun 2024 20:16:37 +0200
Subject: [PATCH 2/4] Remove zero arguments for IsNonAssociativeRing

Now that we've replaced the field `zero` with a definition, we
need to update the usages of `IsNonAssociativeRing`.
---
 src/Algebra/Construct/DirectProduct.agda | 2 --
 1 file changed, 2 deletions(-)

diff --git a/src/Algebra/Construct/DirectProduct.agda b/src/Algebra/Construct/DirectProduct.agda
index 3c0ec699ee..867de0c5fb 100644
--- a/src/Algebra/Construct/DirectProduct.agda
+++ b/src/Algebra/Construct/DirectProduct.agda
@@ -347,8 +347,6 @@ nonAssociativeRing R S = record
       ; *-identity       = UnitalMagma.identity (unitalMagma R.*-unitalMagma S.*-unitalMagma)
       ; distrib          = (λ x y z → (R.distribˡ , S.distribˡ) <*> x <*> y <*> z)
                             , (λ x y z → (R.distribʳ , S.distribʳ) <*> x <*> y <*> z)
-      ; zero             = uncurry (λ x y → R.zeroˡ x , S.zeroˡ y)
-                            , uncurry (λ x y → R.zeroʳ x , S.zeroʳ y)
       }
 
   } where module R = NonAssociativeRing R; module S = NonAssociativeRing S

From 83d9df2ad772c00a1f1b91db6cbb8d1c19cd9be9 Mon Sep 17 00:00:00 2001
From: Lex van der Stoep <lex.vanderstoep@gmail.com>
Date: Sat, 21 Dec 2024 15:13:22 +0100
Subject: [PATCH 3/4] Update CHANGELOG

For the removal of the redundant `zero` parameter in `IsNonAssociativeRing`.
---
 CHANGELOG.md | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 3c1c689d57..d2c19150d5 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -15,6 +15,8 @@ Bug-fixes
   These operators are used for equational reasoning of heterogeneous equality
   `x ≅ y`, but previously the three operators in `≡-syntax` unnecessarily require
   `x` and `y` to have the same type, making them unusable in most situations.
+* Removed unnecessary parameter `zero : Zero 0# *` from 
+  `Algebra.Structures.IsNonAssociativeRing`.
 
 Non-backwards compatible changes
 --------------------------------

From 83859b3e6d2a469a3d3701371b5077e6d5bf9882 Mon Sep 17 00:00:00 2001
From: Lex van der Stoep <lex.vanderstoep@gmail.com>
Date: Sat, 21 Dec 2024 15:16:52 +0100
Subject: [PATCH 4/4] Fix whitespace

---
 CHANGELOG.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index d2c19150d5..ac6de1fb81 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -15,7 +15,7 @@ Bug-fixes
   These operators are used for equational reasoning of heterogeneous equality
   `x ≅ y`, but previously the three operators in `≡-syntax` unnecessarily require
   `x` and `y` to have the same type, making them unusable in most situations.
-* Removed unnecessary parameter `zero : Zero 0# *` from 
+* Removed unnecessary parameter `zero : Zero 0# *` from
   `Algebra.Structures.IsNonAssociativeRing`.
 
 Non-backwards compatible changes