[Agda] Proposed minor additions to standard library

[Nils Anders Danielsson]

On 2010-09-14 06:12, Gregory Crosswhite wrote:
>      1) Adding a function mapDec to Relation.Nullary that allows users
>         to change between types Dec A to Dec B given maps (A -> B) and
>         (B -> A).

import Relation.Nullary.Decidable as Dec

...Dec.map...Dec.map′...

It would be good to have a Hoogle-like search engine for Agda. Is anyone
interested in implementing one?

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

I am a bit reluctant to add this module unless you have more use cases
for it.

--
/NAD