[Agda] _iff_ in lib

[Nils Anders Danielsson]

On 2013-10-24 17:17, Sergei Meshveliani wrote:
> I use
>    _←→_ : ∀ {α β} (A : Set α) → (B : Set β) → Set (α ⊔ β)
>    _←→_ A B =  (A → B) × (B → A)
>
> as the most general expression for equivalence of two statements.
> This allows to save a considerable size in the type signatures of kind
> (p → q , q → p).
>
> But something equivalent is expected to be in Standard library.

Function.Equivalence._⇔_.

-- 
/NAD