[Agda] expressing iff

Nils Anders Danielsson nad at chalmers.se
Tue Apr 2 12:31:19 CEST 2013

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.


More information about the Agda mailing list