From 67adc1ddf7d7cd16a7a97a36981dae79af978d6d Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Mon, 9 Dec 2024 10:13:57 +0000
Subject: [PATCH] Fixes #2471

---
 CHANGELOG.md                                  |  4 ++-
 src/Data/Bool/Properties.agda                 |  2 +-
 src/Data/Char/Properties.agda                 |  4 +--
 src/Data/Fin/Properties.agda                  |  2 +-
 src/Data/List/Relation/Binary/Lex.agda        | 32 +++++++++----------
 src/Data/List/Relation/Binary/Pointwise.agda  |  4 +--
 .../Relation/Binary/Pointwise/Properties.agda |  2 +-
 src/Data/Nat/Properties.agda                  |  2 +-
 src/Data/Sum/Relation/Binary/Pointwise.agda   |  2 +-
 src/Relation/Binary/Consequences.agda         | 10 +++---
 .../Binary/Construct/Add/Supremum/Strict.agda |  4 +--
 .../Binary/Construct/Composition.agda         |  2 +-
 .../Binary/Construct/Intersection.agda        |  2 +-
 .../Binary/Construct/NaturalOrder/Left.agda   |  2 +-
 .../Binary/Construct/NaturalOrder/Right.agda  |  2 +-
 .../Binary/Construct/NonStrictToStrict.agda   |  4 +--
 src/Relation/Binary/Definitions.agda          |  6 ++--
 src/Relation/Binary/Properties/Setoid.agda    |  2 +-
 .../Binary/PropositionalEquality/Core.agda    |  2 +-
 .../Binary/Reasoning/Base/Triple.agda         |  4 +--
 src/Relation/Binary/Structures.agda           | 10 +++---
 src/Relation/Unary/Properties.agda            |  4 +--
 22 files changed, 55 insertions(+), 53 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 6cbf2b82aa..17538ebb5a 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -19,7 +19,9 @@ Bug-fixes
 Non-backwards compatible changes
 --------------------------------
 
-In `Function.Related.TypeIsomorphisms`, the unprimed versions are more level polymorphic; and the primed versions retain `Level` homogeneous types for the `Semiring` axioms to hold.
+* In `Function.Related.TypeIsomorphisms`, the unprimed versions are more level polymorphic; and the primed versions retain `Level` homogeneous types for the `Semiring` axioms to hold.
+
+* In `Relation.Binary.Definitions`, the left/right order of the components of `_Respects₂_` have been swapped [issue #2471](https://github.com/agda/agda-stdlib/issues/2471).
 
 Minor improvements
 ------------------
diff --git a/src/Data/Bool/Properties.agda b/src/Data/Bool/Properties.agda
index eb7ffb3869..98cb0234c0 100644
--- a/src/Data/Bool/Properties.agda
+++ b/src/Data/Bool/Properties.agda
@@ -186,7 +186,7 @@ false <? true  = yes f<t
 true  <? _     = no  (λ())
 
 <-resp₂-≡ : _<_ Respects₂ _≡_
-<-resp₂-≡ = subst (_ <_) , subst (_< _)
+<-resp₂-≡ = subst (_< _) , subst (_ <_)
 
 <-irrelevant : Irrelevant _<_
 <-irrelevant f<t f<t = refl
diff --git a/src/Data/Char/Properties.agda b/src/Data/Char/Properties.agda
index 36e6d37d3c..2cd00678fb 100644
--- a/src/Data/Char/Properties.agda
+++ b/src/Data/Char/Properties.agda
@@ -117,8 +117,8 @@ _<?_ = On.decidable toℕ ℕ._<_ ℕ._<?_
   { isEquivalence = ≡.isEquivalence
   ; irrefl        = <-irrefl
   ; trans         = λ {a} {b} {c} → <-trans {a} {b} {c}
-  ; <-resp-≈      = (λ {c} → ≡.subst (c <_))
-                  , (λ {c} → ≡.subst (_< c))
+  ; <-resp-≈      = (λ {c} → ≡.subst (_< c))
+                  , (λ {c} → ≡.subst (c <_))
   }
 
 <-isStrictTotalOrder : IsStrictTotalOrder _≡_ _<_
diff --git a/src/Data/Fin/Properties.agda b/src/Data/Fin/Properties.agda
index e1f2d25d24..7f2ced04c5 100644
--- a/src/Data/Fin/Properties.agda
+++ b/src/Data/Fin/Properties.agda
@@ -392,7 +392,7 @@ m <? n = suc (toℕ m) ℕ.≤? toℕ n
 <-respʳ-≡ refl x≤y = x≤y
 
 <-resp₂-≡ : (_<_ {n}) Respects₂ _≡_
-<-resp₂-≡ = <-respʳ-≡ , <-respˡ-≡
+<-resp₂-≡ = <-respˡ-≡ , <-respʳ-≡
 
 <-irrelevant : Irrelevant (_<_ {m} {n})
 <-irrelevant = ℕ.<-irrelevant
diff --git a/src/Data/List/Relation/Binary/Lex.agda b/src/Data/List/Relation/Binary/Lex.agda
index 6c8fb4b323..822a9426c8 100644
--- a/src/Data/List/Relation/Binary/Lex.agda
+++ b/src/Data/List/Relation/Binary/Lex.agda
@@ -68,7 +68,7 @@ module _ {a ℓ₁ ℓ₂} {A : Set a} {P : Set}
 
   transitive : IsEquivalence _≈_ → _≺_ Respects₂ _≈_ → Transitive _≺_ →
                Transitive _<_
-  transitive eq resp tr = trans
+  transitive eq resp@(respˡ , respʳ) tr = trans
     where
     trans : Transitive (Lex P _≈_ _≺_)
     trans (base p)         (base _)         = base p
@@ -76,28 +76,28 @@ module _ {a ℓ₁ ℓ₂} {A : Set a} {P : Set}
     trans halt             (this y≺z)       = halt
     trans halt             (next y≈z ys<zs) = halt
     trans (this x≺y)       (this y≺z)       = this (tr x≺y y≺z)
-    trans (this x≺y)       (next y≈z ys<zs) = this (proj₁ resp y≈z x≺y)
+    trans (this x≺y)       (next y≈z ys<zs) = this (respʳ y≈z x≺y)
     trans (next x≈y xs<ys) (this y≺z)       =
-      this (proj₂ resp (IsEquivalence.sym eq x≈y) y≺z)
+      this (respˡ (IsEquivalence.sym eq x≈y) y≺z)
     trans (next x≈y xs<ys) (next y≈z ys<zs) =
       next (IsEquivalence.trans eq x≈y y≈z) (trans xs<ys ys<zs)
 
   respects₂ : IsEquivalence _≈_ → _≺_ Respects₂ _≈_ → _<_ Respects₂ _≋_
-  respects₂ eq (resp₁ , resp₂) = resp¹ , resp²
+  respects₂ eq (respˡ , respʳ) = respₗ , respᵣ
     where
     open IsEquivalence eq using (sym; trans)
-    resp¹ : ∀ {xs} → Lex P _≈_ _≺_ xs Respects _≋_
-    resp¹ []            xs<[]            = xs<[]
-    resp¹ (_   ∷ _)     halt             = halt
-    resp¹ (x≈y ∷ _)     (this z≺x)       = this (resp₁ x≈y z≺x)
-    resp¹ (x≈y ∷ xs≋ys) (next z≈x zs<xs) =
-      next (trans z≈x x≈y) (resp¹ xs≋ys zs<xs)
-
-    resp² : ∀ {ys} → flip (Lex P _≈_ _≺_) ys Respects _≋_
-    resp² []            []<ys            = []<ys
-    resp² (x≈z ∷ _)     (this x≺y)       = this (resp₂ x≈z x≺y)
-    resp² (x≈z ∷ xs≋zs) (next x≈y xs<ys) =
-      next (trans (sym x≈z) x≈y) (resp² xs≋zs xs<ys)
+    respᵣ : ∀ {xs} → Lex P _≈_ _≺_ xs Respects _≋_
+    respᵣ []            xs<[]            = xs<[]
+    respᵣ (_   ∷ _)     halt             = halt
+    respᵣ (x≈y ∷ _)     (this z≺x)       = this (respʳ x≈y z≺x)
+    respᵣ (x≈y ∷ xs≋ys) (next z≈x zs<xs) =
+      next (trans z≈x x≈y) (respᵣ xs≋ys zs<xs)
+
+    respₗ : ∀ {ys} → flip (Lex P _≈_ _≺_) ys Respects _≋_
+    respₗ []            []<ys            = []<ys
+    respₗ (x≈z ∷ _)     (this x≺y)       = this (respˡ x≈z x≺y)
+    respₗ (x≈z ∷ xs≋zs) (next x≈y xs<ys) =
+      next (trans (sym x≈z) x≈y) (respₗ xs≋zs xs<ys)
 
 
   []<[]-⇔ : P ⇔ [] < []
diff --git a/src/Data/List/Relation/Binary/Pointwise.agda b/src/Data/List/Relation/Binary/Pointwise.agda
index 56d261a646..ab3b879ea1 100644
--- a/src/Data/List/Relation/Binary/Pointwise.agda
+++ b/src/Data/List/Relation/Binary/Pointwise.agda
@@ -119,8 +119,8 @@ Any-resp-Pointwise resp (x∼y ∷ xs) (there pxs) =
 AllPairs-resp-Pointwise : R Respects₂ S →
                           (AllPairs R) Respects (Pointwise S)
 AllPairs-resp-Pointwise _                    []         []         = []
-AllPairs-resp-Pointwise resp@(respₗ , respᵣ) (x∼y ∷ xs) (px ∷ pxs) =
-  All-resp-Pointwise respₗ xs (All.map (respᵣ x∼y) px) ∷
+AllPairs-resp-Pointwise resp@(respˡ , respʳ) (x∼y ∷ xs) (px ∷ pxs) =
+  All-resp-Pointwise respʳ xs (All.map (respˡ x∼y) px) ∷
   (AllPairs-resp-Pointwise resp xs pxs)
 
 ------------------------------------------------------------------------
diff --git a/src/Data/List/Relation/Binary/Pointwise/Properties.agda b/src/Data/List/Relation/Binary/Pointwise/Properties.agda
index 1761dd3cda..92e87a9226 100644
--- a/src/Data/List/Relation/Binary/Pointwise/Properties.agda
+++ b/src/Data/List/Relation/Binary/Pointwise/Properties.agda
@@ -62,7 +62,7 @@ respˡ resp []            []            = []
 respˡ resp (x≈y ∷ xs≈ys) (x∼z ∷ xs∼zs) = resp x≈y x∼z ∷ respˡ resp xs≈ys xs∼zs
 
 respects₂ : R Respects₂ S → (Pointwise R) Respects₂ (Pointwise S)
-respects₂ (rʳ , rˡ) = respʳ rʳ , respˡ rˡ
+respects₂ (rˡ , rʳ) = respˡ rˡ , respʳ rʳ
 
 decidable : Decidable R → Decidable (Pointwise R)
 decidable _  []       []       = yes []
diff --git a/src/Data/Nat/Properties.agda b/src/Data/Nat/Properties.agda
index 68efe6bcdf..fbf6a1aacd 100644
--- a/src/Data/Nat/Properties.agda
+++ b/src/Data/Nat/Properties.agda
@@ -404,7 +404,7 @@ _>?_ = flip _<?_
 <-irrelevant = ≤-irrelevant
 
 <-resp₂-≡ : _<_ Respects₂ _≡_
-<-resp₂-≡ = subst (_ <_) , subst (_< _)
+<-resp₂-≡ = subst (_< _) , subst (_ <_)
 
 ------------------------------------------------------------------------
 -- Bundles
diff --git a/src/Data/Sum/Relation/Binary/Pointwise.agda b/src/Data/Sum/Relation/Binary/Pointwise.agda
index 6d6c84a253..1a7f9021f8 100644
--- a/src/Data/Sum/Relation/Binary/Pointwise.agda
+++ b/src/Data/Sum/Relation/Binary/Pointwise.agda
@@ -111,7 +111,7 @@ drop-inj₂ (inj₂ x) = x
 
 ⊎-respects₂ : R Respects₂ ≈₁ → S Respects₂ ≈₂ →
               (Pointwise R S) Respects₂ (Pointwise ≈₁ ≈₂)
-⊎-respects₂ (r₁ , l₁) (r₂ , l₂) = ⊎-respectsʳ r₁ r₂ , ⊎-respectsˡ l₁ l₂
+⊎-respects₂ (l₁ , r₁) (l₂ , r₂) = ⊎-respectsˡ l₁ l₂ , ⊎-respectsʳ r₁ r₂
 
 ------------------------------------------------------------------------
 -- Structures
diff --git a/src/Relation/Binary/Consequences.agda b/src/Relation/Binary/Consequences.agda
index 3cdb4db356..dd6444db97 100644
--- a/src/Relation/Binary/Consequences.agda
+++ b/src/Relation/Binary/Consequences.agda
@@ -37,7 +37,7 @@ module _ {_∼_ : Rel A ℓ} (R : Rel A p) where
   subst⇒respʳ subst {x} y′∼y Pxy′ = subst (R x) y′∼y Pxy′
 
   subst⇒resp₂ : Substitutive _∼_ p → R Respects₂ _∼_
-  subst⇒resp₂ subst = subst⇒respʳ subst , subst⇒respˡ subst
+  subst⇒resp₂ subst = subst⇒respˡ subst , subst⇒respʳ subst
 
 module _ {_∼_ : Rel A ℓ} {P : Pred A p} where
 
@@ -74,7 +74,7 @@ module _ {_≈_ : Rel A ℓ₁} {_≤_ : Rel A ℓ₂} where
 
   total⇒refl : _≤_ Respects₂ _≈_ → Symmetric _≈_ →
                Total _≤_ → _≈_ ⇒ _≤_
-  total⇒refl (respʳ , respˡ) sym total {x} {y} x≈y with total x y
+  total⇒refl (respˡ , respʳ) sym total {x} {y} x≈y with total x y
   ... | inj₁ x∼y = x∼y
   ... | inj₂ y∼x = respʳ x≈y (respˡ (sym x≈y) y∼x)
 
@@ -125,7 +125,7 @@ module _ {_≈_ : Rel A ℓ₁} {_<_ : Rel A ℓ₂} where
 
   asym⇒irr : _<_ Respects₂ _≈_ → Symmetric _≈_ →
              Asymmetric _<_ → Irreflexive _≈_ _<_
-  asym⇒irr (respʳ , respˡ) sym asym {x} {y} x≈y x<y =
+  asym⇒irr (respˡ , respʳ) sym asym {x} {y} x≈y x<y =
     asym x<y (respʳ (sym x≈y) (respˡ x≈y x<y))
 
   tri⇒asym : Trichotomous _≈_ _<_ → Asymmetric _<_
@@ -172,8 +172,8 @@ module _ {_≈_ : Rel A ℓ₁} {_<_ : Rel A ℓ₂} where
                    Transitive _<_ → Trichotomous _≈_ _<_ →
                    _<_ Respects₂ _≈_
   trans∧tri⇒resp sym ≈-tr <-tr tri =
-    trans∧tri⇒respʳ sym ≈-tr <-tr tri ,
-    trans∧tri⇒respˡ ≈-tr <-tr tri
+    trans∧tri⇒respˡ ≈-tr <-tr tri ,
+    trans∧tri⇒respʳ sym ≈-tr <-tr tri
 
 ------------------------------------------------------------------------
 -- Without Loss of Generality
diff --git a/src/Relation/Binary/Construct/Add/Supremum/Strict.agda b/src/Relation/Binary/Construct/Add/Supremum/Strict.agda
index 5613be8112..1a92600c4f 100644
--- a/src/Relation/Binary/Construct/Add/Supremum/Strict.agda
+++ b/src/Relation/Binary/Construct/Add/Supremum/Strict.agda
@@ -97,7 +97,7 @@ module _ {r} {_≤_ : Rel A r} where
 <⁺-respʳ-≡ = subst (_ <⁺_)
 
 <⁺-resp-≡ : _<⁺_ Respects₂ _≡_
-<⁺-resp-≡ = <⁺-respʳ-≡ , <⁺-respˡ-≡
+<⁺-resp-≡ = <⁺-respˡ-≡ , <⁺-respʳ-≡
 
 ------------------------------------------------------------------------
 -- Relational properties + setoid equality
@@ -128,7 +128,7 @@ module _ {e} {_≈_ : Rel A e} where
   <⁺-respʳ-≈⁺ <-respʳ-≈ ⊤⁺≈⊤⁺ q     = q
 
   <⁺-resp-≈⁺ : _<_ Respects₂ _≈_ → _<⁺_ Respects₂ _≈⁺_
-  <⁺-resp-≈⁺ = map <⁺-respʳ-≈⁺ <⁺-respˡ-≈⁺
+  <⁺-resp-≈⁺ = map <⁺-respˡ-≈⁺ <⁺-respʳ-≈⁺
 
 ------------------------------------------------------------------------
 -- Structures + propositional equality
diff --git a/src/Relation/Binary/Construct/Composition.agda b/src/Relation/Binary/Construct/Composition.agda
index 35df23947d..87b88fcba1 100644
--- a/src/Relation/Binary/Construct/Composition.agda
+++ b/src/Relation/Binary/Construct/Composition.agda
@@ -57,7 +57,7 @@ module _ {≈ : Rel C ℓ} (L : REL A B ℓ₁) (R : REL B C ℓ₂) where
 module _ {≈ : Rel A ℓ} (L : REL A B ℓ₁) (R : REL B A ℓ₂) where
 
   respects₂ :  L Respectsˡ ≈ → R Respectsʳ ≈ → (L ; R) Respects₂ ≈
-  respects₂ Lˡ Rʳ = respectsʳ L R Rʳ , respectsˡ L R Lˡ
+  respects₂ Lˡ Rʳ = respectsˡ L R Lˡ , respectsʳ L R Rʳ
 
 module _ {≈ : REL A B ℓ} (L : REL A B ℓ₁) (R : Rel B ℓ₂) where
 
diff --git a/src/Relation/Binary/Construct/Intersection.agda b/src/Relation/Binary/Construct/Intersection.agda
index 0d26d675e6..b661d6dbb9 100644
--- a/src/Relation/Binary/Construct/Intersection.agda
+++ b/src/Relation/Binary/Construct/Intersection.agda
@@ -76,7 +76,7 @@ module _ (≈ : Rel A ℓ₁) (L : Rel A ℓ₂) (R : Rel A ℓ₃) where
   respectsʳ L-resp R-resp x≈y = map (L-resp x≈y) (R-resp x≈y)
 
   respects₂ : L Respects₂ ≈ → R Respects₂ ≈ → (L ∩ R) Respects₂ ≈
-  respects₂ (Lʳ , Lˡ) (Rʳ , Rˡ) = respectsʳ Lʳ Rʳ , respectsˡ Lˡ Rˡ
+  respects₂ (Lˡ , Lʳ) (Rˡ , Rʳ) = respectsˡ Lˡ Rˡ , respectsʳ Lʳ Rʳ
 
   antisymmetric : Antisymmetric ≈ L ⊎ Antisymmetric ≈ R → Antisymmetric ≈ (L ∩ R)
   antisymmetric (inj₁ L-antisym) (Lxy , _) (Lyx , _) = L-antisym Lxy Lyx
diff --git a/src/Relation/Binary/Construct/NaturalOrder/Left.agda b/src/Relation/Binary/Construct/NaturalOrder/Left.agda
index cd8864af6e..4969c9f856 100644
--- a/src/Relation/Binary/Construct/NaturalOrder/Left.agda
+++ b/src/Relation/Binary/Construct/NaturalOrder/Left.agda
@@ -85,7 +85,7 @@ respˡ magma {x} {y} {z} y≈z y≤x = begin
   where open module M = IsMagma magma; open ≈-Reasoning M.setoid
 
 resp₂ : IsMagma _∙_ →  _≤_ Respects₂ _≈_
-resp₂ magma = respʳ magma , respˡ magma
+resp₂ magma = respˡ magma , respʳ magma
 
 dec : Decidable _≈_ → Decidable _≤_
 dec _≟_ x y = x ≟ (x ∙ y)
diff --git a/src/Relation/Binary/Construct/NaturalOrder/Right.agda b/src/Relation/Binary/Construct/NaturalOrder/Right.agda
index 024b946cc8..4518050f3b 100644
--- a/src/Relation/Binary/Construct/NaturalOrder/Right.agda
+++ b/src/Relation/Binary/Construct/NaturalOrder/Right.agda
@@ -86,7 +86,7 @@ respˡ magma {x} {y} {z} y≈z y≤x = begin
   where open module M = IsMagma magma; open ≈-Reasoning M.setoid
 
 resp₂ : IsMagma _∙_ →  _≤_ Respects₂ _≈_
-resp₂ magma = respʳ magma , respˡ magma
+resp₂ magma = respˡ magma , respʳ magma
 
 dec : Decidable _≈_ → Decidable _≤_
 dec _≟_ x y = x ≟ (y ∙ x)
diff --git a/src/Relation/Binary/Construct/NonStrictToStrict.agda b/src/Relation/Binary/Construct/NonStrictToStrict.agda
index f0402d7fb9..1a91454f2f 100644
--- a/src/Relation/Binary/Construct/NonStrictToStrict.agda
+++ b/src/Relation/Binary/Construct/NonStrictToStrict.agda
@@ -99,8 +99,8 @@ x < y = x ≤ y × x ≉ y
   (respʳ y≈z x≤y) , λ x≈z → x≉y (trans x≈z (sym y≈z))
 
 <-resp-≈ : IsEquivalence _≈_ → _≤_ Respects₂ _≈_ → _<_ Respects₂ _≈_
-<-resp-≈ eq (respʳ , respˡ) =
-  <-respʳ-≈ sym trans respʳ , <-respˡ-≈ trans respˡ
+<-resp-≈ eq (respˡ , respʳ) =
+  <-respˡ-≈ trans respˡ , <-respʳ-≈ sym trans respʳ
   where open IsEquivalence eq
 
 <-trichotomous : Symmetric _≈_ → Decidable _≈_ →
diff --git a/src/Relation/Binary/Definitions.agda b/src/Relation/Binary/Definitions.agda
index 167b63a8cb..cb17b5508b 100644
--- a/src/Relation/Binary/Definitions.agda
+++ b/src/Relation/Binary/Definitions.agda
@@ -185,17 +185,17 @@ P Respects _∼_ = P ⟶ P Respects _∼_
 -- Right respecting - relatedness is preserved on the right by equality.
 
 _Respectsʳ_ : REL A B ℓ₁ → Rel B ℓ₂ → Set _
-_∼_ Respectsʳ _≈_ = ∀ {x} → (x ∼_) Respects _≈_
+R Respectsʳ _≈_ = ∀ {x} → (R x) Respects _≈_
 
 -- Left respecting - relatedness is preserved on the left by equality.
 
 _Respectsˡ_ : REL A B ℓ₁ → Rel A ℓ₂ → Set _
-P Respectsˡ _∼_ = ∀ {y} → (flip P y) Respects _∼_
+R Respectsˡ _∼_ = ∀ {y} → (flip R y) Respects _∼_
 
 -- Respecting - relatedness is preserved on both sides by equality
 
 _Respects₂_ : Rel A ℓ₁ → Rel A ℓ₂ → Set _
-P Respects₂ _∼_ = (P Respectsʳ _∼_) × (P Respectsˡ _∼_)
+R Respects₂ _∼_ = (R Respectsˡ _∼_) × (R Respectsʳ _∼_)
 
 -- Substitutivity - any two related elements satisfy exactly the same
 -- set of unary relations. Note that only the various derivatives
diff --git a/src/Relation/Binary/Properties/Setoid.agda b/src/Relation/Binary/Properties/Setoid.agda
index 43dc7e67d0..5e80b2586c 100644
--- a/src/Relation/Binary/Properties/Setoid.agda
+++ b/src/Relation/Binary/Properties/Setoid.agda
@@ -78,7 +78,7 @@ preorder = record
 ≉-respʳ y≈y′ x≉y x≈y′ = x≉y $ trans x≈y′ (sym y≈y′)
 
 ≉-resp₂ : _≉_ Respects₂ _≈_
-≉-resp₂ = ≉-respʳ , ≉-respˡ
+≉-resp₂ = ≉-respˡ , ≉-respʳ
 
 ≉-irrefl : Irreflexive _≈_ _≉_
 ≉-irrefl x≈y x≉y = contradiction x≈y x≉y
diff --git a/src/Relation/Binary/PropositionalEquality/Core.agda b/src/Relation/Binary/PropositionalEquality/Core.agda
index f52fed277f..0c951ad5d9 100644
--- a/src/Relation/Binary/PropositionalEquality/Core.agda
+++ b/src/Relation/Binary/PropositionalEquality/Core.agda
@@ -93,7 +93,7 @@ respʳ : ∀ (∼ : Rel A ℓ) → ∼ Respectsʳ _≡_
 respʳ _∼_ refl x∼y = x∼y
 
 resp₂ : ∀ (∼ : Rel A ℓ) → ∼ Respects₂ _≡_
-resp₂ _∼_ = respʳ _∼_ , respˡ _∼_
+resp₂ _∼_ = respˡ _∼_ , respʳ _∼_
 
 ------------------------------------------------------------------------
 -- Properties of _≢_
diff --git a/src/Relation/Binary/Reasoning/Base/Triple.agda b/src/Relation/Binary/Reasoning/Base/Triple.agda
index 3433e58063..f9d96731fb 100644
--- a/src/Relation/Binary/Reasoning/Base/Triple.agda
+++ b/src/Relation/Binary/Reasoning/Base/Triple.agda
@@ -55,7 +55,7 @@ start (strict x<y) = <⇒≤ x<y
 ≈-go : Trans _≈_ _IsRelatedTo_ _IsRelatedTo_
 ≈-go x≈y (equals y≈z) = equals (Eq.trans x≈y y≈z)
 ≈-go x≈y (nonstrict y≤z) = nonstrict (∼-respˡ-≈ (Eq.sym x≈y) y≤z)
-≈-go x≈y (strict y<z) = strict (proj₂ <-resp-≈ (Eq.sym x≈y) y<z)
+≈-go x≈y (strict y<z) = strict (proj₁ <-resp-≈ (Eq.sym x≈y) y<z)
 
 ≤-go : Trans _≤_ _IsRelatedTo_ _IsRelatedTo_
 ≤-go x≤y (equals y≈z) = nonstrict (∼-respʳ-≈ y≈z x≤y)
@@ -63,7 +63,7 @@ start (strict x<y) = <⇒≤ x<y
 ≤-go x≤y (strict y<z) = strict (≤-<-trans x≤y y<z)
 
 <-go : Trans _<_ _IsRelatedTo_ _IsRelatedTo_
-<-go x<y (equals y≈z) = strict (proj₁ <-resp-≈ y≈z x<y)
+<-go x<y (equals y≈z) = strict (proj₂ <-resp-≈ y≈z x<y)
 <-go x<y (nonstrict y≤z) = strict (<-≤-trans x<y y≤z)
 <-go x<y (strict y<z) = strict (<-trans x<y y<z)
 
diff --git a/src/Relation/Binary/Structures.agda b/src/Relation/Binary/Structures.agda
index 3bbfc6db27..7c6e43eb73 100644
--- a/src/Relation/Binary/Structures.agda
+++ b/src/Relation/Binary/Structures.agda
@@ -92,7 +92,7 @@ record IsPreorder (_≲_ : Rel A ℓ₂) : Set (a ⊔ ℓ ⊔ ℓ₂) where
   ≲-respʳ-≈ x≈y z∼x = trans z∼x (reflexive x≈y)
 
   ≲-resp-≈ : _≲_ Respects₂ _≈_
-  ≲-resp-≈ = ≲-respʳ-≈ , ≲-respˡ-≈
+  ≲-resp-≈ = ≲-respˡ-≈ , ≲-respʳ-≈
 
   ∼-respˡ-≈ = ≲-respˡ-≈
   {-# WARNING_ON_USAGE ∼-respˡ-≈
@@ -189,11 +189,11 @@ record IsStrictPartialOrder (_<_ : Rel A ℓ₂) : Set (a ⊔ ℓ ⊔ ℓ₂) wh
   asym : Asymmetric _<_
   asym {x} {y} = trans∧irr⇒asym Eq.refl trans irrefl {x = x} {y}
 
-  <-respʳ-≈ : _<_ Respectsʳ _≈_
-  <-respʳ-≈ = proj₁ <-resp-≈
-
   <-respˡ-≈ : _<_ Respectsˡ _≈_
-  <-respˡ-≈ = proj₂ <-resp-≈
+  <-respˡ-≈ = proj₁ <-resp-≈
+
+  <-respʳ-≈ : _<_ Respectsʳ _≈_
+  <-respʳ-≈ = proj₂ <-resp-≈
 
 
 record IsDecStrictPartialOrder (_<_ : Rel A ℓ₂) : Set (a ⊔ ℓ ⊔ ℓ₂) where
diff --git a/src/Relation/Unary/Properties.agda b/src/Relation/Unary/Properties.agda
index 5a108d9081..3045835fce 100644
--- a/src/Relation/Unary/Properties.agda
+++ b/src/Relation/Unary/Properties.agda
@@ -96,7 +96,7 @@ U-Universal = λ _ → _
 ⊂-respˡ-≐ (_ , R⊆Q) P⊂Q = ⊆-⊂-trans R⊆Q P⊂Q
 
 ⊂-resp-≐ : _Respects₂_ {A = Pred A ℓ} _⊂_ _≐_
-⊂-resp-≐ = ⊂-respʳ-≐ , ⊂-respˡ-≐
+⊂-resp-≐ = ⊂-respˡ-≐ , ⊂-respʳ-≐
 
 ⊂-irrefl : Irreflexive {A = Pred A ℓ₁} {B = Pred A ℓ₂} _≐_ _⊂_
 ⊂-irrefl (_ , Q⊆P) (_ , Q⊈P) = Q⊈P Q⊆P
@@ -150,7 +150,7 @@ U-Universal = λ _ → _
 ⊂′-respˡ-≐′ (_ , R⊆Q) P⊂Q = ⊆′-⊂′-trans R⊆Q P⊂Q
 
 ⊂′-resp-≐′ : _Respects₂_ {A = Pred A ℓ₁} _⊂′_ _≐′_
-⊂′-resp-≐′ = ⊂′-respʳ-≐′ , ⊂′-respˡ-≐′
+⊂′-resp-≐′ = ⊂′-respˡ-≐′ , ⊂′-respʳ-≐′
 
 ⊂′-irrefl : Irreflexive {A = Pred A ℓ₁} {B = Pred A ℓ₂} _≐′_ _⊂′_
 ⊂′-irrefl (_ , Q⊆P) (_ , Q⊈P) = Q⊈P Q⊆P