remove unnecessary parameter from `Relation.Binary.Reasoning.Base.Apa…

…rtness` (#2438) Co-authored-by: MatthewDaggitt <matthewdaggitt@gmail.com>
agda · Aug 14, 2024 · b6cf220 · b6cf220
1 parent ab0038b
commit b6cf220
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 1 deletion.
diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -9,6 +9,9 @@ Highlights
 Bug-fixes
 ---------
 
+* Removed unnecessary parameter `#-trans : Transitive _#_` from
+  `Relation.Binary.Reasoning.Base.Apartness`.
+
 Non-backwards compatible changes
 --------------------------------
 

diff --git a/src/Relation/Binary/Reasoning/Base/Apartness.agda b/src/Relation/Binary/Reasoning/Base/Apartness.agda
@@ -20,7 +20,7 @@ open import Relation.Binary.Reasoning.Syntax
 module Relation.Binary.Reasoning.Base.Apartness {a ℓ₁ ℓ₂} {A : Set a}
   {_≈_ : Rel A ℓ₁} {_#_ : Rel A ℓ₂}
   (≈-equiv : IsEquivalence _≈_)
-  (#-trans : Transitive _#_) (#-sym   : Symmetric _#_)
+  (#-sym   : Symmetric _#_)
   (#-≈-trans : Trans _#_ _≈_ _#_) (≈-#-trans : Trans _≈_ _#_ _#_)
   where