Sciweavers

Share
ICALP
2004
Springer

Representing Nested Inductive Types Using W-Types

10 years 4 months ago
Representing Nested Inductive Types Using W-Types
We show that strictly positive inductive types, constructed from polynomial functors, constant exponentiation and arbitrarily nested inductive types exist in any Martin-L¨of category (extensive locally cartesian closed category with W-types) by exploiting our work on container types. This generalises a result by Dybjer (1997) who showed that non-nested strictly positive inductive types can be represented using W-types. We also provide a detailed analysis of the categorical infrastructure needed to establish the result.
Michael Abbott, Thorsten Altenkirch, Neil Ghani
Added 01 Jul 2010
Updated 01 Jul 2010
Type Conference
Year 2004
Where ICALP
Authors Michael Abbott, Thorsten Altenkirch, Neil Ghani
Comments (0)
books