``_=ₛ_`` and ``⊆ + reverse`` for lib-2.0

[mechvel]

I suggest to add to standard library the following items.

To Data.List.Relation.Binary.Subset.Setoid:

_=ₛ_ : Rel (List A) _            -- equality of sets                            
xs =ₛ ys =  xs ⊆ ys × ys ⊆ xs    -- represented by lists                        

_≠ₛ_ : Rel (List A) _                                                           
_≠ₛ_ xs =  ¬_ ∘ _=ₛ_ xs                                                         

To Data.List.Relation.Binary.Subset.Setoid.Properties:

=ₛ-refl : Reflexive _=ₛ_                                                        
=ₛ-sym : Symmetric _=ₛ_                                                         
=ₛ-trans : Transitive _=ₛ_                                                      
=ₛ-isEquivalence : IsEquivalence _=ₛ_                                           
=ₛ-reflexive = IsEquivalence.reflexive =ₛ-isEquivalence                         

setoidₛ : Setoid a _                                                            

≟ₛ : Decidable₂ _≈_ → Decidable₂ _=ₛ_                                           

reverse-preservesʳ-⊆ :  ∀ {xs} → reverse Preserves (xs ⊆_)                      
reverse-preservesˡ-⊆ :  ∀ {xs} → reverse Preserves (_⊆ xs)                      

reverse-xs-=ₛ-xs :  ∀ xs → reverse xs =ₛ xs                                     

This is because the above items are usable.

[MatthewDaggitt]

We already have many different formalisations of this notion:

https://github.com/agda/agda-stdlib/blob/master/src/Data/List/Relation/Binary/BagAndSetEquality.agda

https://github.com/agda/agda-stdlib/blob/master/src/Data/List/Relation/Binary/Permutation/Setoid.agda

while I would welcome a proof that bidirectional subset inclusion implies these, I really don't think we want to be adding yet another relation.

[Taneb]

If we do add this new relation, I think we should name it the same as Relation.Unary._≐_, which is defined in an analogous way on predicates

[jamesmckinna]

See also the recently added (#2070 / #2071 ) https://github.com/agda/agda-stdlib/blob/master/src/Relation/Binary/Construct/Interior/Symmetric.agda It seems that what you are asking for is the instance of this construction for the $\subseteq$ preorder...

[MatthewDaggitt]

It seems that what you are asking for is the instance of this construction for the preorder...

I agreed, but I still really don't think we should add it as a first class relation, merely a proof that the construction is equivalent to the current definitions of set equality.