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

[Nicolas Pouillard]

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
compatible.

[agda-nplib]: https://github.com/crypto-agda/agda-nplib
[three]: https://github.com/crypto-agda/agda-nplib/blob/master/lib/Function/Inverse/NP.agda

Best regards,
-- NP