[Agda] Function.Equivalence._⇔_

[Sergei Meshveliani]

To my 
>>     _←→_ A B =  (A → B) × (B → A)
>> 
>> [..]
>> But something equivalent is expected to be in Standard library.

Nils responds 

> Function.Equivalence._⇔_.

I manage to build a value in  A ⇔ B  by applying the function  Equiv.equivalence.
But, for example, having 
                  e  :  m≤n ⇔ suc-m≤suc-n

how to extract    to :  m ≤ n → suc m ≤ suc n
from  e  ?

Thanks,

------
Sergei