Re: [TYPES] Representing inductive types with W-types

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

Does this mean that containers are "the same" as strictly positive 
functors?

Because all strictly postive functors are isomorphic to some container, 
and every container is a strictly positive functor?

On Thu, 17 Nov 2011, Altenkirch Thorsten wrote:

> Hi Russell,
>
> I think our work on containers is relevant here. You can show that any
> strictly positive functor can be represented as a container, I.e. A
> functor of the form
> F X = Sigma s:S. P s -> X where S : Set, P : S -> Set, I.e. the signature
> of a W-type.
> Actually for your example you need n-ary containers to handle nested types.
>
> The relevant results are in our '05 Journal paper
> http://www.cs.nott.ac.uk/~txa/publ/cont-tcs.pdf
> And in Michael Abbot's PhD.
>
> Recently (with Peter Morris) we extended this to dependent types, this
> appeared in LICS 2009 http://www.cs.nott.ac.uk/~txa/publ/ICont.pdf
>
> Cheers,
> Thorsten
>
> On 17/11/2011 20:57, "roconnor@..."