[Agda] A type for positive type functors?

[Thorsten Altenkirch]

You cannot in general construct fixpoints of arbitrary functors, e.g. FX = (X->2)->2 hasn't got an initial algebra in Type Theory.

If you want to have fixpoints you should refer to containers, i.e. S : Set, P : S -> Set which give rise to the functor FX = Sigma S (\ s -> Ps -> X). The initial algebra of a container is given by the W-type W S P.

Cheers,
Thorsten

On 19 Nov 2010, at 08:33, Dominique Devriese wrote:

> 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