From f08e67bf82baca7f5bc15ada6224b0592d79e7f8 Mon Sep 17 00:00:00 2001
From: Saransh Chopra <saransh0701@gmail.com>
Date: Thu, 15 Jun 2023 22:57:23 -0400
Subject: [PATCH] Fixities for `Relation` and `Algebra`

---
 CHANGELOG.md                                              | 7 +++++++
 src/Algebra/Solver/Ring.agda                              | 2 ++
 src/Relation/Binary/Bundles.agda                          | 1 +
 src/Relation/Binary/Construct/Add/Infimum/Strict.agda     | 2 ++
 src/Relation/Binary/Construct/Add/Point/Equality.agda     | 2 ++
 src/Relation/Binary/Construct/Add/Supremum/NonStrict.agda | 2 ++
 src/Relation/Binary/Construct/Closure/Transitive.agda     | 2 ++
 src/Relation/Binary/Construct/Intersection.agda           | 2 ++
 8 files changed, 20 insertions(+)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 25bc7bd058..c6f541483d 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -105,6 +105,13 @@ Bug-fixes
   infix   8 _⁻¹                                              (Data.Parity.Base)
   infixr  5 _`∷_                                             (Data.Vec.Reflection)
   infixr  5 _∷=_                                             (Data.Vec.Membership.Setoid)
+  infix   4 _≟H_ _≟N_                                        (Algebra.Solver.Ring)
+  infix   4 _≈_                                              (Relation.Binary.Bundles)
+  infixl  6 _∩_                                              (Relation.Binary.Construct.Intersection)
+  infix   4 _<₋_                                             (Relation.Binary.Construct.Add.Infimum.Strict)
+  infix   4 _≈∙_                                             (Relation.Binary.Construct.Add.Point.Equality)
+  infix   4 _≤⁺_ _≤⊤⁺                                        (Relation.Binary.Construct.Add.Supremum.NonStrict)
+  infixr  5 _∷ʳ_                                             (Relation.Binary.Construct.Closure.Transitive)
   ```
 
 * In `System.Exit`, the `ExitFailure` constructor is now carrying an integer
diff --git a/src/Algebra/Solver/Ring.agda b/src/Algebra/Solver/Ring.agda
index 669cbe8d25..a1ea98ead3 100644
--- a/src/Algebra/Solver/Ring.agda
+++ b/src/Algebra/Solver/Ring.agda
@@ -176,6 +176,8 @@ mutual
 
   -- Equality is weakly decidable.
 
+  infix 4 _≟H_ _≟N_
+
   _≟H_ : ∀ {n} → WeaklyDecidable (_≈H_ {n = n})
   ∅           ≟H ∅           = just ∅
   ∅           ≟H (_ *x+ _)   = nothing
diff --git a/src/Relation/Binary/Bundles.agda b/src/Relation/Binary/Bundles.agda
index 498e1f95ef..5a0621629f 100644
--- a/src/Relation/Binary/Bundles.agda
+++ b/src/Relation/Binary/Bundles.agda
@@ -21,6 +21,7 @@ open import Relation.Binary.Structures
 ------------------------------------------------------------------------
 
 record PartialSetoid a ℓ : Set (suc (a ⊔ ℓ)) where
+  infix 4 _≈_
   field
     Carrier              : Set a
     _≈_                  : Rel Carrier ℓ
diff --git a/src/Relation/Binary/Construct/Add/Infimum/Strict.agda b/src/Relation/Binary/Construct/Add/Infimum/Strict.agda
index 06ac74899b..45463af482 100644
--- a/src/Relation/Binary/Construct/Add/Infimum/Strict.agda
+++ b/src/Relation/Binary/Construct/Add/Infimum/Strict.agda
@@ -28,6 +28,8 @@ import Relation.Nullary.Decidable as Dec
 ------------------------------------------------------------------------
 -- Definition
 
+infix 4 _<₋_
+
 data _<₋_ : Rel (A ₋) (a ⊔ ℓ) where
   ⊥₋<[_] : (l : A)           → ⊥₋    <₋ [ l ]
   [_]    : {k l : A} → k < l → [ k ] <₋ [ l ]
diff --git a/src/Relation/Binary/Construct/Add/Point/Equality.agda b/src/Relation/Binary/Construct/Add/Point/Equality.agda
index 2968754a9f..a0b01a3d2b 100644
--- a/src/Relation/Binary/Construct/Add/Point/Equality.agda
+++ b/src/Relation/Binary/Construct/Add/Point/Equality.agda
@@ -24,6 +24,8 @@ import Relation.Nullary.Decidable as Dec
 ------------------------------------------------------------------------
 -- Definition
 
+infix 4 _≈∙_
+
 data _≈∙_ : Rel (Pointed A) (a ⊔ ℓ) where
   ∙≈∙ :                     ∙     ≈∙ ∙
   [_] : {k l : A} → k ≈ l → [ k ] ≈∙ [ l ]
diff --git a/src/Relation/Binary/Construct/Add/Supremum/NonStrict.agda b/src/Relation/Binary/Construct/Add/Supremum/NonStrict.agda
index 68346824a2..be30c7973c 100644
--- a/src/Relation/Binary/Construct/Add/Supremum/NonStrict.agda
+++ b/src/Relation/Binary/Construct/Add/Supremum/NonStrict.agda
@@ -26,6 +26,8 @@ import Relation.Binary.Construct.Add.Supremum.Equality as Equality
 ------------------------------------------------------------------------
 -- Definition
 
+infix 4 _≤⁺_ _≤⊤⁺
+
 data _≤⁺_ : Rel (A ⁺) (a ⊔ ℓ) where
   [_]  : {k l : A} → k ≤ l → [ k ] ≤⁺ [ l ]
   _≤⊤⁺ : (k : A ⁺)         → k     ≤⁺ ⊤⁺
diff --git a/src/Relation/Binary/Construct/Closure/Transitive.agda b/src/Relation/Binary/Construct/Closure/Transitive.agda
index 85ab19e3dc..1699dc0cb6 100644
--- a/src/Relation/Binary/Construct/Closure/Transitive.agda
+++ b/src/Relation/Binary/Construct/Closure/Transitive.agda
@@ -39,6 +39,8 @@ module _ {_∼_ : Rel A ℓ} where
   private
     _∼⁺_ = TransClosure _∼_
 
+  infixr 5 _∷ʳ_
+
   _∷ʳ_ : ∀ {x y z} → (x∼⁺y : x ∼⁺ y) (y∼z : y ∼ z) → x ∼⁺ z
   [ x∼y ]      ∷ʳ y∼z = x∼y ∷ [ y∼z ]
   (x∼y ∷ x∼⁺y) ∷ʳ y∼z = x∼y ∷ (x∼⁺y ∷ʳ y∼z)
diff --git a/src/Relation/Binary/Construct/Intersection.agda b/src/Relation/Binary/Construct/Intersection.agda
index f74dfb3de9..17845536ca 100644
--- a/src/Relation/Binary/Construct/Intersection.agda
+++ b/src/Relation/Binary/Construct/Intersection.agda
@@ -24,6 +24,8 @@ private
 ------------------------------------------------------------------------
 -- Definition
 
+infixl 6 _∩_
+
 _∩_ : REL A B ℓ₁ → REL A B ℓ₂ → REL A B (ℓ₁ ⊔ ℓ₂)
 L ∩ R = λ i j → L i j × R i j