[ refactor ] Exchange components of Relation.Binary.Definitions._Respects₂_

CHANGELOG.md

@@ -19,9 +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 `Data.List.Relation.Binary.Sublist.Propositional.Properties` the implicit module parameters `a` and `A` have been replaced with `variable`s. This should be a backwards compatible change for the overwhelming majority of uses, and would only be non-backwards compatible if you were explicitly supplying these implicit parameters for some reason when importing the module. Explicitly supplying the implicit parameters for functions exported from the module should not be affected.
+* 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
 ------------------

src/Algebra/Properties/Magma/Divisibility.agda

@@ -33,7 +33,7 @@ open import Algebra.Definitions.RawMagma rawMagma public
 ∣-respˡ-≈ x≈z (q , qx≈y) = q , trans (∙-congˡ (sym x≈z)) qx≈y
 
 ∣-resp-≈ : _∣_ Respects₂ _≈_
-∣-resp-≈ = ∣-respʳ-≈ , ∣-respˡ-≈
+∣-resp-≈ = ∣-respˡ-≈ , ∣-respʳ-≈
 
 x∣yx : ∀ x y → x ∣ y ∙ x
 x∣yx x y = y , refl
@@ -51,7 +51,7 @@ xy≈z⇒y∣z x y xy≈z = ∣-respʳ-≈ xy≈z (x∣yx y x)
 ∤-respʳ-≈ x≈y z∤x z∣y = contradiction (∣-respʳ-≈ (sym x≈y) z∣y) z∤x
 
 ∤-resp-≈ : _∤_ Respects₂ _≈_
-∤-resp-≈ = ∤-respʳ-≈ , ∤-respˡ-≈
+∤-resp-≈ = ∤-respˡ-≈ , ∤-respʳ-≈
 
 ------------------------------------------------------------------------
 -- Properties of mutual divisibility _∣∣_
@@ -66,7 +66,7 @@ xy≈z⇒y∣z x y xy≈z = ∣-respʳ-≈ xy≈z (x∣yx y x)
 ∣∣-respʳ-≈ y≈z (x∣y , y∣x) = ∣-respʳ-≈ y≈z x∣y , ∣-respˡ-≈ y≈z y∣x
 
 ∣∣-resp-≈ : _∣∣_ Respects₂ _≈_
-∣∣-resp-≈ = ∣∣-respʳ-≈ , ∣∣-respˡ-≈
+∣∣-resp-≈ = ∣∣-respˡ-≈ , ∣∣-respʳ-≈
 
 ------------------------------------------------------------------------
 -- Properties of mutual non-divisibility _∤∤_
@@ -81,7 +81,7 @@ xy≈z⇒y∣z x y xy≈z = ∣-respʳ-≈ xy≈z (x∣yx y x)
 ∤∤-respʳ-≈ x≈y z∤∤x z∣∣y = contradiction (∣∣-respʳ-≈ (sym x≈y) z∣∣y) z∤∤x
 
 ∤∤-resp-≈ : _∤∤_ Respects₂ _≈_
-∤∤-resp-≈ = ∤∤-respʳ-≈ , ∤∤-respˡ-≈
+∤∤-resp-≈ = ∤∤-respˡ-≈ , ∤∤-respʳ-≈
 
 
 ------------------------------------------------------------------------

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

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 _≡_ _<_

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

src/Data/Integer/Properties.agda

@@ -328,7 +328,7 @@ _<?_ : Decidable _<_
   { isEquivalence = isEquivalence
   ; irrefl        = <-irrefl
   ; trans         = <-trans
-  ; <-resp-≈      = subst (_ <_) , subst (_< _)
+  ; <-resp-≈      = subst (_< _) , subst (_ <_)
   }
 
 <-isStrictTotalOrder : IsStrictTotalOrder _≡_ _<_

src/Data/List/Relation/Binary/Lex.agda

@@ -68,36 +68,36 @@ 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
     trans (base y)         halt             = halt
     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 ⇔ [] < []

src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda

@@ -84,11 +84,11 @@ Any-resp-↭ resp (trans p₁ p₂) pxs                = Any-resp-↭ resp p₂
 
 AllPairs-resp-↭ : Symmetric R → R Respects₂ _≈_ → (AllPairs R) Respects _↭_
 AllPairs-resp-↭ sym resp (refl xs≋ys)     pxs             = AllPairs-resp-≋ resp xs≋ys pxs
-AllPairs-resp-↭ sym resp (prep x≈y p)     (∼ ∷ pxs)       =
-  All-resp-↭ (proj₁ resp) p (All.map (proj₂ resp x≈y) ∼) ∷
+AllPairs-resp-↭ sym resp@(rˡ , rʳ) (prep x≈y p)     (∼ ∷ pxs)       =
+  All-resp-↭ rʳ p (All.map (rˡ x≈y) ∼) ∷
   AllPairs-resp-↭ sym resp p pxs
-AllPairs-resp-↭ sym resp@(rʳ , rˡ) (swap eq₁ eq₂ p) ((∼₁ ∷ ∼₂) ∷ ∼₃ ∷ pxs) =
-  (sym (rʳ eq₂ (rˡ eq₁ ∼₁)) ∷ All-resp-↭ rʳ p (All.map (rˡ eq₂) ∼₃)) ∷
+AllPairs-resp-↭ sym resp@(rˡ , rʳ) (swap eq₁ eq₂ p) ((∼₁ ∷ ∼₂) ∷ ∼₃ ∷ pxs) =
+  (sym (rˡ eq₁ (rʳ eq₂ ∼₁)) ∷ All-resp-↭ rʳ p (All.map (rˡ eq₂) ∼₃)) ∷
   All-resp-↭ rʳ p (All.map (rˡ eq₁) ∼₂) ∷
   AllPairs-resp-↭ sym resp p pxs
 AllPairs-resp-↭ sym resp (trans p₁ p₂)    pxs             =

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

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 []

src/Data/Nat/Properties.agda

@@ -404,7 +404,7 @@ _>?_ = flip _<?_
 <-irrelevant = ≤-irrelevant
 
 <-resp₂-≡ : _<_ Respects₂ _≡_
-<-resp₂-≡ = subst (_ <_) , subst (_< _)
+<-resp₂-≡ = subst (_< _) , subst (_ <_)
 
 ------------------------------------------------------------------------
 -- Bundles

src/Data/Product/Relation/Binary/Lex/Strict.agda

@@ -62,16 +62,16 @@ module _ {_≈₁_ : Rel A ℓ₁} {_<₁_ : Rel A ℓ₂} {_<₂_ : Rel B ℓ
 
   ×-transitive : IsEquivalence _≈₁_ → _<₁_ Respects₂ _≈₁_ → Transitive _<₁_ →
                  Transitive _<₂_ → Transitive _<ₗₑₓ_
-  ×-transitive eq₁ resp₁ trans₁ trans₂ = trans
+  ×-transitive eq₁ resp₁@(respˡ , respʳ) trans₁ trans₂ = trans
     where
     module Eq₁ = IsEquivalence eq₁
 
     trans : Transitive _<ₗₑₓ_
     trans (inj₁ x₁<y₁) (inj₁ y₁<z₁) = inj₁ (trans₁ x₁<y₁ y₁<z₁)
     trans (inj₁ x₁<y₁) (inj₂ y≈≤z)  =
-      inj₁ (proj₁ resp₁ (proj₁ y≈≤z) x₁<y₁)
+      inj₁ (respʳ (proj₁ y≈≤z) x₁<y₁)
     trans (inj₂ x≈≤y)  (inj₁ y₁<z₁) =
-      inj₁ (proj₂ resp₁ (Eq₁.sym $ proj₁ x≈≤y) y₁<z₁)
+      inj₁ (respˡ (Eq₁.sym $ proj₁ x≈≤y) y₁<z₁)
     trans (inj₂ x≈≤y)  (inj₂ y≈≤z)  =
       inj₂ ( Eq₁.trans (proj₁ x≈≤y) (proj₁ y≈≤z)
            , trans₂    (proj₂ x≈≤y) (proj₂ y≈≤z))
@@ -157,8 +157,8 @@ module _ {_≈₁_ : Rel A ℓ₁} {_<₁_ : Rel A ℓ₂}
   ×-respects₂ : IsEquivalence _≈₁_ →
                 _<₁_ Respects₂ _≈₁_ → _<₂_ Respects₂ _≈₂_ →
                 _<ₗₑₓ_ Respects₂ _≋_
-  ×-respects₂ eq₁ resp₁ resp₂ = ×-respectsʳ trans (proj₁ resp₁) (proj₁ resp₂)
-                              , ×-respectsˡ sym trans (proj₂ resp₁) (proj₂ resp₂)
+  ×-respects₂ eq₁ resp₁ resp₂ = ×-respectsˡ sym trans (proj₁ resp₁) (proj₁ resp₂)
+                              , ×-respectsʳ trans (proj₂ resp₁) (proj₂ resp₂)
     where open IsEquivalence eq₁
 
   ×-compare : Symmetric _≈₁_ →

src/Data/Rational/Properties.agda

@@ -699,7 +699,7 @@ _>?_ = flip _<?_
 <-respˡ-≡ = subst (_< _)
 
 <-resp-≡ : _<_ Respects₂ _≡_
-<-resp-≡ = <-respʳ-≡ , <-respˡ-≡
+<-resp-≡ = <-respˡ-≡ , <-respʳ-≡
 
 ------------------------------------------------------------------------
 -- Structures

src/Data/Rational/Unnormalised/Properties.agda

@@ -258,7 +258,7 @@ drop-*≤* (*≤* pq≤qp) = pq≤qp
 ≤-respʳ-≃ x≈y z≤x = ≤-trans z≤x (≤-reflexive x≈y)
 
 ≤-resp₂-≃ : _≤_ Respects₂ _≃_
-≤-resp₂-≃ = ≤-respʳ-≃ , ≤-respˡ-≃
+≤-resp₂-≃ = ≤-respˡ-≃ , ≤-respʳ-≃
 
 infix 4 _≤?_ _≥?_
 
@@ -532,7 +532,7 @@ _>?_ = flip _<?_
   $ neg-mono-< (<-respʳ-≃ (-‿cong q≃r) (neg-mono-< q<p))
 
 <-resp-≃ : _<_ Respects₂ _≃_
-<-resp-≃ = <-respʳ-≃ , <-respˡ-≃
+<-resp-≃ = <-respˡ-≃ , <-respʳ-≃
 
 ------------------------------------------------------------------------
 -- Structures
@@ -542,7 +542,7 @@ _>?_ = flip _<?_
   { isEquivalence = isEquivalence
   ; irrefl        = <-irrefl-≡
   ; trans         = <-trans
-  ; <-resp-≈      = subst (_ <_) , subst (_< _)
+  ; <-resp-≈      = subst (_< _) , subst (_ <_)
   }
 
 <-isStrictPartialOrder : IsStrictPartialOrder _≃_ _<_

src/Data/Sum/Relation/Binary/LeftOrder.agda

@@ -118,7 +118,7 @@ module _ {a₁ a₂} {A₁ : Set a₁} {A₂ : Set a₂}
 
   ⊎-<-respects₂ : ∼₁ Respects₂ ≈₁ → ∼₂ Respects₂ ≈₂ →
                   (∼₁ ⊎-< ∼₂) Respects₂ (Pointwise ≈₁ ≈₂)
-  ⊎-<-respects₂ (r₁ , l₁) (r₂ , l₂) = ⊎-<-respectsʳ r₁ r₂ , ⊎-<-respectsˡ l₁ l₂
+  ⊎-<-respects₂ (l₁ , r₁) (l₂ , r₂) = ⊎-<-respectsˡ l₁ l₂ , ⊎-<-respectsʳ r₁ r₂
 
   ⊎-<-trichotomous : Trichotomous ≈₁ ∼₁ → Trichotomous ≈₂ ∼₂ →
                      Trichotomous (Pointwise ≈₁ ≈₂) (∼₁ ⊎-< ∼₂)

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

src/Data/Vec/Relation/Binary/Lex/Core.agda

@@ -94,7 +94,7 @@ module _ {P : Set} {_≈_ : Rel A ℓ₁} {_≺_ : Rel A ℓ₂} where
   ∷<∷-⇔ = mk⇔ [ flip this refl , uncurry next ] toSum
 
   module _ (≈-equiv : IsPartialEquivalence _≈_)
-           ((≺-respʳ-≈ , ≺-respˡ-≈) : _≺_ Respects₂ _≈_)
+           ((≺-respˡ-≈ , ≺-respʳ-≈) : _≺_ Respects₂ _≈_)
            (≺-trans : Transitive _≺_)
            (open IsPartialEquivalence ≈-equiv)
            where
@@ -131,7 +131,7 @@ module _ {P : Set} {_≈_ : Rel A ℓ₁} {_≺_ : Rel A ℓ₂} where
     respectsʳ resp (x≈y ∷ xs≋ys) (next x≈z xs<zs) = next (trans x≈z x≈y) (respectsʳ resp xs≋ys xs<zs)
 
     respects₂ : _≺_ Respects₂ _≈_ → ∀ {n} → (_<ₗₑₓ_ {n} {n}) Respects₂ _≋_
-    respects₂ (≺-resp-≈ʳ , ≺-resp-≈ˡ) = respectsʳ ≺-resp-≈ʳ , respectsˡ ≺-resp-≈ˡ
+    respects₂ (≺-resp-≈ˡ , ≺-resp-≈ʳ) = respectsˡ ≺-resp-≈ˡ , respectsʳ ≺-resp-≈ʳ
 
   module _ (P? : Dec P) (_≈?_ : Decidable _≈_) (_≺?_ : Decidable _≺_) where
 

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

src/Relation/Binary/Construct/Add/Infimum/Strict.agda

@@ -96,7 +96,7 @@ module _ {r} {_≤_ : Rel A r} where
 <₋-respʳ-≡ = subst (_ <₋_)
 
 <₋-resp-≡ : _<₋_ Respects₂ _≡_
-<₋-resp-≡ = <₋-respʳ-≡ , <₋-respˡ-≡
+<₋-resp-≡ = <₋-respˡ-≡ , <₋-respʳ-≡
 
 ------------------------------------------------------------------------
 -- Relational properties + setoid equality
@@ -127,7 +127,7 @@ module _ {e} {_≈_ : Rel A e} where
   <₋-respʳ-≈₋ <-respʳ-≈ [ p ] [ q ]    = [ <-respʳ-≈ p q ]
 
   <₋-resp-≈₋ : _<_ Respects₂ _≈_ → _<₋_ Respects₂ _≈₋_
-  <₋-resp-≈₋ = map <₋-respʳ-≈₋ <₋-respˡ-≈₋
+  <₋-resp-≈₋ = map <₋-respˡ-≈₋ <₋-respʳ-≈₋
 
 ------------------------------------------------------------------------
 -- Structures + propositional equality

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

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
 

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

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)

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)