[Agda] Function.Equivalence._⇔_

[Nils Anders Danielsson]

On 2013-10-24 21:43, Andrés Sicard-Ramírez wrote:
> foo : {A B : Set} → A ⇔ B → A → B
> foo h = _⟨$⟩_ (Equivalence.to h)

In retrospect I think it was a bad idea to use setoids in so many places
in the standard library. I almost always use propositional equality, and
I prefer the setup of (parts of) my --without-K library, where I don't
use setoids.

-- 
/NAD