[ refactor ] exchange left and right in Data.List.Relation.Binary.Pointwise etc. congruence rules for _++_

CHANGELOG.md

@@ -356,8 +356,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`:
@@ -406,8 +406,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`:

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

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