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

[Altenkirch Thorsten]

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

Cheers,
Thorsten



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

>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
>
>_______________________________________________
>Agda mailing list
>Agda at lists.chalmers.se
>https://lists.chalmers.se/mailman/listinfo/agda