Fixes #2352: exchanges left and right (#2535)

agda · Jan 2, 2025 · d481f5c · d481f5c
1 parent 429e617
commit d481f5c
Show file tree

Hide file tree

Showing 3 changed files with 12 additions and 12 deletions.
diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -377,8 +377,8 @@ Additions to existing modules
 
 * In `Data.List.Relation.Binary.Equality.Setoid`:
   ```agda
-  ++⁺ʳ : ∀ xs → ys ≋ zs → xs ++ ys ≋ xs ++ zs
-  ++⁺ˡ : ∀ zs → ws ≋ xs → ws ++ zs ≋ xs ++ zs
+  ++⁺ˡ : ∀ xs → ys ≋ zs → xs ++ ys ≋ xs ++ zs
+  ++⁺ʳ : ∀ zs → ws ≋ xs → ws ++ zs ≋ xs ++ zs
   ```
 
 * In `Data.List.Relation.Binary.Permutation.Homogeneous`:
@@ -427,8 +427,8 @@ Additions to existing modules
 
 * 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)
+  ++⁺ˡ : Reflexive R → ∀ xs → (xs ++_) Preserves (Pointwise R) ⟶ (Pointwise R)
+  ++⁺ʳ : Reflexive R → ∀ zs → (_++ zs) Preserves (Pointwise R) ⟶ (Pointwise R)
   ```
 
 * In `Data.List.Relation.Unary.All`:

diff --git a/src/Data/List/Relation/Binary/Equality/Setoid.agda b/src/Data/List/Relation/Binary/Equality/Setoid.agda
@@ -111,11 +111,11 @@ foldr⁺ ∙⇔◦ e≈f xs≋ys = PW.foldr⁺ ∙⇔◦ e≈f xs≋ys
 ++⁺ : ws ≋ xs → ys ≋ zs → ws ++ ys ≋ xs ++ zs
 ++⁺ = PW.++⁺
 
-++⁺ʳ : ∀ xs → ys ≋ zs → xs ++ ys ≋ xs ++ zs
-++⁺ʳ xs = PW.++⁺ʳ refl xs
+++⁺ˡ : ∀ xs → ys ≋ zs → xs ++ ys ≋ xs ++ zs
+++⁺ˡ xs = PW.++⁺ˡ refl xs
 
-++⁺ˡ : ∀ zs → ws ≋ xs → ws ++ zs ≋ xs ++ zs
-++⁺ˡ zs = PW.++⁺ˡ refl zs
+++⁺ʳ : ∀ zs → ws ≋ xs → ws ++ zs ≋ xs ++ zs
+++⁺ʳ zs = PW.++⁺ʳ refl zs
 
 ++-cancelˡ : ∀ xs {ys zs} → xs ++ ys ≋ xs ++ zs → ys ≋ zs
 ++-cancelˡ xs = PW.++-cancelˡ xs

diff --git a/src/Data/List/Relation/Binary/Pointwise.agda b/src/Data/List/Relation/Binary/Pointwise.agda
@@ -168,11 +168,11 @@ tabulate⁻ {n = suc n} (x∼y ∷ xs∼ys) (fsuc i) = tabulate⁻ xs∼ys i
 
 module _ (rfl : Reflexive R) where
 
-  ++⁺ʳ : ∀ xs → (xs ++_) Preserves (Pointwise R) ⟶ (Pointwise R)
-  ++⁺ʳ xs = ++⁺ (refl rfl)
+  ++⁺ˡ : ∀ xs → (xs ++_) Preserves (Pointwise R) ⟶ (Pointwise R)
+  ++⁺ˡ xs = ++⁺ (refl rfl)
 
-  ++⁺ˡ : ∀ zs → (_++ zs) Preserves (Pointwise R) ⟶ (Pointwise R)
-  ++⁺ˡ zs rs = ++⁺ rs (refl rfl)
+  ++⁺ʳ : ∀ zs → (_++ zs) Preserves (Pointwise R) ⟶ (Pointwise R)
+  ++⁺ʳ zs rs = ++⁺ rs (refl rfl)
 
 
 ------------------------------------------------------------------------