diff --git a/CHANGELOG.md b/CHANGELOG.md
index 2959d3d6ce..7386461191 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -25,6 +25,8 @@ Non-backwards compatible changes
   significantly faster. However, its reduction behaviour on open terms may have
   changed.
 
+* [issue #2547](https://github.com/agda/agda-stdlib/issues/2547) The names of the *implicit* binders in the following definitions have been rectified to be consistent with those in the rest of `Relation.Binary.Definitions`: `Transitive`, `Antisym`, and `Antisymmetric`.
+
 Minor improvements
 ------------------
 
diff --git a/doc/README/Data/Container/Indexed/MultiSortedAlgebraExample.agda b/doc/README/Data/Container/Indexed/MultiSortedAlgebraExample.agda
index 0c466c932c..a8bad10f32 100644
--- a/doc/README/Data/Container/Indexed/MultiSortedAlgebraExample.agda
+++ b/doc/README/Data/Container/Indexed/MultiSortedAlgebraExample.agda
@@ -335,7 +335,7 @@ module _ (Sort : Set ℓˢ) (Ops : Container Sort Sort ℓᵒ ℓᵃ) where
                                             {x = t} {y = t'} (sound e)
     sound (trans  {t₁ = t₁} {t₂ = t₂}
                   {t₃ = t₃} e e')        =  isEquiv {M = M} .IsEquivalence.trans
-                                            {i = t₁} {j = t₂} {k = t₃} (sound e) (sound e')
+                                            {x = t₁} {y = t₂} {z = t₃} (sound e) (sound e')
 
 
 ------------------------------------------------------------------------
diff --git a/src/Algebra/Construct/Initial.agda b/src/Algebra/Construct/Initial.agda
index ce60096210..8a726b838a 100644
--- a/src/Algebra/Construct/Initial.agda
+++ b/src/Algebra/Construct/Initial.agda
@@ -58,7 +58,7 @@ module ℤero where
   sym {x = ()}
 
   trans : Transitive _≈_
-  trans {i = ()}
+  trans {x = ()}
 
   ∙-cong : Congruent₂ _≈_ _∙_
   ∙-cong {x = ()}
diff --git a/src/Data/Container/Indexed/WithK.agda b/src/Data/Container/Indexed/WithK.agda
index 3ec22ce240..d30e9a24c4 100644
--- a/src/Data/Container/Indexed/WithK.agda
+++ b/src/Data/Container/Indexed/WithK.agda
@@ -54,7 +54,7 @@ setoid C X = record
   ; isEquivalence = record
     { refl  = refl , refl , λ { r .r refl → X.refl }
     ; sym   = sym
-    ; trans = λ { {_} {i = xs} {ys} {zs} → trans {_} {i = xs} {ys} {zs}  }
+    ; trans = λ { {_} {x = xs} {ys} {zs} → trans {_} {x = xs} {ys} {zs}  }
     }
   }
   where
diff --git a/src/Data/Fin/Subset/Properties.agda b/src/Data/Fin/Subset/Properties.agda
index 1dd0847d30..64ecf1a605 100644
--- a/src/Data/Fin/Subset/Properties.agda
+++ b/src/Data/Fin/Subset/Properties.agda
@@ -218,8 +218,8 @@ x∉⁅y⁆⇒x≢y x∉⁅x⁆ refl = x∉⁅x⁆ (x∈⁅x⁆ _)
 ⊆-trans p⊆q q⊆r x∈p = q⊆r (p⊆q x∈p)
 
 ⊆-antisym : Antisymmetric {A = Subset n} _≡_ _⊆_
-⊆-antisym {i = []}     {[]}     p⊆q q⊆p = refl
-⊆-antisym {i = x ∷ xs} {y ∷ ys} p⊆q q⊆p with x | y
+⊆-antisym {x = []}     {[]}     p⊆q q⊆p = refl
+⊆-antisym {x = x ∷ xs} {y ∷ ys} p⊆q q⊆p with x | y
 ... | inside  | inside  = cong₂ _∷_ refl (⊆-antisym (drop-∷-⊆ p⊆q) (drop-∷-⊆ q⊆p))
 ... | inside  | outside = contradiction (p⊆q here) λ()
 ... | outside | inside  = contradiction (q⊆p here) λ()
diff --git a/src/Data/Fin/Substitution.agda b/src/Data/Fin/Substitution.agda
index 1d39b468e1..d0d197bf65 100644
--- a/src/Data/Fin/Substitution.agda
+++ b/src/Data/Fin/Substitution.agda
@@ -104,7 +104,7 @@ record Application (T₁ : Pred ℕ ℓ₁) (T₂ : Pred ℕ ℓ₂) : Set (ℓ
   -- Application of multiple substitutions.
 
   _/✶_ : T₁ m → Subs T₂ m n → T₁ n
-  _/✶_ = Star.gfold Fun.id _ (flip _/_) {k = zero}
+  _/✶_ = Star.gfold Fun.id _ (flip _/_) {z = zero}
 
 -- A combination of the two records above.
 
diff --git a/src/Data/List/Relation/Binary/Infix/Heterogeneous/Properties.agda b/src/Data/List/Relation/Binary/Infix/Heterogeneous/Properties.agda
index 6fd10257d3..90f8619140 100644
--- a/src/Data/List/Relation/Binary/Infix/Heterogeneous/Properties.agda
+++ b/src/Data/List/Relation/Binary/Infix/Heterogeneous/Properties.agda
@@ -99,17 +99,17 @@ module _ {c t} {C : Set c} {T : REL A C t} where
 
   antisym : Antisym R S T → Antisym (Infix R) (Infix S) (Pointwise T)
   antisym asym (here p) (here q) = Prefix.antisym asym p q
-  antisym asym {i = a ∷ as} {j = bs} p@(here _) (there q)
-    = contradiction (begin-strict
+  antisym asym {x = a ∷ as} {y = bs} p@(here _) (there q)
+   = contradiction (begin-strict
       length as <⟨ length-mono p ⟩
       length bs ≤⟨ length-mono q ⟩
       length as ∎) (ℕ.<-irrefl refl) where open ℕ.≤-Reasoning
-  antisym asym {i = as} {j = b ∷ bs} (there p) q@(here _)
+  antisym asym {x = as} {y = b ∷ bs} (there p) q@(here _)
     = contradiction (begin-strict
       length bs <⟨ length-mono q ⟩
       length as ≤⟨ length-mono p ⟩
       length bs ∎) (ℕ.<-irrefl refl) where open ℕ.≤-Reasoning
-  antisym asym {i = a ∷ as} {j = b ∷ bs} (there p) (there q)
+  antisym asym {x = a ∷ as} {y = b ∷ bs} (there p) (there q)
     = contradiction (begin-strict
       length as <⟨ length-mono p ⟩
       length bs <⟨ length-mono q ⟩
diff --git a/src/Data/Tree/AVL/Map/Membership/Propositional/Properties.agda b/src/Data/Tree/AVL/Map/Membership/Propositional/Properties.agda
index 5e472cfe2b..52dc763233 100644
--- a/src/Data/Tree/AVL/Map/Membership/Propositional/Properties.agda
+++ b/src/Data/Tree/AVL/Map/Membership/Propositional/Properties.agda
@@ -57,7 +57,7 @@ private
     kx : Key × V
 
 ≈ₖᵥ-trans : Transitive (_≈ₖᵥ_ {V = V})
-≈ₖᵥ-trans {i = i} {k = k} = ×-transitive Eq.trans ≡-trans {i = i} {k = k}
+≈ₖᵥ-trans {x = x} {z = z} = ×-transitive Eq.trans ≡-trans {x = x} {z = z}
 
 ≈ₖᵥ-sym : Symmetric (_≈ₖᵥ_ {V = V})
 ≈ₖᵥ-sym {x = x} {y = y} = ×-symmetric sym ≡-sym {x} {y}
diff --git a/src/Data/Vec/Functional/Relation/Binary/Permutation/Properties.agda b/src/Data/Vec/Functional/Relation/Binary/Permutation/Properties.agda
index 83d65ab5bb..22c54abb40 100644
--- a/src/Data/Vec/Functional/Relation/Binary/Permutation/Properties.agda
+++ b/src/Data/Vec/Functional/Relation/Binary/Permutation/Properties.agda
@@ -58,7 +58,7 @@ isIndexedEquivalence {A = A} = record
   { refl = ↭-refl
   ; sym = ↭-sym
   ; trans = λ {n₁ n₂ n₃} {xs : Vector A n₁} {ys : Vector A n₂} {zs : Vector A n₃}
-              xs↭ys ys↭zs → ↭-trans {i = n₁} {i = xs} xs↭ys ys↭zs
+              xs↭ys ys↭zs → ↭-trans {i = n₁} {x = xs} xs↭ys ys↭zs
   }
 
 ------------------------------------------------------------------------
diff --git a/src/Relation/Binary/Consequences.agda b/src/Relation/Binary/Consequences.agda
index 9add6af3a0..aef3e8351c 100644
--- a/src/Relation/Binary/Consequences.agda
+++ b/src/Relation/Binary/Consequences.agda
@@ -54,8 +54,7 @@ module _ {_∼_ : Rel A ℓ} where
   -- N.B. the implicit arguments to Cotransitive are permuted w.r.t.
   -- those of Transitive
   cotrans⇒¬-trans : Cotransitive _∼_ → Transitive (¬_ ∘₂ _∼_)
-  cotrans⇒¬-trans cotrans {j = z} x≁z z≁y x∼y =
-    [ x≁z , z≁y ]′ (cotrans x∼y z)
+  cotrans⇒¬-trans cotrans x≁z z≁y x∼y = [ x≁z , z≁y ]′ (cotrans x∼y _)
 
 ------------------------------------------------------------------------
 -- Proofs for Irreflexive relations
diff --git a/src/Relation/Binary/Definitions.agda b/src/Relation/Binary/Definitions.agda
index 55906c5b8d..b542da2a8c 100644
--- a/src/Relation/Binary/Definitions.agda
+++ b/src/Relation/Binary/Definitions.agda
@@ -53,7 +53,7 @@ Symmetric _∼_ = Sym _∼_ _∼_
 -- Generalised transitivity.
 
 Trans : REL A B ℓ₁ → REL B C ℓ₂ → REL A C ℓ₃ → Set _
-Trans P Q R = ∀ {i j k} → P i j → Q j k → R i k
+Trans P Q R = ∀ {x y z} → P x y → Q y z → R x z
 
 RightTrans : REL A B ℓ₁ → REL B B ℓ₂ → Set _
 RightTrans R S = Trans R S R
@@ -64,7 +64,7 @@ LeftTrans S R = Trans S R R
 -- A flipped variant of generalised transitivity.
 
 TransFlip : REL A B ℓ₁ → REL B C ℓ₂ → REL A C ℓ₃ → Set _
-TransFlip P Q R = ∀ {i j k} → Q j k → P i j → R i k
+TransFlip P Q R = ∀ {x y z} → Q y z → P x y → R x z
 
 -- Transitivity.
 
@@ -74,7 +74,7 @@ Transitive _∼_ = Trans _∼_ _∼_ _∼_
 -- Generalised antisymmetry
 
 Antisym : REL A B ℓ₁ → REL B A ℓ₂ → REL A B ℓ₃ → Set _
-Antisym R S E = ∀ {i j} → R i j → S j i → E i j
+Antisym R S E = ∀ {x y} → R x y → S y x → E x y
 
 -- Antisymmetry.