From b6cf220932dcdbd0af417a4247540d2482cc4e12 Mon Sep 17 00:00:00 2001
From: SoonWon Moon <damhiya@gmail.com>
Date: Thu, 15 Aug 2024 06:02:57 +0900
Subject: [PATCH] remove unnecessary parameter from
 `Relation.Binary.Reasoning.Base.Apartness` (#2438)

Co-authored-by: MatthewDaggitt <matthewdaggitt@gmail.com>
---
 CHANGELOG.md                                      | 3 +++
 src/Relation/Binary/Reasoning/Base/Apartness.agda | 2 +-
 2 files changed, 4 insertions(+), 1 deletion(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index a0a916793c..8091cbfff9 100644
--- 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
index d3a850eca7..c2097dd80c 100644
--- 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