[Agda] Function.Equivalence._⇔_

Nils Anders Danielsson nad at cse.gu.se
Fri Oct 25 10:53:00 CEST 2013

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.


More information about the Agda mailing list