[Agda] A type for positive type functors?

[Dominique Devriese]

Thorsten,

2010/11/18 Thorsten Altenkirch <txa at cs.nott.ac.uk>:
> I just wonder how many different functions spaces we'll end up with.
>
> If one wants to quantify over functors why don't you just do that? I mean define Functor : Set1 as a record (extending RawFunctor from the library) and then show that it is closed under various operations?

I think I understand what you mean, but wouldn't this ultimately
require some form of collaboration from the positivity checker when
taking a data type fixpoint as in my EventHandlerMonad example above?

Dominique