[Agda] map⊆

[Sergei Meshveliani]

On Fri, 2014-10-10 at 18:04 +0200, Nils Anders Danielsson wrote:
> On 2014-10-10 17:44, Sergei Meshveliani wrote:
> > And I wonder of whether all this is inventing a bicycle.
> > Can  map⊆  be expressed in a simpler way?
> > What Standard library has for all this?
> 
> See Data.List.Any.Membership.map-mono, which is restricted to
> propositional equality.
> 

I am a bit confused.
I need  _⊆_ and map⊆  with respect to  _≈_ and _≈'_  of setoids

(is  Setoid._≈_  called a  definitional equality?).


I understand your answer as follows:

1)  map⊆ : (f : C → C') → (f Preserves _≈_ ⟶ _≈'_) → {xs ys : List C} →
                                        xs ⊆ ys → map f xs ⊆' map f ys
   is not close to Standard library
   (so that an user home-made implementation has sense),

2) its special case of _≡_ {A = C} and _≡_ {A = C'}  set for _≈_ and  
   _≈'_  respectively  is done by 
   Data.List.Any.Membership.map-mono.

Do I understand this correct?

Thanks,

------
Sergei