The Coq mailing list

[Thorsten Altenkirch <txa AT Cs.Nott.AC.UK>]

Hi Vladimir,

>> Martin-Loef''s W-type is universal for strictly positive definitions. I am 
>> not sure when W-types appeared first, they certainly feature in the 1980 
>> Sambin/Martin-Loef book. 
> 
> 
> I am not sure that it is entirely correct since "strictly positive" 
> definitions also include things such as the definition of the identity 
> types which (as far as I know) can not be encoded through W-types.

Indeed we assume that also 0,1,2,Pi,Sigma and Id is present, i.e. roughly a 
locally cartesian closed category with finite coproducts. In this theory all 
strictly positive types in the sense of Coq can be presented using W-types.

We have shown this using "containers" (basically W-algebras) first for 
non-dependent datatypes in a TCS 05 paper "Containers - Constructing Strictly 
Positive Types" (http://www.cs.nott.ac.uk/~txa/publ/cont-tcs.pdf) and then 
more recently in a paper  "Indexed Containers" (LICS 09) for dependent 
datatypes (http://www.cs.nott.ac.uk/~txa/publ/ICont.pdf). The latter uses 
indexed W-types but those can be encoded using W-types.

I should add that all this requires an extensional Type Theory, in the sense 
that the principle of extensionality is propositionally provable. However, I 
don't need K (or uniqueness of identity proofs) is used.

Cheers,
Thorsten