Chapter 5 Notes

Inductive definitions have a long pedigree in mathematics, arguably going back at least to Frege and Peano’s axioms for the natural numbers. More general “inductive predicates” are not uncommon, but in set theoretic foundations they are usually constructed explicitly, either as an intersection of an appropriate class of subsets or using transfinite iteration along the ordinals, rather than regarded as a basic notion.

In type theory, particular cases of inductive definitions date back to Martin-Löf’s original papers: [10] presents a general notion of inductively defined predicates and relations; the notion of inductive type was present (but only with instances, not as a general notion) in Martin-Löf’s first papers in type theory [8]; and then as a general notion with $\mathsf{W}$ -types in [9].

A general notion of inductive type was introduced in 1985 by Constable and Mendler [3]. A general schema for inductive types in intensional type theory was suggested in [14]. Further developments included [2],[Dybjer:1991].

The notion of inductive-recursive definition appears in [4]. An important type-theoretic notion is the notion of tree types (a general expression of the notion of Post system in type theory) which appears in [13].

The universal property of the natural numbers as an initial object of the category of $\mathbb{N}$ -algebras is due to Lawvere [6]. This was later generalized to a description of $\mathsf{W}$ -types as initial algebras for polynomial endofunctors by [11]. The coherently homotopy-theoretic equivalence between such universal properties and the corresponding induction principles (§5.4 (http://planetmath.org/54inductivetypesareinitialalgebras),§5.5 (http://planetmath.org/55homotopyinductivetypes)) is due to [1].

For actual constructions of inductive types in homotopy-theoretic semantics of type theory, see [5],[12],[7].

References

1 Awodey,Steve and Gambino,Nicola and Sojakova,Kristina. Inductive Types in Homotopy Type Theory. In emphProceedings of the 2012 27th Annual IEEE/ACM Symposium on Logic in Computer Science, pages 95–104IEEE Computer Society, .
2 Thierry Coquand and Christine Paulin. Inductively defined types. In COLOG-88 (Tallinn,1988),volume 416 of Lecture Notes in Computer Science, pages 50–66. Springer, 1990.
3 Robert L. Constable and N. P. Mendler. Recursive Definitions in Type Theory. In emphLogics of Programs,Conference,Brooklyn College,June 17–19,1985,Proceedings, pages 61–78.
4 Peter Dybjer. A general formulation of simultaneous inductive-recursive definitions in type theory. Journal of Symbolic Logic, 65:525–549 2000
5 Chris Kapulkin and Peter LeFanu Lumsdaine and Vladimir Voevodsky. The Simplicial Model of Univalent Foundations, 2012. \hrefhttp://arxiv.org/abs/1211.2851/arXiv:1211.2851.
6 F. William Lawvere. Adjointness in Foundations. Reprints in Theory and Applications of Categories, 16:1–16 2006
7 Peter LeFanu Lumsdaine and Michael Shulman. Higher inductive types. In preparation, 2013.
8 Martin-Löf,Per. An intuitionistic theory of types: predicative part. In Logic Colloquium ’73,Proceedings of the Logic Colloquium,volume 80 of Studies in Logic and the Foundations of Mathematics, pages 73–118. North-Holland, 1975.
9 Martin-Löf,Per. Constructive mathematics and computer programming. In Logic,Methodology and Philosophy of Science VI,Proceedings of the Sixth International Congress of Logic,Methodology and Philosophy of Science,Hannover 1979,volume 104 of Studies in Logic and the Foundations of Mathematics, pages 153–175. North-Holland, 1982.
10 Per Martin-Löf. Hauptsatz for the intuitionistic theory of iterated inductive definitions. In emphProceedings of the Second Scandinavian Logic Symposium (University of Oslo 1970), pages 179–216North-Holland, .
11 Moerdijk,Ieke and Palmgren,Erik. Wellfounded trees in categories. In emphProceedings of the Workshop on Proof Theory and Complexity,PTAC’98 (Aarhus), pages 189–218.
12 Ieke Moerdijk and Benno van den Berg. $W$ -types in Cartesian model categories. in preparation, 2013.
13 Kent Petersson and Dan Synek. A Set Constructor for Inductive Sets in Martin-Löf’s Type Theory. In emphCategory Theory and Computer Science,Manchester,UK,September 5–8,1989,Proceedings, pages 128–140Springer, .
14 Frank Pfenning and Christine Paulin-Mohring. Inductively defined types in the calculus of constructions. In Mathematical Foundations of Programming Semantics,5th International Conference,Tulane University,New Orleans,Louisiana,USA,March 29 – April 1,1989,Proceedings,of Lecture Notes in Computer Science, pages 209–228. Springer, 1990.

Title	Chapter 5 Notes
\metatable