Fixes agda#2471

Author: jamesmckinna

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

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

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 _≈_ →

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

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

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

src/Relation/Binary/Reasoning/Base/Triple.agda

@@ -55,15 +55,15 @@ 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)
 ≤-go x≤y (nonstrict y≤z) = nonstrict (trans x≤y y≤z)
 ≤-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)
 

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

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