[Agda] A type for positive type functors?

[Dominique Devriese]

Dan,

Thanks for your comments.

2010/11/18 Dan Licata <drl at cs.cmu.edu>:
> The main problem here is that Agda does not allow you to take the fixed
> point of an arbitrary functor, but only a *strictly positive* one.  For
> example, the following definition is illegal:
>
>  data C : Set where
>    c : ((C -> Bool) -> Bool) -> C
>
> As I understand it, the motivation for this is the desire for a model in
> Sets: this datatype would be asking for a set C such that C is
> isomorphic to its double-powerset, which cannot exist for size reasons.

Yes, I understand the need for restricting fixpoint data types  to
strictly positive functors to keep the logic consistent.

> You could look at the work by Altenkrich, Morris, et al. on "containers"
> if you would like to pass around a representation of a strictly positive
> functor.

This seems interesting, but the type theory is still a bit over my
head at the moment. Thanks for the reference though.

Dominique