[Agda] Function.Equivalence._⇔_

[Nils Anders Danielsson]

On 2013-10-25 11:12, Martin Escardo wrote:
> 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?

Yes:

   http://www.cse.chalmers.se/~nad/listings/equality/README.html
   darcs get http://www.cse.chalmers.se/~nad/repos/equality/

Note that many modules in this library are parametrised by a definition
of equality:

   open import Equality

   module Bijection
     {reflexive} (eq : ∀ {a p} → Equality-with-J a p reflexive) where

   ...

I used this construction because Thierry Coquand and I wanted to make
sure that the development worked even if the computation rule for J only
holds propositionally, not definitionally. If you want to use the
regular computation rule, then you can instantiate the parameters in the
following way:

   open import Equality.Propositional
   open import Bijection equality-with-J

There are also other --without-K libraries out there. One of them may be
preferable to you.

-- 
/NAD