[Agda] A type for positive type functors?

Dominique Devriese dominique.devriese at gmail.com
Mon Nov 22 15:42:29 CET 2010


Dan,

2010/11/18 Dan Licata <drl at cs.cmu.edu>:
> 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.

I've looked further into the containers work you (and other people in
this thread) reference, and I have the impression that the
Data.Container code in the Agda standard lib could be sufficient for
my use case.

Thanks for the help, everyone,
Dominique


More information about the Agda mailing list