Re: [Agda] Function.Equivalence._⇔_
np at nicolaspouillard.fr
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
More information about the Agda