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

Nicolas Pouillard np at
Fri Oct 25 09:57:11 CEST 2013

Quoting Sergei Meshveliani (2013-10-24 21:15:42)
> To my 
> >>     _←→_ A B =  (A → B) × (B → A)
> >> 
> >> [..]
> >> But something equivalent is expected to be in Standard library.
> Nils responds 
> > Function.Equivalence._⇔_.

In my extension to standard library (called [agda-nplib]), I have [three]
convenient functions to work with inverses:

* `inverses' takes the two functions and the two proofs they are inverse
  from each other.
* `_$₁_` and `_$₂_` which given an invertible function (`_ ↔ _`) and an
  argument applies the first, resp the second direction
  (As a remark, I'm not too happy about my choice of these two names).

You can either depend on this library or just include these definitions
in your own development.

If you choose to depend on it you will get all the goodness it provides
but also suffer from all the changes I make which might be non backward


Best regards,
-- NP

More information about the Agda mailing list