[Agda] expressing iff

[Serge D. Mechveliani]

I meant:
as lib-0.7  has  \r=  for inclusion, may be it also has something
ready for `iff' ? -- the one that also coveres the below example.
It looks a bit strange for a user to introduce such `iff'.  
May be, Standard library needs to add such?

Thanks,

------
Sergei


On Tue, Apr 02, 2013 at 09:10:15AM +0200, Andreas Abel wrote:
> Looks fine to me. --Andreas
> 
> On 01.04.13 1:09 AM, Serge D. Mechveliani wrote:
> >Dear all,
> >I need to express a relation like
> >
> >    p x y  (: Bool)    if and only iff  f x \~~ f y   holds
> >                                                    (is not empty).
> >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?
> >
> >The code with math symbols is attached here as  t.agda.zip.
> >