Add left and right versions of ++⁺ for pointwise relations

[mechvel]

Data.List.Relation.Binary.Pointwise has

module _ {_∼_ : REL A B ℓ} where                                                                                                                                
  ++⁺ : ∀ {ws xs ys zs} → Pointwise _∼_ ws xs → Pointwise _∼_ ys zs →             
                                        Pointwise _∼_ (ws ++ ys) (xs ++ zs)  

According to the library style, needs it to be
++-cong₂ : _++_ Preserves₂ (Pointwise _~_) ⟶ (Pointwise _~_) ⟶ (Pointwise _~_)
?
There remains a question of the difference between REL A B _ and Rel A _, Rel B _.
So that I wonder.
Anyway, it has, probably, sense to add lemmas derived from ++⁺, named ++-cong<foo>,
and having Preserves/Preserves₂ in the signature.
For example, in my program, I write for lists over a setoid:

  ++cong1=ₗ :   ∀ {ys} → (_++ ys) Preserves _=ₗ_ ⟶ _=ₗ_
  ++cong1=ₗ {ys} ws=ₗxs =   ++⁺ {_∼_ = _≈_} ws=ₗxs =ₗrefl 

[jamesmckinna]

For Lists defined over a Setoid, S say, you can now, since #2393 (part of the v2.1-rc1), proceed as follows: instead of defining such things directly, write

open import Data.List.Relation.Binary.Equality.Setoid S using (isMagma)
open IsMagma isMagma using () renaming (∙-congʳ to ++⁺ʳ; ∙-congˡ to ++⁺ˡ)

(or whatever names you find convenient)

This does not tackle the Pointwise heterogeneous definitions directly, but suffices for the homogeneous Equality.Setoid case.

Suggest closing this issue now, unless the full generality for Pointwise is required... in which case #2426 will eventually do so.