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.

• Type: Conference
• Year: 2004
• Where: ICALP
• Authors: Michael Abbott, Thorsten Altenkirch, Neil Ghani
• Keywords: ICALP 2004, Inductive Types, Locally Cartesian Closed Category, Positive Inductive Types, Theoretical Computer Science