[Agda] Proposed minor additions to standard library

[Nils Anders Danielsson]

On 2010-09-14 19:21, Dan Doel wrote:
> 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.

That's what I thought. I think it is better to put this thing in a
dedicated library for category theory. This would make it easy to define
it as a special case of something more general.

--
/NAD