Add left- and right- Pointwise congruence for _++_ on List

src/Data/List/Relation/Binary/Equality/Setoid.agda

@@ -116,6 +116,12 @@ foldr⁺ ∙⇔◦ e≈f xs≋ys = PW.foldr⁺ ∙⇔◦ e≈f xs≋ys
 ++⁺ : ∀ {ws xs ys zs} → ws ≋ xs → ys ≋ zs → ws ++ ys ≋ xs ++ zs
 ++⁺ = PW.++⁺
 
+++⁺ʳ : ∀ xs {ys zs} → ys ≋ zs → xs ++ ys ≋ xs ++ zs
+++⁺ʳ xs = PW.++⁺ʳ refl xs
+
+++⁺ˡ : ∀ {ws xs} → ws ≋ xs → ∀ zs → ws ++ zs ≋ xs ++ zs
+++⁺ˡ rs = PW.++⁺ˡ refl rs
+
 ++-cancelˡ : ∀ xs {ys zs} → xs ++ ys ≋ xs ++ zs → ys ≋ zs
 ++-cancelˡ xs = PW.++-cancelˡ xs
 

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

@@ -26,7 +26,7 @@ open import Relation.Nullary hiding (Irrelevant)
 import Relation.Nullary.Decidable as Dec using (map′)
 open import Relation.Unary as U using (Pred)
 open import Relation.Binary.Core renaming (Rel to Rel₂)
-open import Relation.Binary.Definitions using (_Respects_; _Respects₂_)
+open import Relation.Binary.Definitions using (Reflexive;_Respects_; _Respects₂_)
 open import Relation.Binary.Bundles using (Setoid; DecSetoid; Preorder; Poset)
 open import Relation.Binary.Structures using (IsEquivalence; IsDecEquivalence; IsPartialOrder; IsPreorder)
 open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_)
@@ -166,6 +166,15 @@ tabulate⁻ {n = suc n} (x∼y ∷ xs∼ys) (fsuc i) = tabulate⁻ xs∼ys i
 ++-cancelʳ {xs = xs}     (y ∷ ys) []       eq   =
   contradiction (≡.trans (≡.sym (length-++ (y ∷ ys))) (Pointwise-length eq)) (m≢1+n+m (length xs) ∘ ≡.sym)
 
+module _ (rfl : Reflexive R) where
+
+  ++⁺ʳ : ∀ xs → Pointwise R ys zs → Pointwise R (xs ++ ys) (xs ++ zs)
+  ++⁺ʳ xs = ++⁺ (refl rfl)
+
+  ++⁺ˡ : Pointwise R ws xs → ∀ zs → Pointwise R (ws ++ zs) (xs ++ zs)
+  ++⁺ˡ rs zs = ++⁺ rs (refl rfl)
+
+
 ------------------------------------------------------------------------
 -- concat
 
@@ -261,8 +270,7 @@ lookup⁺ (_   ∷ Rxys) (fsuc i) = lookup⁺ Rxys i
 
 Pointwise-≡⇒≡ : Pointwise {A = A} _≡_ ⇒ _≡_
 Pointwise-≡⇒≡ []               = ≡.refl
-Pointwise-≡⇒≡ (≡.refl ∷ xs∼ys) with Pointwise-≡⇒≡ xs∼ys
-... | ≡.refl = ≡.refl
+Pointwise-≡⇒≡ (≡.refl ∷ xs∼ys) = ≡.cong (_ ∷_) (Pointwise-≡⇒≡ xs∼ys)
 
 ≡⇒Pointwise-≡ :  _≡_ ⇒ Pointwise {A = A} _≡_
 ≡⇒Pointwise-≡ ≡.refl = refl ≡.refl