[Agda] lists as sets

[Nils Anders Danielsson]

On 2013-12-28 19:24, Sergei Meshveliani wrote:
> For  A : Setoid α α=,  I define
>
>    C = Setoid.Carrier A
>    open Membership A using (_∈_; _⊆_)
>
>    _=set_ : Rel (List C) (α ⊔ α=)
>    xs =set ys =  xs ⊆ ys × ys ⊆ xs
>
> And then need to have the list setoid by the _=set_ equality
> (not the one of Pointwise). This will be actually a finite set setoid.
> Has Standard library something ready for this?

I suppose that Data.List.Any.Membership-≡.[_]-Equality could be
generalised to work with arbitrary underlying setoids.

-- 
/NAD