[Agda] Proposed minor additions to standard library

[Dan Doel]

On Tuesday 14 September 2010 6:26:57 am Nils Anders Danielsson wrote:

> Is ExpFunctor an established name?

I don't think it's very common. I had thought it originated in the paper 
Bananas in Space, but it seems I was wrong. It looks like the name was coined 
by Edward Kmett here:

  http://comonad.com/reader/2008/rotten-bananas/

which must be where I actually heard it. He notes that 'invariant functor' is 
another possible name. It's actually in the Haskell category-extras package as 
exponential functor, though:

  http://hackage.haskell.org/packages/archive/category-
extras/0.53.5/doc/html/Control-Functor-Exponential.html

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

Another example is Endo a = a -> a. Certain higher-order representations of 
lambda calculi, too. And any other case where the parameter appears on both 
sides of an exponential, of course.

-- Dan