[Agda] _iff_ in lib

[Andreas Abel]

On 24.10.2013 17:17, Sergei Meshveliani wrote:
> 1)   _←→_ : ∀ {α β} (A : Set α) (B : Set β) → Set (α ⊔ β)
>
>       also works, despite that one `→' is forgotten,

That's right.  The arrow is only needed between non-dependent domains 
(like Bool -> Nat -> Nat as opposed to (x : Bool)(y : Nat) -> Nat) and 
before the codomain (right at the end).

> 2)   _←→_ : ∀ (α β) (A : Set α) → (B : Set β) → Set (α ⊔ β)
>
>       ("forall explicit ...")  is not type-checked.

But this works:

   ∀ α β (A : Set α) → (B : Set β) → Set (α ⊔ β)

Or:

   ∀ α β (A : Set α) (B : Set β) → Set (α ⊔ β)

Cheers,
Andreas