[Agda] Function.Equivalence._⇔_

[Sergei Meshveliani]

On Fri, 2013-10-25 at 10:12 +0100, Martin Escardo wrote:
> 
> On 25/10/13 09:53, Nils Anders Danielsson wrote:
> > On 2013-10-24 21:43, Andrés Sicard-Ramírez wrote:
> >> foo : {A B : Set} → A ⇔ B → A → B
> >> foo h = _⟨$⟩_ (Equivalence.to h)
> >
> > In retrospect I think it was a bad idea to use setoids in so many places
> > in the standard library. I almost always use propositional equality, and
> > I prefer the setup of (parts of) my --without-K library, where I don't
> > use setoids.
> 
> The reason I can't use the standard library for my purposes is that it 
> currently doesn't work without K. A without-K library would be welcome.
> Also, I agree that the use of setoids should have been avoided.  
> [..]

1) Probably it has sense to add  _←→_ A B = (A → B) × (B → A).

2) I use a predicate  `member'  to define a subset.
   And initially I made  `member'  as a map on setoids, by using the
library construct.
But later I changed this to  member : Carrier -> Set _,
with explicit use of         congM  : member Respects _≈_.

All algebraic relations/operations respect (or are congruent by) _≈_ of
underlying setoid.
But it turns out that is is simpler to use explicitly the fields like 
congM  above than to use  _⟶_ (of setoid maps) and _⟨$⟩_. 

I suspect that generally, instead of using 
                                  _⟶_ (of setoid maps) and _⟨$⟩_  
it is better to use an ordinary maps on Carriers with adding arguments
expressing  Respects or Preserves..

3) Why to avoid at all setoids in Standard library?

For example, propositional equality on  List A  is done all right.
The things like  (map f \o map g) xs ≡ map (f \o g) xs
are useful. 
But for example, defining Setoid on  List A  from  Setoid for A  is also
useful. The same is for Maybe, and so on.
Is not it?

Regards,

------
Sergei