Inductive types

Inductive types are types which can be introduced as least fixed points of strictly positive functors.

In Martin-Löf type theory

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 (+, \times, \to). A journal version of this result has appeared in Dybjer 1997.

References

Peter Dybjer has written a series of articles on inductive types in type theory.

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}
}