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 universes, all these rules are special cases of the general notion of inductive definition.In this chapter we study inductive definitions more generally.