[Agda] `Pointwise' over Setoid

[Sergei Meshveliani]

Dear Standard library developers,

(I am sorry, if this was discussed earlier)

Standard library provides  map-cong, map-id, map-compose  
as related to the propositional equality _≡_.
But the case of  List over Setoid  is highly usable.

And I suggest this:

-----------------------------------------------------------------------
module OfMapsToSetoid {α β β=} (A : Set α) (S : Setoid β β=)
 where
 open Setoid S using (_≈_)
               renaming (Carrier to B; reflexive to ≈reflexive;
                         refl to ≈refl; sym to ≈sym; trans to ≈trans)
 infixl 2 _≈∘_

 _≈∘_ :  Rel (A → B) _
 f ≈∘ g =  (x : A) → f x ≈ g x

 ≈∘refl : Reflexive _≈∘_
 ≈∘refl _ = ≈refl

 ≈∘reflexive : _≡_ ⇒ _≈∘_
 ≈∘reflexive {x} refl =  ≈∘refl {x}

 ≈∘sym : Symmetric _≈∘_
 ≈∘sym f≈∘g =  ≈sym ∘ f≈∘g

 ≈∘trans : Transitive _≈∘_
 ≈∘trans f≈∘g g≈∘h x =  ≈trans (f≈∘g x) (g≈∘h x)

 ≈∘Equiv : IsEquivalence _≈∘_
 ≈∘Equiv = record{ refl  = \{x}         → ≈∘refl {x}
                 ; sym   = \{x} {y}     → ≈∘sym {x} {y}
                 ; trans = \{x} {y} {z} → ≈∘trans {x} {y} {z} }

 ≈∘Setoid : Setoid (α ⊔ β) (α ⊔ β=)
 ≈∘Setoid = record{ Carrier       = A → B
                  ; _≈_           = _≈∘_
                  ; isEquivalence = ≈∘Equiv }

 lSetoid = ListPoint.setoid S

 open Setoid lSetoid using () renaming (_≈_ to _=l_; refl to =l-refl)

 gen-map-cong : {f g : A → B} → f ≈∘ g → (xs : List A) →
                                                    map f xs =l map g xs
 gen-map-cong _    []       =  =l-refl
 gen-map-cong f≈∘g (x ∷ xs) =  (f≈∘g x) ∷p (gen-map-cong f≈∘g xs)

 ...
----------------------------------------------------------


Regards,

------
Sergei