From ebbac9b589935e3b787d10fa0396528041575bd6 Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Thu, 14 Sep 2023 13:11:37 +0100
Subject: [PATCH] solution to #1917

---
 src/Algebra/Bundles.agda    | 4 ++--
 src/Algebra/Structures.agda | 4 +++-
 2 files changed, 5 insertions(+), 3 deletions(-)

diff --git a/src/Algebra/Bundles.agda b/src/Algebra/Bundles.agda
index 5bc2d5a1d0..f10e3477a9 100644
--- a/src/Algebra/Bundles.agda
+++ b/src/Algebra/Bundles.agda
@@ -504,7 +504,7 @@ record SemiringWithoutOne c ℓ : Set (suc (c ⊔ ℓ)) where
 
   open NearSemiring nearSemiring public
     using
-    ( _≉_; +-rawMagma; +-magma; +-unitalMagma; +-semigroup
+    ( +-rawMagma; +-magma; +-unitalMagma; +-semigroup
     ; +-rawMonoid; +-monoid
     ; *-rawMagma; *-magma; *-semigroup
     ; rawNearSemiring
@@ -542,7 +542,7 @@ record CommutativeSemiringWithoutOne c ℓ : Set (suc (c ⊔ ℓ)) where
 
   open SemiringWithoutOne semiringWithoutOne public
     using
-    ( _≉_; +-rawMagma; +-magma; +-unitalMagma; +-semigroup; +-commutativeSemigroup
+    ( +-rawMagma; +-magma; +-unitalMagma; +-semigroup; +-commutativeSemigroup
     ; *-rawMagma; *-magma; *-semigroup
     ; +-rawMonoid; +-monoid; +-commutativeMonoid
     ; nearSemiring; rawNearSemiring
diff --git a/src/Algebra/Structures.agda b/src/Algebra/Structures.agda
index e38bbe7ba9..ed55226d67 100644
--- a/src/Algebra/Structures.agda
+++ b/src/Algebra/Structures.agda
@@ -358,7 +358,7 @@ record IsSemiringWithoutOne (+ * : Op₂ A) (0# : A) : Set (a ⊔ ℓ) where
     zero                  : Zero 0# *
 
   open IsCommutativeMonoid +-isCommutativeMonoid public
-    using (isEquivalence)
+    using (setoid)
     renaming
     ( comm                   to +-comm
     ; isMonoid               to +-isMonoid
@@ -366,6 +366,8 @@ record IsSemiringWithoutOne (+ * : Op₂ A) (0# : A) : Set (a ⊔ ℓ) where
     ; isCommutativeSemigroup to +-isCommutativeSemigroup
     )
 
+  open Setoid setoid public
+
   *-isMagma : IsMagma *
   *-isMagma = record
     { isEquivalence = isEquivalence