[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