[Agda] map⊆

[Sergei Meshveliani]

On Fri, 2014-10-17 at 22:17 +0200, Nils Anders Danielsson wrote:
> On 2014-10-10 19:46, Sergei Meshveliani wrote:
> > 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),
> 
> I don't think a function of this type exists in the library.
> 
> > 2) its special case of _≡_ {A = C} and _≡_ {A = C'}  set for _≈_ and
> >     _≈'_  respectively  is done by
> >     Data.List.Any.Membership.map-mono.
> 
> Yes.
> 
> I've attached two implementations of your function, both using the
> library. One is short (not counting import statements…) and IMO not very
> readable, the other is longer, more modular, and should be easier to
> understand.
> 


I see. Thank you.
Probably it will be natural to add to Standard library some
implementation for this generic version of  map⊆.

Regards,

------
Sergei