[Agda] Function.Equivalence._⇔_

[Martin Escardo]

On 25/10/13 09:53, Nils Anders Danielsson 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.

The reason I can't use the standard library for my purposes is that it 
currently doesn't work without K. A without-K library would be welcome.
Also, I agree that the use of setoids should have been avoided. Is your 
without-K available somewhere?

Martin