Inductive types are types which can be introduced as least fixed points of strictly positive functors.
It is often useful to extend Martin-Löf type theory with inductive types.
The can be achieved easily in an extensional type theory by adding W-types. [Dybjer 1988] shows that, in an extensional type theory, W-types can represent the least fixed points of all functors constructed from (, , ). A journal version of this result has appeared in [Dybjer 1997].
Dybjer, Peter. 1988. ‘Inductively Defined Sets in Martin-Löf’s Set Theory’. In Workshop on General Logic. University of Edinburgh.
Dybjer, Peter. 1990. ‘Inductive Sets and Families in Martin-Löf’s Type Theory and Their Set-Theoretic Semantics’. In Proceedings of the First Workshop on Logical Frameworks. Antibes. [pdf]
Dybjer, Peter. 1997. ‘Representing Inductively Defined Sets by Wellorderings in Martin-Löf’s Type Theory’. Theoretical Computer Science 176 (1–2): 329–35. https://doi.org/10.1016/S0304-3975(96)00145-4. [pdf]
@article{dybjer_1997,
title = {Representing inductively defined sets by wellorderings in {Martin}-{Löf}'s type theory},
volume = {176},
doi = {10.1016/S0304-3975(96)00145-4},
number = {1-2},
journal = {Theoretical Computer Science},
author = {Dybjer, Peter},
year = {1997},
pages = {329--335}
}