[Agda] expressing iff

[Nils Anders Danielsson]

On 2013-04-01 01:09, Serge D. Mechveliani wrote:
> 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?

You may want to use Function.Equivalence._⇔_. However, this type is
defined as a special case of a more general definition that uses
setoids, and can be somewhat awkward to use.

-- 
/NAD