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 1/5] 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

From faaf1b9a19b569901f79b2e2f71a8f695424a270 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Mon, 9 Dec 2024 10:52:07 +0000
Subject: [PATCH 2/5] more knock-ons

---
 src/Algebra/Properties/Magma/Divisibility.agda        | 8 ++++----
 src/Relation/Binary/Construct/Add/Infimum/Strict.agda | 4 ++--
 2 files changed, 6 insertions(+), 6 deletions(-)

diff --git a/src/Algebra/Properties/Magma/Divisibility.agda b/src/Algebra/Properties/Magma/Divisibility.agda
index aa9f4e53c5..5bc1cfb29b 100644
--- a/src/Algebra/Properties/Magma/Divisibility.agda
+++ b/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ʳ-≈
 
 
 ------------------------------------------------------------------------
diff --git a/src/Relation/Binary/Construct/Add/Infimum/Strict.agda b/src/Relation/Binary/Construct/Add/Infimum/Strict.agda
index c1312d7b14..fd2a1373f6 100644
--- a/src/Relation/Binary/Construct/Add/Infimum/Strict.agda
+++ b/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

From e15a3c4a4b92283063c44dad3cc5d2f7ed2ca67a Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Mon, 9 Dec 2024 10:57:13 +0000
Subject: [PATCH 3/5] final knock-ons?

---
 src/Data/Integer/Properties.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Data/Integer/Properties.agda b/src/Data/Integer/Properties.agda
index f89d3164f6..6092bcb959 100644
--- a/src/Data/Integer/Properties.agda
+++ b/src/Data/Integer/Properties.agda
@@ -328,7 +328,7 @@ _<?_ : Decidable _<_
   { isEquivalence = isEquivalence
   ; irrefl        = <-irrefl
   ; trans         = <-trans
-  ; <-resp-≈      = subst (_ <_) , subst (_< _)
+  ; <-resp-≈      = subst (_< _) , subst (_ <_)
   }
 
 <-isStrictTotalOrder : IsStrictTotalOrder _≡_ _<_

From db6f05ef99b0af25afa5420ab63f5a7970e87fcd Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Mon, 9 Dec 2024 12:49:52 +0000
Subject: [PATCH 4/5] final knock-ons?

---
 .../Relation/Binary/Permutation/Setoid/Properties.agda |  8 ++++----
 src/Data/Product/Relation/Binary/Lex/Strict.agda       | 10 +++++-----
 src/Data/Rational/Properties.agda                      |  2 +-
 src/Data/Rational/Unnormalised/Properties.agda         |  6 +++---
 src/Data/Sum/Relation/Binary/LeftOrder.agda            |  2 +-
 src/Data/Vec/Relation/Binary/Lex/Core.agda             |  4 ++--
 src/Relation/Binary/Construct/StrictToNonStrict.agda   |  4 ++--
 src/Relation/Binary/Construct/Union.agda               |  2 +-
 .../Binary/Indexed/Homogeneous/Structures.agda         |  2 +-
 src/Relation/Binary/Morphism/OrderMonomorphism.agda    |  2 +-
 10 files changed, 21 insertions(+), 21 deletions(-)

diff --git a/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda b/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda
index d82178dd8b..ec1c568496 100644
--- a/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda
+++ b/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             =
diff --git a/src/Data/Product/Relation/Binary/Lex/Strict.agda b/src/Data/Product/Relation/Binary/Lex/Strict.agda
index 39d86602f2..b6a35188e7 100644
--- a/src/Data/Product/Relation/Binary/Lex/Strict.agda
+++ b/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 _≈₁_ →
diff --git a/src/Data/Rational/Properties.agda b/src/Data/Rational/Properties.agda
index 0341f53c45..99ad60ab13 100644
--- a/src/Data/Rational/Properties.agda
+++ b/src/Data/Rational/Properties.agda
@@ -699,7 +699,7 @@ _>?_ = flip _<?_
 <-respˡ-≡ = subst (_< _)
 
 <-resp-≡ : _<_ Respects₂ _≡_
-<-resp-≡ = <-respʳ-≡ , <-respˡ-≡
+<-resp-≡ = <-respˡ-≡ , <-respʳ-≡
 
 ------------------------------------------------------------------------
 -- Structures
diff --git a/src/Data/Rational/Unnormalised/Properties.agda b/src/Data/Rational/Unnormalised/Properties.agda
index 181e4a6189..42f19ebf04 100644
--- a/src/Data/Rational/Unnormalised/Properties.agda
+++ b/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 _≃_ _<_
diff --git a/src/Data/Sum/Relation/Binary/LeftOrder.agda b/src/Data/Sum/Relation/Binary/LeftOrder.agda
index d29a6a96ed..0863b5785e 100644
--- a/src/Data/Sum/Relation/Binary/LeftOrder.agda
+++ b/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 ≈₁ ≈₂) (∼₁ ⊎-< ∼₂)
diff --git a/src/Data/Vec/Relation/Binary/Lex/Core.agda b/src/Data/Vec/Relation/Binary/Lex/Core.agda
index 92237d4f18..211147da17 100644
--- a/src/Data/Vec/Relation/Binary/Lex/Core.agda
+++ b/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
 
diff --git a/src/Relation/Binary/Construct/StrictToNonStrict.agda b/src/Relation/Binary/Construct/StrictToNonStrict.agda
index d17b6017fc..ae00871972 100644
--- a/src/Relation/Binary/Construct/StrictToNonStrict.agda
+++ b/src/Relation/Binary/Construct/StrictToNonStrict.agda
@@ -61,7 +61,7 @@ antisym eq trans irrefl = as
 
 trans : IsEquivalence _≈_ → _<_ Respects₂ _≈_ → Transitive _<_ →
         Transitive _≤_
-trans eq (respʳ , respˡ) <-trans = tr
+trans eq (respˡ , respʳ) <-trans = tr
   where
   module Eq = IsEquivalence eq
 
@@ -88,7 +88,7 @@ trans eq (respʳ , respˡ) <-trans = tr
 ≤-respˡ-≈ sym trans respˡ x′≈x (inj₂ x′≈y) = inj₂ (trans (sym x′≈x) x′≈y)
 
 ≤-resp-≈ : IsEquivalence _≈_ → _<_ Respects₂ _≈_ → _≤_ Respects₂ _≈_
-≤-resp-≈ eq (respʳ , respˡ) = ≤-respʳ-≈ Eq.trans respʳ , ≤-respˡ-≈ Eq.sym Eq.trans respˡ
+≤-resp-≈ eq (respˡ , respʳ) = ≤-respˡ-≈ Eq.sym Eq.trans respˡ , ≤-respʳ-≈ Eq.trans respʳ
   where module Eq = IsEquivalence eq
 
 total : Trichotomous _≈_ _<_ → Total _≤_
diff --git a/src/Relation/Binary/Construct/Union.agda b/src/Relation/Binary/Construct/Union.agda
index 45f72c8190..c59f2b42cf 100644
--- a/src/Relation/Binary/Construct/Union.agda
+++ b/src/Relation/Binary/Construct/Union.agda
@@ -72,7 +72,7 @@ module _ {≈ : Rel B ℓ₁} (L : REL A B ℓ₂) (R : REL A B ℓ₃) where
 module _ {≈ : Rel A ℓ₁} {L : Rel A ℓ₂} {R : Rel A ℓ₃} where
 
   resp₂ : L Respects₂ ≈ → R Respects₂ ≈ → (L ∪ R) Respects₂ ≈
-  resp₂ (Lʳ , Lˡ) (Rʳ , Rˡ) = respʳ L R Lʳ Rʳ , respˡ L R Lˡ Rˡ
+  resp₂ (Lˡ , Lʳ) (Rˡ , Rʳ) = respˡ L R Lˡ Rˡ , respʳ L R Lʳ Rʳ
 
 module _ (≈ : REL A B ℓ₁) (L : REL A B ℓ₂) (R : REL A B ℓ₃) where
 
diff --git a/src/Relation/Binary/Indexed/Homogeneous/Structures.agda b/src/Relation/Binary/Indexed/Homogeneous/Structures.agda
index f5a941b65b..29ade77c90 100644
--- a/src/Relation/Binary/Indexed/Homogeneous/Structures.agda
+++ b/src/Relation/Binary/Indexed/Homogeneous/Structures.agda
@@ -115,7 +115,7 @@ record IsIndexedPreorder {ℓ₂} (_∼ᵢ_ : IRel A ℓ₂)
   ∼-respʳ-≈ x≈y z∼x i = ∼ᵢ-respʳ-≈ᵢ (x≈y i) (z∼x i)
 
   ∼-resp-≈ : (Lift A _∼ᵢ_) B.Respects₂ (Lift A _≈ᵢ_)
-  ∼-resp-≈ = ∼-respʳ-≈ , ∼-respˡ-≈
+  ∼-resp-≈ = ∼-respˡ-≈ , ∼-respʳ-≈
 
   isPreorder : B.IsPreorder (Lift A _≈ᵢ_) (Lift A _∼ᵢ_)
   isPreorder = record
diff --git a/src/Relation/Binary/Morphism/OrderMonomorphism.agda b/src/Relation/Binary/Morphism/OrderMonomorphism.agda
index 12a80d1f31..8add872d3d 100644
--- a/src/Relation/Binary/Morphism/OrderMonomorphism.agda
+++ b/src/Relation/Binary/Morphism/OrderMonomorphism.agda
@@ -62,7 +62,7 @@ respʳ : _≲₂_ Respectsʳ _≈₂_ → _≲₁_ Respectsʳ _≈₁_
 respʳ resp x≈y y∼z = cancel (resp (cong x≈y) (mono y∼z))
 
 resp : _≲₂_ Respects₂ _≈₂_ → _≲₁_ Respects₂ _≈₁_
-resp = map respʳ respˡ
+resp = map respˡ respʳ
 
 ------------------------------------------------------------------------
 -- Structures

From 40aba6e43206665427cfe01825853a2c78b3e353 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Sat, 18 Jan 2025 09:13:52 +0000
Subject: [PATCH 5/5] `CHANGELOG`: added fresh entry

---
 CHANGELOG.md | 545 +--------------------------------------------------
 1 file changed, 3 insertions(+), 542 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 5baa1c39f1..b36d36b7f1 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,7 +1,7 @@
-Version 2.2-dev
+Version 2.3-dev
 ===============
 
-The library has been tested using Agda 2.7.0.
+The library has been tested using Agda 2.7.0 and 2.7.0.1.
 
 Highlights
 ----------
@@ -9,19 +9,10 @@ Highlights
 Bug-fixes
 ---------
 
-* Removed unnecessary parameter `#-trans : Transitive _#_` from
-  `Relation.Binary.Reasoning.Base.Apartness`.
-* Relax the types for `≡-syntax` in `Relation.Binary.HeterogeneousEquality`.
-  These operators are used for equational reasoning of heterogeneous equality
-  `x ≅ y`, but previously the three operators in `≡-syntax` unnecessarily require
-  `x` and `y` to have the same type, making them unusable in most situations.
-
 Non-backwards compatible changes
 --------------------------------
 
-* 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).
+* [issue #2471](https://github.com/agda/agda-stdlib/issues/2471) In `Relation.Binary.Definitions`, the left/right order of the components of `_Respects₂_` have been swapped.
 
 Minor improvements
 ------------------
@@ -32,538 +23,8 @@ Deprecated modules
 Deprecated names
 ----------------
 
-* In `Algebra.Properties.CommutativeMagma.Divisibility`:
-  ```agda
-  ∣-factors    ↦  x|xy∧y|xy
-  ∣-factors-≈  ↦  xy≈z⇒x|z∧y|z
-  ```
-
-* In `Algebra.Properties.Magma.Divisibility`:
-  ```agda
-  ∣-respˡ   ↦  ∣-respˡ-≈
-  ∣-respʳ   ↦  ∣-respʳ-≈
-  ∣-resp    ↦  ∣-resp-≈
- ```
-
-* In `Algebra.Solver.CommutativeMonoid`:
-  ```agda
-  normalise-correct  ↦  Algebra.Solver.CommutativeMonoid.Normal.correct
-  sg                 ↦  Algebra.Solver.CommutativeMonoid.Normal.singleton
-  sg-correct         ↦  Algebra.Solver.CommutativeMonoid.Normal.singleton-correct
-  ```
-
-* In `Algebra.Solver.IdempotentCommutativeMonoid`:
-  ```agda
-  flip12             ↦  Algebra.Properties.CommutativeSemigroup.xy∙z≈y∙xz
-  distr              ↦  Algebra.Properties.IdempotentCommutativeMonoid.∙-distrˡ-∙
-  normalise-correct  ↦  Algebra.Solver.IdempotentCommutativeMonoid.Normal.correct
-  sg                 ↦  Algebra.Solver.IdempotentCommutativeMonoid.Normal.singleton
-  sg-correct         ↦  Algebra.Solver.IdempotentCommutativeMonoid.Normal.singleton-correct
-  ```
-
-* In `Algebra.Solver.Monoid`:
-  ```agda
-  homomorphic        ↦  Algebra.Solver.Monoid.Normal.comp-correct
-  normalise-correct  ↦  Algebra.Solver.Monoid.Normal.correct
-  ```
-
-* In `Data.List.Relation.Binary.Permutation.Setoid.Properties`:
-  ```agda
-  split  ↦  ↭-split
-  ```
-  with a more informative type (see below).
-  ```
-
-* In `Data.Vec.Properties`:
-  ```agda
-  ++-assoc _      ↦  ++-assoc-eqFree
-  ++-identityʳ _  ↦  ++-identityʳ-eqFree
-  unfold-∷ʳ _     ↦  unfold-∷ʳ-eqFree
-  ++-∷ʳ _         ↦  ++-∷ʳ-eqFree
-  ∷ʳ-++ _         ↦  ∷ʳ-++-eqFree
-  reverse-++ _    ↦  reverse-++-eqFree
-  ∷-ʳ++ _         ↦  ∷-ʳ++-eqFree
-  ++-ʳ++ _        ↦  ++-ʳ++-eqFree
-  ʳ++-ʳ++ _       ↦  ʳ++-ʳ++-eqFree
-  ```
-
 New modules
 -----------
 
-* Bundled morphisms between (raw) algebraic structures:
-  ```
-  Algebra.Morphism.Bundles
-  ```
-
-* Properties of `IdempotentCommutativeMonoid`s refactored out from `Algebra.Solver.IdempotentCommutativeMonoid`:
-  ```agda
-  Algebra.Properties.IdempotentCommutativeMonoid
-  ```
-
-* Consequences of module monomorphisms
-  ```agda
-  Algebra.Module.Morphism.BimoduleMonomorphism
-  Algebra.Module.Morphism.BisemimoduleMonomorphism
-  Algebra.Module.Morphism.LeftModuleMonomorphism
-  Algebra.Module.Morphism.LeftSemimoduleMonomorphism
-  Algebra.Module.Morphism.ModuleMonomorphism
-  Algebra.Module.Morphism.RightModuleMonomorphism
-  Algebra.Module.Morphism.RightSemimoduleMonomorphism
-  Algebra.Module.Morphism.SemimoduleMonomorphism
-  ```
-
-* Refactoring of the `Algebra.Solver.*Monoid` implementations, via
-  a single `Solver` module API based on the existing `Expr`, and
-  a common `Normal`-form API:
-  ```agda
-  Algebra.Solver.CommutativeMonoid.Normal
-  Algebra.Solver.IdempotentCommutativeMonoid.Normal
-  Algebra.Solver.Monoid.Expression
-  Algebra.Solver.Monoid.Normal
-  Algebra.Solver.Monoid.Solver
-  ```
-
-  NB Imports of the existing proof procedures `solve` and `prove` etc. should still be via the top-level interfaces in `Algebra.Solver.*Monoid`.
-
-* Refactored out from `Data.List.Relation.Unary.All.Properties` in order to break a dependency cycle with `Data.List.Membership.Setoid.Properties`:
-  ```agda
-  Data.List.Relation.Unary.All.Properties.Core
-  ```
-
-* `Data.List.Relation.Binary.Disjoint.Propositional.Properties`:
-  Propositional counterpart to `Data.List.Relation.Binary.Disjoint.Setoid.Properties`
-  ```agda
-  sum-↭ : sum Preserves _↭_ ⟶ _≡_
-  ```
-
-* `Data.List.Relation.Binary.Permutation.Propositional.Properties.WithK`
-
-* Refactored `Data.Refinement` into:
-  ```agda
-  Data.Refinement.Base
-  Data.Refinement.Properties
-  ```
-
-* Raw bundles for the `Relation.Binary.Bundles` hierarchy:
-  ```agda
-  Relation.Binary.Bundles.Raw
-  ```
-  plus adding `rawX` fields to each of `Relation.Binary.Bundles.X`.
-
-* `Data.List.Effectful.Foldable`: `List` is `Foldable`
-
-* `Data.Vec.Effectful.Foldable`: `Vec` is `Foldable`
-
-* `Effect.Foldable`: implementation of haskell-like `Foldable`
-
 Additions to existing modules
 -----------------------------
-
-* In `Algebra.Bundles.KleeneAlgebra`:
-  ```agda
-  rawKleeneAlgebra : RawKleeneAlgebra _ _
-  ```
-
-* In `Algebra.Bundles.Raw.RawRingWithoutOne`
-  ```agda
-  rawNearSemiring : RawNearSemiring c ℓ
-  ```
-
-* Exporting more `Raw` substructures from `Algebra.Bundles.Ring`:
-  ```agda
-  rawNearSemiring   : RawNearSemiring _ _
-  rawRingWithoutOne : RawRingWithoutOne _ _
-  +-rawGroup        : RawGroup _ _
-  ```
-
-* Exporting `RawRingWithoutOne` and `(Raw)NearSemiring` subbundles from
-  `Algebra.Bundles.RingWithoutOne`:
-  ```agda
-  nearSemiring      : NearSemiring _ _
-  rawNearSemiring   : RawNearSemiring _ _
-  rawRingWithoutOne : RawRingWithoutOne _ _
-  ```
-
-* In `Algebra.Morphism.Construct.Composition`:
-  ```agda
-  magmaHomomorphism          : MagmaHomomorphism M₁.rawMagma M₂.rawMagma →
-                               MagmaHomomorphism M₂.rawMagma M₃.rawMagma →
-                               MagmaHomomorphism M₁.rawMagma M₃.rawMagma
-  monoidHomomorphism         : MonoidHomomorphism M₁.rawMonoid M₂.rawMonoid →
-                               MonoidHomomorphism M₂.rawMonoid M₃.rawMonoid →
-                               MonoidHomomorphism M₁.rawMonoid M₃.rawMonoid
-  groupHomomorphism          : GroupHomomorphism M₁.rawGroup M₂.rawGroup →
-                               GroupHomomorphism M₂.rawGroup M₃.rawGroup →
-                               GroupHomomorphism M₁.rawGroup M₃.rawGroup
-  nearSemiringHomomorphism   : NearSemiringHomomorphism M₁.rawNearSemiring M₂.rawNearSemiring →
-                               NearSemiringHomomorphism M₂.rawNearSemiring M₃.rawNearSemiring →
-                               NearSemiringHomomorphism M₁.rawNearSemiring M₃.rawNearSemiring
-  semiringHomomorphism       : SemiringHomomorphism M₁.rawSemiring M₂.rawSemiring →
-                               SemiringHomomorphism M₂.rawSemiring M₃.rawSemiring →
-                               SemiringHomomorphism M₁.rawSemiring M₃.rawSemiring
-  kleeneAlgebraHomomorphism  : KleeneAlgebraHomomorphism M₁.rawKleeneAlgebra M₂.rawKleeneAlgebra →
-                               KleeneAlgebraHomomorphism M₂.rawKleeneAlgebra M₃.rawKleeneAlgebra →
-                               KleeneAlgebraHomomorphism M₁.rawKleeneAlgebra M₃.rawKleeneAlgebra
-  nearSemiringHomomorphism   : NearSemiringHomomorphism M₁.rawNearSemiring M₂.rawNearSemiring →
-                               NearSemiringHomomorphism M₂.rawNearSemiring M₃.rawNearSemiring →
-                               NearSemiringHomomorphism M₁.rawNearSemiring M₃.rawNearSemiring
-  ringWithoutOneHomomorphism : RingWithoutOneHomomorphism M₁.rawRingWithoutOne M₂.rawRingWithoutOne →
-                               RingWithoutOneHomomorphism M₂.rawRingWithoutOne M₃.rawRingWithoutOne →
-                               RingWithoutOneHomomorphism M₁.rawRingWithoutOne M₃.rawRingWithoutOne
-  ringHomomorphism           : RingHomomorphism M₁.rawRing M₂.rawRing →
-                               RingHomomorphism M₂.rawRing M₃.rawRing →
-                               RingHomomorphism M₁.rawRing M₃.rawRing
-  quasigroupHomomorphism     : QuasigroupHomomorphism M₁.rawQuasigroup M₂.rawQuasigroup →
-                               QuasigroupHomomorphism M₂.rawQuasigroup M₃.rawQuasigroup →
-                               QuasigroupHomomorphism M₁.rawQuasigroup M₃.rawQuasigroup
-  loopHomomorphism           : LoopHomomorphism M₁.rawLoop M₂.rawLoop →
-                               LoopHomomorphism M₂.rawLoop M₃.rawLoop →
-                               LoopHomomorphism M₁.rawLoop M₃.rawLoop
-  ```
-
-* In `Algebra.Morphism.Construct.Identity`:
-  ```agda
-  magmaHomomorphism          : MagmaHomomorphism M.rawMagma M.rawMagma
-  monoidHomomorphism         : MonoidHomomorphism M.rawMonoid M.rawMonoid
-  groupHomomorphism          : GroupHomomorphism M.rawGroup M.rawGroup
-  nearSemiringHomomorphism   : NearSemiringHomomorphism M.raw M.raw
-  semiringHomomorphism       : SemiringHomomorphism M.rawNearSemiring M.rawNearSemiring
-  kleeneAlgebraHomomorphism  : KleeneAlgebraHomomorphism M.rawKleeneAlgebra M.rawKleeneAlgebra
-  nearSemiringHomomorphism   : NearSemiringHomomorphism M.rawNearSemiring M.rawNearSemiring
-  ringWithoutOneHomomorphism : RingWithoutOneHomomorphism M.rawRingWithoutOne M.rawRingWithoutOne
-  ringHomomorphism           : RingHomomorphism M.rawRing M.rawRing
-  quasigroupHomomorphism     : QuasigroupHomomorphism M.rawQuasigroup M.rawQuasigroup
-  loopHomomorphism           : LoopHomomorphism M.rawLoop M.rawLoop
-  ```
-
-* In `Algebra.Morphism.Structures.RingMorphisms`
-  ```agda
-  isRingWithoutOneHomomorphism : IsRingWithoutOneHomomorphism ⟦_⟧
-  ```
-
-* In `Algebra.Morphism.Structures.RingWithoutOneMorphisms`
-  ```agda
-  isNearSemiringHomomorphism : IsNearSemiringHomomorphism ⟦_⟧
-  ```
-
-* Properties of non-divisibility in `Algebra.Properties.Magma.Divisibility`:
-  ```agda
-  ∤-respˡ-≈ : _∤_ Respectsˡ _≈_
-  ∤-respʳ-≈ : _∤_ Respectsʳ _≈_
-  ∤-resp-≈  : _∤_ Respects₂ _≈_
-  ∤∤-sym    : Symmetric _∤∤_
-  ∤∤-respˡ-≈ : _∤∤_ Respectsˡ _≈_
-  ∤∤-respʳ-≈ : _∤∤_ Respectsʳ _≈_
-  ∤∤-resp-≈  : _∤∤_ Respects₂ _≈_
-  ```
-
-* In `Algebra.Solver.Ring`
-  ```agda
-  Env : ℕ → Set _
-  Env = Vec Carrier
- ```
-
-* In `Algebra.Structures.RingWithoutOne`:
-  ```agda
-  isNearSemiring      : IsNearSemiring _ _
- ```
-
-* In `Data.List.Membership.Setoid.Properties`:
-  ```agda
-  ∉⇒All[≉]       : x ∉ xs → All (x ≉_) xs
-  All[≉]⇒∉       : All (x ≉_) xs → x ∉ xs
-  Any-∈-swap     : Any (_∈ ys) xs → Any (_∈ xs) ys
-  All-∉-swap     : All (_∉ ys) xs → All (_∉ xs) ys
-  ∈-map∘filter⁻  : y ∈₂ map f (filter P? xs) → ∃[ x ] x ∈₁ xs × y ≈₂ f x × P x
-  ∈-map∘filter⁺  : f Preserves _≈₁_ ⟶ _≈₂_ →
-                   ∃[ x ] x ∈₁ xs × y ≈₂ f x × P x →
-                   y ∈₂ map f (filter P? xs)
-  ∈-concatMap⁺   : Any ((y ∈_) ∘ f) xs → y ∈ concatMap f xs
-  ∈-concatMap⁻   : y ∈ concatMap f xs → Any ((y ∈_) ∘ f) xs
-  ∉[]            : x ∉ []
-  deduplicate-∈⇔ : _≈_ Respectsʳ (flip R) → z ∈ xs ⇔ z ∈ deduplicate R? xs
-  ```
-
-* In `Data.List.Membership.Propositional.Properties`:
-  ```agda
-  ∈-AllPairs₂    : AllPairs R xs → x ∈ xs → y ∈ xs → x ≡ y ⊎ R x y ⊎ R y x
-  ∈-map∘filter⁻  : y ∈ map f (filter P? xs) → (∃[ x ] x ∈ xs × y ≡ f x × P x)
-  ∈-map∘filter⁺  : (∃[ x ] x ∈ xs × y ≡ f x × P x) → y ∈ map f (filter P? xs)
-  ∈-concatMap⁺   : Any ((y ∈_) ∘ f) xs → y ∈ concatMap f xs
-  ∈-concatMap⁻   : y ∈ concatMap f xs → Any ((y ∈_) ∘ f) xs
-  ++-∈⇔          : v ∈ xs ++ ys ⇔ (v ∈ xs ⊎ v ∈ ys)
-  []∉map∷        : [] ∉ map (x ∷_) xss
-  map∷⁻          : xs ∈ map (y ∷_) xss → ∃[ ys ] ys ∈ xss × xs ≡ y ∷ ys
-  map∷-decomp∈   : (x ∷ xs) ∈ map (y ∷_) xss → x ≡ y × xs ∈ xss
-  ∈-map∷⁻        : xs ∈ map (x ∷_) xss → x ∈ xs
-  ∉[]            : x ∉ []
-  deduplicate-∈⇔ : z ∈ xs ⇔ z ∈ deduplicate _≈?_ xs
-  ```
-
-* In `Data.List.Membership.Propositional.Properties.WithK`:
-  ```agda
-  unique∧set⇒bag : Unique xs → Unique ys → xs ∼[ set ] ys → xs ∼[ bag ] ys
-  ```
-
-* In `Data.List.Properties`:
-  ```agda
-  product≢0    : All NonZero ns → NonZero (product ns)
-  ∈⇒≤product   : All NonZero ns → n ∈ ns → n ≤ product ns
-  concatMap-++ : concatMap f (xs ++ ys) ≡ concatMap f xs ++ concatMap f ys
-  filter-≐     : P ≐ Q → filter P? ≗ filter Q?
-
-  partition-is-foldr : partition P? ≗ foldr (λ x → if does (P? x) then Product.map₁ (x ∷_)
-                                                                  else Product.map₂ (x ∷_))
-                                            ([] , [])
-  ```
-
-* In `Data.List.Relation.Unary.All.Properties`:
-  ```agda
-  all⊆concat : (xss : List (List A)) → All (Sublist._⊆ concat xss) xss
-  ```
-
-* In `Data.List.Relation.Unary.Any.Properties`:
-  ```agda
-  concatMap⁺ : Any (Any P ∘ f) xs → Any P (concatMap f xs)
-  concatMap⁻ : Any P (concatMap f xs) → Any (Any P ∘ f) xs
-  ```
-
-* In `Data.List.Relation.Unary.Unique.Setoid.Properties`:
-  ```agda
-  Unique[x∷xs]⇒x∉xs : Unique S (x ∷ xs) → x ∉ xs
-  ```
-
-* In `Data.List.Relation.Unary.Unique.Propositional.Properties`:
-  ```agda
-  Unique[x∷xs]⇒x∉xs : Unique (x ∷ xs) → x ∉ xs
-  ```
-
-* In `Data.List.Relation.Binary.Equality.Setoid`:
-  ```agda
-  ++⁺ʳ : ∀ xs → ys ≋ zs → xs ++ ys ≋ xs ++ zs
-  ++⁺ˡ : ∀ zs → ws ≋ xs → ws ++ zs ≋ xs ++ zs
-  ```
-
-* In `Data.List.Relation.Binary.Permutation.Homogeneous`:
-  ```agda
-  steps : Permutation R xs ys → ℕ
-  ```
-
-* In `Data.List.Relation.Binary.Permutation.Propositional`:
-  constructor aliases
-  ```agda
-  ↭-refl  : Reflexive _↭_
-  ↭-prep  : ∀ x → xs ↭ ys → x ∷ xs ↭ x ∷ ys
-  ↭-swap  : ∀ x y → xs ↭ ys → x ∷ y ∷ xs ↭ y ∷ x ∷ ys
-  ```
-  and properties
-  ```agda
-  ↭-reflexive-≋ : _≋_ ⇒ _↭_
-  ↭⇒↭ₛ          : _↭_  ⇒ _↭ₛ_
-  ↭ₛ⇒↭          : _↭ₛ_ ⇒ _↭_
-  ```
-  where `_↭ₛ_` is the `Setoid (setoid _)` instance of `Permutation`
-
-* In `Data.List.Relation.Binary.Permutation.Propositional.Properties`:
-  ```agda
-  Any-resp-[σ∘σ⁻¹] : (σ : xs ↭ ys) (iy : Any P ys) →
-                     Any-resp-↭ (trans (↭-sym σ) σ) iy ≡ iy
-  ∈-resp-[σ∘σ⁻¹]   : (σ : xs ↭ ys) (iy : y ∈ ys) →
-                     ∈-resp-↭ (trans (↭-sym σ) σ) iy ≡ iy
-  product-↭        : product Preserves _↭_ ⟶ _≡_
-  ```
-
-* In `Data.List.Relation.Binary.Permutation.Setoid`:
-  ```agda
-  ↭-reflexive-≋ : _≋_  ⇒ _↭_
-  ↭-transˡ-≋    : LeftTrans _≋_ _↭_
-  ↭-transʳ-≋    : RightTrans _↭_ _≋_
-  ↭-trans′      : Transitive _↭_
-  ```
-
-* In `Data.List.Relation.Binary.Permutation.Setoid.Properties`:
-  ```agda
-  ↭-split : xs ↭ (as ++ [ v ] ++ bs) →
-            ∃₂ λ ps qs → xs ≋ (ps ++ [ v ] ++ qs) × (ps ++ qs) ↭ (as ++ bs)
-  drop-∷  : x ∷ xs ↭ x ∷ ys → xs ↭ ys
-  ```
-
-* In `Data.List.Relation.Binary.Pointwise`:
-  ```agda
-  ++⁺ʳ : Reflexive R → ∀ xs → (xs ++_) Preserves (Pointwise R) ⟶ (Pointwise R)
-  ++⁺ˡ : Reflexive R → ∀ zs → (_++ zs) Preserves (Pointwise R) ⟶ (Pointwise R)
-  ```
-
-* In `Data.List.Relation.Unary.All`:
-  ```agda
-  search : Decidable P → ∀ xs → All (∁ P) xs ⊎ Any P xs
-
-* In `Data.List.Relation.Binary.Subset.Setoid.Properties`:
-  ```agda
-  ∷⊈[]   : x ∷ xs ⊈ []
-  ⊆∷⇒∈∨⊆ : xs ⊆ y ∷ ys → y ∈ xs ⊎ xs ⊆ ys
-  ⊆∷∧∉⇒⊆ : xs ⊆ y ∷ ys → y ∉ xs → xs ⊆ ys
-  ```
-
-* In `Data.List.Relation.Binary.Subset.Propositional.Properties`:
-  ```agda
-  ∷⊈[]   : x ∷ xs ⊈ []
-  ⊆∷⇒∈∨⊆ : xs ⊆ y ∷ ys → y ∈ xs ⊎ xs ⊆ ys
-  ⊆∷∧∉⇒⊆ : xs ⊆ y ∷ ys → y ∉ xs → xs ⊆ ys
-  ```
-
-* In `Data.List.Relation.Binary.Subset.Propositional.Properties`:
-  ```agda
-  concatMap⁺ : xs ⊆ ys → concatMap f xs ⊆ concatMap f ys
-  ```
-
-* In `Data.List.Relation.Binary.Sublist.Heterogeneous.Properties`:
-  ```agda
-  Sublist-[]-universal : Universal (Sublist R [])
-  ```
-
-* In `Data.List.Relation.Binary.Sublist.Setoid.Properties`:
-  ```agda
-  []⊆-universal : Universal ([] ⊆_)
-  ```
-
-* In `Data.List.Relation.Binary.Disjoint.Setoid.Properties`:
-  ```agda
-  deduplicate⁺ : Disjoint S xs ys → Disjoint S (deduplicate _≟_ xs) (deduplicate _≟_ ys)
-  ```
-
-* In `Data.List.Relation.Binary.Disjoint.Propositional.Properties`:
-  ```agda
-  deduplicate⁺ : Disjoint xs ys → Disjoint (deduplicate _≟_ xs) (deduplicate _≟_ ys)
-  ```
-
-* In `Data.List.Relation.Binary.Permutation.Propositional.Properties.WithK`:
-  ```agda
-  dedup-++-↭ : Disjoint xs ys →
-               deduplicate _≟_ (xs ++ ys) ↭ deduplicate _≟_ xs ++ deduplicate _≟_ ys
-  ```
-
-* In `Data.List.Relation.Unary.First.Properties`:
-  ```agda
-  ¬First⇒All : ∁ Q ⊆ P → ∁ (First P Q) ⊆ All P
-  ¬All⇒First : Decidable P → ∁ P ⊆ Q → ∁ (All P) ⊆ First P Q
-  ```
-
-* In `Data.Maybe.Properties`:
-  ```agda
-  maybe′-∘ : ∀ f g → f ∘ (maybe′ g b) ≗ maybe′ (f ∘ g) (f b)
-  ```
-
-* New lemmas in `Data.Nat.Properties`:
-  ```agda
-  m≤n⇒m≤n*o : ∀ o .{{_ : NonZero o}} → m ≤ n → m ≤ n * o
-  m≤n⇒m≤o*n : ∀ o .{{_ : NonZero o}} → m ≤ n → m ≤ o * n
-  <‴-irrefl : Irreflexive _≡_ _<‴_
-  ≤‴-irrelevant : Irrelevant {A = ℕ} _≤‴_
-  <‴-irrelevant : Irrelevant {A = ℕ} _<‴_
-  >‴-irrelevant : Irrelevant {A = ℕ} _>‴_
-  ≥‴-irrelevant : Irrelevant {A = ℕ} _≥‴_
-  ```
-
-  adjunction between `suc` and `pred`
-  ```agda
-  suc[m]≤n⇒m≤pred[n] : suc m ≤ n → m ≤ pred n
-  m≤pred[n]⇒suc[m]≤n : .{{NonZero n}} → m ≤ pred n → suc m ≤ n
-  ```
-
-* In `Data.Product.Function.Dependent.Propositional`:
-  ```agda
-  congˡ : ∀ {k} → (∀ {x} → A x ∼[ k ] B x) → Σ I A ∼[ k ] Σ I B
-  ```
-
-* New lemmas in `Data.Rational.Properties`:
-  ```agda
-  nonNeg+nonNeg⇒nonNeg : ∀ p .{{_ : NonNegative p}} q .{{_ : NonNegative q}} → NonNegative (p + q)
-  nonPos+nonPos⇒nonPos : ∀ p .{{_ : NonPositive p}} q .{{_ : NonPositive q}} → NonPositive (p + q)
-  pos+nonNeg⇒pos : ∀ p .{{_ : Positive p}} q .{{_ : NonNegative q}} → Positive (p + q)
-  nonNeg+pos⇒pos : ∀ p .{{_ : NonNegative p}} q .{{_ : Positive q}} → Positive (p + q)
-  pos+pos⇒pos : ∀ p .{{_ : Positive p}} q .{{_ : Positive q}} → Positive (p + q)
-  neg+nonPos⇒neg : ∀ p .{{_ : Negative p}} q .{{_ : NonPositive q}} → Negative (p + q)
-  nonPos+neg⇒neg : ∀ p .{{_ : NonPositive p}} q .{{_ : Negative q}} → Negative (p + q)
-  neg+neg⇒neg : ∀ p .{{_ : Negative p}} q .{{_ : Negative q}} → Negative (p + q)
-  nonNeg*nonNeg⇒nonNeg : ∀ p .{{_ : NonNegative p}} q .{{_ : NonNegative q}} → NonNegative (p * q)
-  nonPos*nonNeg⇒nonPos : ∀ p .{{_ : NonPositive p}} q .{{_ : NonNegative q}} → NonPositive (p * q)
-  nonNeg*nonPos⇒nonPos : ∀ p .{{_ : NonNegative p}} q .{{_ : NonPositive q}} → NonPositive (p * q)
-  nonPos*nonPos⇒nonPos : ∀ p .{{_ : NonPositive p}} q .{{_ : NonPositive q}} → NonNegative (p * q)
-  pos*pos⇒pos : ∀ p .{{_ : Positive p}} q .{{_ : Positive q}} → Positive (p * q)
-  neg*pos⇒neg : ∀ p .{{_ : Negative p}} q .{{_ : Positive q}} → Negative (p * q)
-  pos*neg⇒neg : ∀ p .{{_ : Positive p}} q .{{_ : Negative q}} → Negative (p * q)
-  neg*neg⇒pos : ∀ p .{{_ : Negative p}} q .{{_ : Negative q}} → Positive (p * q)
-  ```
-
-* New properties re-exported from `Data.Refinement`:
-  ```agda
-  value-injective : value v ≡ value w → v ≡ w
-  _≟_             : DecidableEquality A → DecidableEquality [ x ∈ A ∣ P x ]
- ```
-
-* New lemma in `Data.Vec.Properties`:
-  ```agda
-  map-concat : map f (concat xss) ≡ concat (map (map f) xss)
-  ```
-
-* In `Data.Vec.Relation.Binary.Equality.DecPropositional`:
-  ```agda
-  _≡?_ : DecidableEquality (Vec A n)
-  ```
-
-* In `Function.Related.TypeIsomorphisms`:
-  ```agda
-  Σ-distribˡ-⊎ : (∃ λ a → P a ⊎ Q a) ↔ (∃ P ⊎ ∃ Q)
-  Σ-distribʳ-⊎ : (Σ (A ⊎ B) P) ↔ (Σ A (P ∘ inj₁) ⊎ Σ B (P ∘ inj₂))
-  ×-distribˡ-⊎ : (A × (B ⊎ C)) ↔ (A × B ⊎ A × C)
-  ×-distribʳ-⊎ : ((A ⊎ B) × C) ↔ (A × C ⊎ B × C)
-  ∃-≡ : ∀ (P : A → Set b) {x} → P x ↔ (∃[ y ] y ≡ x × P y)
- ```
-
-* In `Relation.Binary.Bundles`:
-  ```agda
-  record DecPreorder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂))
-  ```
-  plus associated sub-bundles.
-
-* In `Relation.Binary.Construct.Interior.Symmetric`:
-  ```agda
-  decidable         : Decidable R → Decidable (SymInterior R)
-  ```
-  and for `Reflexive` and `Transitive` relations `R`:
-  ```agda
-  isDecEquivalence  : Decidable R → IsDecEquivalence (SymInterior R)
-  isDecPreorder     : Decidable R → IsDecPreorder (SymInterior R) R
-  isDecPartialOrder : Decidable R → IsDecPartialOrder (SymInterior R) R
-  decPreorder       : Decidable R → DecPreorder _ _ _
-  decPoset          : Decidable R → DecPoset _ _ _
-  ```
-
-* In `Relation.Binary.Structures`:
-  ```agda
-  record IsDecPreorder (_≲_ : Rel A ℓ₂) : Set (a ⊔ ℓ ⊔ ℓ₂) where
-    field
-      isPreorder : IsPreorder _≲_
-      _≟_        : Decidable _≈_
-      _≲?_       : Decidable _≲_
-  ```
-  plus associated `isDecPreorder` fields in each higher `IsDec*Order` structure.
-
-* In `Relation.Nullary.Decidable`:
-  ```agda
-  does-⇔  : A ⇔ B → (a? : Dec A) → (b? : Dec B) → does a? ≡ does b?
-  does-≡  : (a? b? : Dec A) → does a? ≡ does b?
-  ```
-
-* In `Relation.Nullary.Recomputable`:
-  ```agda
-  irrelevant-recompute : Recomputable (Irrelevant A)
-  ```
-
-* In `Relation.Unary.Properties`:
-  ```agda
-  map    : P ≐ Q → Decidable P → Decidable Q
-  does-≐ : P ≐ Q → (P? : Decidable P) → (Q? : Decidable Q) → does ∘ P? ≗ does ∘ Q?
-  does-≡ : (P? P?′ : Decidable P) → does ∘ P? ≗ does ∘ P?′
-  ```