Re: [Agda] Function.Equivalence._⇔_

Altenkirch Thorsten psztxa at
Fri Oct 25 12:20:09 CEST 2013

I agree. Maybe it would be a worthwhile (student ?) project to revise the
standard library along those lines?


On 25/10/2013 09:53, "Nils Anders Danielsson" <nad at> wrote:

>On 2013-10-24 21:43, Andrés Sicard-Ramírez wrote:
>> foo : {A B : Set} → A ⇔ B → A → B
>> foo h = _⟨$⟩_ ( 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.
>Agda mailing list
>Agda at

More information about the Agda mailing list