[ refactor ] rectify binder names in Relation.Binary.Definitions

CHANGELOG.md

@@ -12,6 +12,8 @@ Bug-fixes
 Non-backwards compatible changes
 --------------------------------
 
+* [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
 ------------------
 

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')
 
 
 ------------------------------------------------------------------------

src/Algebra/Construct/Initial.agda

@@ -58,7 +58,7 @@ module ℤero where
   sym {x = ()}
 
   trans : Transitive _≈_
-  trans {i = ()}
+  trans {x = ()}
 
   ∙-cong : Congruent₂ _≈_ _∙_
   ∙-cong {x = ()}

src/Data/Container/Indexed/WithK.agda

@@ -53,7 +53,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

src/Data/Fin/Subset/Properties.agda

@@ -214,8 +214,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) λ()

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.
 

src/Data/List/Relation/Binary/Infix/Heterogeneous/Properties.agda

@@ -97,17 +97,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)
+  antisym asym {x = a ∷ as} {y = bs} p@(here _) (there q)
     = ⊥-elim $′ ℕ.<-irrefl refl $′ begin-strict
       length as <⟨ length-mono p ⟩
       length bs ≤⟨ length-mono q ⟩
       length as ∎ 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 _)
     = ⊥-elim $′ ℕ.<-irrefl refl $′ begin-strict
       length bs <⟨ length-mono q ⟩
       length as ≤⟨ length-mono p ⟩
       length bs ∎ 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)
     = ⊥-elim $′ ℕ.<-irrefl refl $′ begin-strict
       length as <⟨ length-mono p ⟩
       length bs <⟨ length-mono q ⟩

src/Data/Tree/AVL/Map/Membership/Propositional/Properties.agda

@@ -51,7 +51,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}

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
   }
 
 ------------------------------------------------------------------------

src/Relation/Binary/Consequences.agda

@@ -55,8 +55,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

src/Relation/Binary/Definitions.agda

@@ -54,7 +54,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
@@ -65,7 +65,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.
 
@@ -75,7 +75,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.