[Agda] Proposed minor additions to standard library

[Dan Licata]

On Sep14, Nils Anders Danielsson wrote:
> >     2) Creating a module for ExpFunctors -- that is, invariant
> >        functors which can take you between F A to F B if you have
> >        maps (A -> B) and (B -> A).
> 
> Is ExpFunctor an established name? It seems as if this construction
> should be a special case of something else.

It's just a functor, but the domain category is different: a map is a
function in each direction.

Objects: types A, B, ...
Morphism from A to B: a pair A -> B and B -> A

If you required them to be mutually inverse, it would be the category of
sets and isomorphisms.  

-Dan