[Agda] A type for positive type functors?

[Thorsten Altenkirch]

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?

Cheers,
Thorsten

On 18 Nov 2010, at 21:20, Nicolas Pouillard wrote:

> On Thu, 18 Nov 2010 19:55:07 +0100, Andreas Abel <andreas.abel at ifi.lmu.de> wrote:
>> Hi Dominique,
>> 
>> in your case, I am afraid, you have to turn off the positivity checker. 
>>  Agda checks positivity by unfolding definitions, this is why the 
>> concrete version with Maybe works.  However, if you abstract Maybe to a 
>> variable M, positivity hold only if M is positive itself.
>> 
>> Currently Agda cannot handle this.  In my toy language MiniAgda it 
>> works, because you can declare M to be strictly positive as follows:
>> 
>>   data EventHandlerMonad ++(M : Set -> Set) (E : Set) (A : Set) : Set ...
>> 
>> telling the positivity checker that M is assumed to be strictly positive 
>> and can only be instantiated with strictly positive type functions.
> 
> This would be a very nice addition to Agda! In the same vein being able to
> abstract over injective functions/constructors would be really helpful.
> 
> Actually any syntactic criterion could be equiped with a way to abstract over
> things having this criterion.
> 
> -- 
> Nicolas Pouillard
> http://nicolaspouillard.fr
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda