[Agda] expressing iff

[Serge D. Mechveliani]

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.

Thanks,

------
Sergei
-------------- next part --------------
A non-text attachment was scrubbed...
Name: t.agda.zip
Type: application/zip
Size: 461 bytes
Desc: not available
Url : http://lists.chalmers.se/pipermail/agda/attachments/20130401/c8476ab4/t.agda.zip