[Agda] Re: _iff_

[Serge D. Mechveliani]

To my request of

>> [..]
>> And introduce
>>                A iff' B =  (A -> B) \times (B -> A)
>> for this.
>> But can this be written in a nicer way by using Standard library?


Nils Anders Danielsson  wrote on Apr 2 2013

> You may want to use Function.Equivalence._<=>_. 

(I copy `_<=>_' from the letter on the web page).

> However, this type is defined as a special case of a more general 
> definition that uses setoids, and can be somewhat awkward to use.


Well, it works. It is what I asked for. 
I have seen  \r=  and  \l=,  and the problem was to guess to grep for 
the  \iff  math symbol in the source.

Thanks,

------
Sergei