solution to agda#1917

Author: jamesmckinna

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

src/Algebra/Structures.agda

@@ -358,14 +358,16 @@ 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
     ; isCommutativeMagma     to +-isCommutativeMagma
     ; isCommutativeSemigroup to +-isCommutativeSemigroup
     )
 
+  open Setoid setoid public
+
   *-isMagma : IsMagma *
   *-isMagma = record
     { isEquivalence = isEquivalence