Fixed precedence of _≉_ and re-exported it via algebraic bundles (#1329)

Author: MatthewDaggitt

CHANGELOG.md

@@ -14,6 +14,9 @@ Bug-fixes
 * Fixed the type of the proof `map-id` in `List.Relation.Unary.All.Properties`, which was incorrectly abstracted over
   unused module parameters.
 
+* The binary relation `_≉_` exposed by records in `Relation.Binary.Bundles` now has
+  the correct infix precedence.
+
 Non-backwards compatible changes
 --------------------------------
 
@@ -53,6 +56,8 @@ Other major changes
 Other minor additions
 ---------------------
 
+* All bundles in `Algebra.Bundles` now re-export the binary relation `_≉_` from the underlying `Setoid`.
+
 * Added `Reflection.TypeChecking.Format.errorPartFmt`.
 
 * Added new properties to `Data.List.Properties`:

src/Algebra/Bundles.agda

@@ -44,6 +44,9 @@ record Magma c ℓ : Set (suc (c ⊔ ℓ)) where
   rawMagma : RawMagma _ _
   rawMagma = record { _≈_ = _≈_; _∙_ = _∙_ }
 
+  open Setoid setoid public
+    using (_≉_)
+
 
 record Semigroup c ℓ : Set (suc (c ⊔ ℓ)) where
   infixl 7 _∙_
@@ -59,7 +62,8 @@ record Semigroup c ℓ : Set (suc (c ⊔ ℓ)) where
   magma : Magma c ℓ
   magma = record { isMagma = isMagma }
 
-  open Magma magma public using (rawMagma)
+  open Magma magma public
+    using (_≉_; rawMagma)
 
 
 record Band c ℓ : Set (suc (c ⊔ ℓ)) where
@@ -76,7 +80,8 @@ record Band c ℓ : Set (suc (c ⊔ ℓ)) where
   semigroup : Semigroup c ℓ
   semigroup = record { isSemigroup = isSemigroup }
 
-  open Semigroup semigroup public using (magma; rawMagma)
+  open Semigroup semigroup public
+    using (_≉_; magma; rawMagma)
 
 
 record CommutativeSemigroup c ℓ : Set (suc (c ⊔ ℓ)) where
@@ -93,7 +98,8 @@ record CommutativeSemigroup c ℓ : Set (suc (c ⊔ ℓ)) where
   semigroup : Semigroup c ℓ
   semigroup = record { isSemigroup = isSemigroup }
 
-  open Semigroup semigroup public using (magma; rawMagma)
+  open Semigroup semigroup public
+    using (_≉_; magma; rawMagma)
 
 
 record Semilattice c ℓ : Set (suc (c ⊔ ℓ)) where
@@ -110,7 +116,8 @@ record Semilattice c ℓ : Set (suc (c ⊔ ℓ)) where
   band : Band c ℓ
   band = record { isBand = isBand }
 
-  open Band band public using (rawMagma; magma; semigroup)
+  open Band band public
+    using (_≉_; rawMagma; magma; semigroup)
 
 
 record SelectiveMagma c ℓ : Set (suc (c ⊔ ℓ)) where
@@ -127,7 +134,8 @@ record SelectiveMagma c ℓ : Set (suc (c ⊔ ℓ)) where
   magma : Magma c ℓ
   magma = record { isMagma = isMagma }
 
-  open Magma magma public using (rawMagma)
+  open Magma magma public
+    using (_≉_; rawMagma)
 
 ------------------------------------------------------------------------
 -- Bundles with 1 binary operation & 1 element
@@ -166,7 +174,8 @@ record Monoid c ℓ : Set (suc (c ⊔ ℓ)) where
   semigroup : Semigroup _ _
   semigroup = record { isSemigroup = isSemigroup }
 
-  open Semigroup semigroup public using (rawMagma; magma)
+  open Semigroup semigroup public
+    using (_≉_; rawMagma; magma)
 
   rawMonoid : RawMonoid _ _
   rawMonoid = record { _≈_ = _≈_; _∙_ = _∙_; ε = ε}
@@ -187,7 +196,8 @@ record CommutativeMonoid c ℓ : Set (suc (c ⊔ ℓ)) where
   monoid : Monoid _ _
   monoid = record { isMonoid = isMonoid }
 
-  open Monoid monoid public using (rawMagma; magma; semigroup; rawMonoid)
+  open Monoid monoid public
+    using (_≉_; rawMagma; magma; semigroup; rawMonoid)
 
   commutativeSemigroup : CommutativeSemigroup _ _
   commutativeSemigroup = record { isCommutativeSemigroup = isCommutativeSemigroup }
@@ -209,7 +219,7 @@ record IdempotentCommutativeMonoid c ℓ : Set (suc (c ⊔ ℓ)) where
   commutativeMonoid = record { isCommutativeMonoid = isCommutativeMonoid }
 
   open CommutativeMonoid commutativeMonoid public
-    using (rawMagma; magma; semigroup; rawMonoid; monoid)
+    using (_≉_; rawMagma; magma; semigroup; rawMonoid; monoid)
 
 
 -- Idempotent commutative monoids are also known as bounded lattices.
@@ -268,7 +278,8 @@ record Group c ℓ : Set (suc (c ⊔ ℓ)) where
   monoid : Monoid _ _
   monoid = record { isMonoid = isMonoid }
 
-  open Monoid monoid public using (rawMagma; magma; semigroup; rawMonoid)
+  open Monoid monoid public
+    using (_≉_; rawMagma; magma; semigroup; rawMonoid)
 
 record AbelianGroup c ℓ : Set (suc (c ⊔ ℓ)) where
   infix  8 _⁻¹
@@ -288,7 +299,7 @@ record AbelianGroup c ℓ : Set (suc (c ⊔ ℓ)) where
   group = record { isGroup = isGroup }
 
   open Group group public
-    using (rawMagma; magma; semigroup; monoid; rawMonoid; rawGroup)
+    using (_≉_; rawMagma; magma; semigroup; monoid; rawMonoid; rawGroup)
 
   commutativeMonoid : CommutativeMonoid _ _
   commutativeMonoid = record { isCommutativeMonoid = isCommutativeMonoid }
@@ -337,11 +348,15 @@ record Lattice c ℓ : Set (suc (c ⊔ ℓ)) where
     ; _∨_  = _∨_
     }
 
-  open RawLattice rawLattice using (∨-rawMagma; ∧-rawMagma)
+  open RawLattice rawLattice
+    using (∨-rawMagma; ∧-rawMagma)
 
   setoid : Setoid _ _
   setoid = record { isEquivalence = isEquivalence }
 
+  open Setoid setoid public
+    using (_≉_)
+
 
 record DistributiveLattice c ℓ : Set (suc (c ⊔ ℓ)) where
   infixr 7 _∧_
@@ -359,7 +374,8 @@ record DistributiveLattice c ℓ : Set (suc (c ⊔ ℓ)) where
   lattice : Lattice _ _
   lattice = record { isLattice = isLattice }
 
-  open Lattice lattice public using (rawLattice; setoid)
+  open Lattice lattice public
+    using (_≉_; rawLattice; setoid)
 
 
 ------------------------------------------------------------------------
@@ -419,7 +435,7 @@ record NearSemiring c ℓ : Set (suc (c ⊔ ℓ)) where
   +-monoid = record { isMonoid = +-isMonoid }
 
   open Monoid +-monoid public
-    using () renaming
+    using (_≉_) renaming
     ( rawMagma  to +-rawMagma
     ; magma     to +-magma
     ; semigroup to +-semigroup
@@ -455,7 +471,7 @@ record SemiringWithoutOne c ℓ : Set (suc (c ⊔ ℓ)) where
 
   open NearSemiring nearSemiring public
     using
-    ( +-rawMagma; +-magma; +-semigroup
+    ( _≉_; +-rawMagma; +-magma; +-semigroup
     ; +-rawMonoid; +-monoid
     ; *-rawMagma; *-magma; *-semigroup
     ; rawNearSemiring
@@ -490,7 +506,7 @@ record CommutativeSemiringWithoutOne c ℓ : Set (suc (c ⊔ ℓ)) where
 
   open SemiringWithoutOne semiringWithoutOne public
     using
-    ( +-rawMagma; +-magma; +-semigroup; +-commutativeSemigroup
+    ( _≉_; +-rawMagma; +-magma; +-semigroup; +-commutativeSemigroup
     ; *-rawMagma; *-magma; *-semigroup
     ; +-rawMonoid; +-monoid; +-commutativeMonoid
     ; nearSemiring; rawNearSemiring
@@ -565,7 +581,7 @@ record SemiringWithoutAnnihilatingZero c ℓ : Set (suc (c ⊔ ℓ)) where
     record { isCommutativeMonoid = +-isCommutativeMonoid }
 
   open CommutativeMonoid +-commutativeMonoid public
-    using () renaming
+    using (_≉_) renaming
     ( rawMagma             to +-rawMagma
     ; magma                to +-magma
     ; semigroup            to +-semigroup
@@ -610,7 +626,7 @@ record Semiring c ℓ : Set (suc (c ⊔ ℓ)) where
   open SemiringWithoutAnnihilatingZero
          semiringWithoutAnnihilatingZero public
     using
-    ( +-rawMagma;  +-magma;  +-semigroup; +-commutativeSemigroup
+    ( _≉_; +-rawMagma;  +-magma;  +-semigroup; +-commutativeSemigroup
     ; *-rawMagma;  *-magma;  *-semigroup
     ; +-rawMonoid; +-monoid; +-commutativeMonoid
     ; *-rawMonoid; *-monoid
@@ -645,7 +661,7 @@ record CommutativeSemiring c ℓ : Set (suc (c ⊔ ℓ)) where
 
   open Semiring semiring public
     using
-    ( +-rawMagma; +-magma; +-semigroup; +-commutativeSemigroup
+    ( _≉_; +-rawMagma; +-magma; +-semigroup; +-commutativeSemigroup
     ; *-rawMagma; *-magma; *-semigroup
     ; +-rawMonoid; +-monoid; +-commutativeMonoid
     ; *-rawMonoid; *-monoid
@@ -746,7 +762,7 @@ record Ring c ℓ : Set (suc (c ⊔ ℓ)) where
 
   open Semiring semiring public
     using
-    ( +-rawMagma; +-magma; +-semigroup; +-commutativeSemigroup
+    ( _≉_; +-rawMagma; +-magma; +-semigroup; +-commutativeSemigroup
     ; *-rawMagma; *-magma; *-semigroup
     ; +-rawMonoid; +-monoid ; +-commutativeMonoid
     ; *-rawMonoid; *-monoid
@@ -788,11 +804,12 @@ record CommutativeRing c ℓ : Set (suc (c ⊔ ℓ)) where
   ring : Ring _ _
   ring = record { isRing = isRing }
 
+  open Ring ring public using (_≉_; rawRing; +-group; +-abelianGroup)
+
   commutativeSemiring : CommutativeSemiring _ _
   commutativeSemiring =
     record { isCommutativeSemiring = isCommutativeSemiring }
 
-  open Ring ring public using (rawRing; +-group; +-abelianGroup)
   open CommutativeSemiring commutativeSemiring public
     using
     ( +-rawMagma; +-magma; +-semigroup; +-commutativeSemigroup
@@ -826,7 +843,7 @@ record BooleanAlgebra c ℓ : Set (suc (c ⊔ ℓ)) where
   distributiveLattice = record { isDistributiveLattice = isDistributiveLattice }
 
   open DistributiveLattice distributiveLattice public
-    using (setoid; lattice)
+    using (_≉_; setoid; lattice)
 
 
 ------------------------------------------------------------------------

src/Relation/Binary/Bundles.agda

@@ -28,6 +28,7 @@ record PartialSetoid a ℓ : Set (suc (a ⊔ ℓ)) where
 
   open IsPartialEquivalence isPartialEquivalence public
 
+  infix 4 _≉_
   _≉_ : Rel Carrier _
   x ≉ y = ¬ (x ≈ y)