5. Induction


In http://planetmath.org/node/87533Chapter 1, we introduced many ways to form new types from old ones. Except for (dependent) function types and universesPlanetmathPlanetmath, all these rules are special cases of the general notion of inductive definition. In this chapter we study inductive definitions more generally.

Title 5. InductionMathworldPlanetmath
\metatable