5.1 Introduction to inductive types

An inductive type X can be intuitively understood as a type β€œfreely generated” by a certain finite collectionMathworldPlanetmath of constructors, each of which is a function (of some number of arguments) with codomain X. This includes functions of zero arguments, which are simply elements of X.

When describing a particular inductive type, we list the constructors with bullets. For instance, the type 𝟐 from §1.8 (http://planetmath.org/18thetypeofbooleans) is inductively generated by the following constructors:

  • β€’


  • β€’


Similarly, 𝟏 is inductively generated by the constructor:

  • β€’


while 𝟎 is inductively generated by no constructors at all. An example where the constructor functions take arguments is the coproductMathworldPlanetmath A+B, which is generated by the two constructors

  • β€’


  • β€’


And an example with a constructor taking multiple arguments is the cartesian product AΓ—B, which is generated by one constructor

  • β€’


Crucially, we also allow constructors of inductive types that take arguments from the inductive type being defined. For instance, the type β„• of natural numbersMathworldPlanetmath has constructors

  • β€’


  • β€’


Another useful example is the type π–«π—‚π—Œπ—β’(A) of finite lists of elements of some type A, which has constructors

  • β€’


  • β€’


Intuitively, we should understand an inductive type as being freely generated by its constructors. That is, the elements of an inductive type are exactly what can be obtained by starting from nothing and applying the constructors repeatedly. (We will see in Β§5.8 (http://planetmath.org/58identitytypesandidentitysystems),http://planetmath.org/node/87579Chapter 6 that this conception has to be modified slightly for more general kinds of inductive definitions, but for now it is sufficient.) For instance, in the case of 𝟐, we should expect that the only elements are 0𝟐 and 1𝟐. Similarly, in the case of β„•, we should expect that every element is either 0 or obtained by applying π—Œπ—Žπ–Όπ–Ό to some β€œpreviously constructed” natural number.

Rather than assert properties such as this directly, however, we express them by means of an inductionMathworldPlanetmath principle, also called a (dependent) elimination rule. We have seen these principles already in http://planetmath.org/node/87533Chapter 1. For instance, the induction principle for 𝟐 is:

  • β€’

    When proving a statement E:πŸβ†’π’° about all inhabitants of 𝟐, it suffices to prove it for 0𝟐 and 1𝟐, i.e., to give proofs e0:E⁒(0𝟐) and e1:E⁒(1𝟐).

Furthermore, the resulting proof π—‚π—‡π–½πŸβ’(E,e0,e1):∏(b:𝟐)E⁒(b) behaves as expected when applied to the constructors 0𝟐 and 1𝟐; this principle is expressed by the computation rules:

  • β€’

    We have π—‚π—‡π–½πŸβ’(E,e0,e1,0𝟐)≑e0.

  • β€’

    We have π—‚π—‡π–½πŸβ’(E,e0,e1,1𝟐)≑e1.

Thus, the induction principle for the type 𝟐 of booleans allow us to reason by case analysis. Since neither of the two constructors takes any arguments, this is all we need for booleans.

For natural numbers, however, case analysis is generally not sufficient: in the case corresponding to the inductive step π—Œπ—Žπ–Όπ–Όβ’(n), we also want to presume that the statement being proven has already been shown for n. This gives us the following induction principle:

  • β€’

    When proving a statement E:ℕ→𝒰 about all natural numbers, it suffices to prove it for 0 and for π—Œπ—Žπ–Όπ–Όβ’(n), assuming it holds for n, i.e., we construct ez:E⁒(0) and es:∏(n:β„•)∏(y:E(n))E⁒(π—Œπ—Žπ–Όπ–Όβ’(n)).

The variable y represents our inductive hypothesis. As in the case of booleans, we also have the associated computation rules for the function 𝗂𝗇𝖽ℕ⁒(E,ez,es):∏(x:β„•)E⁒(x):

  • β€’


  • β€’

    𝗂𝗇𝖽ℕ⁒(E,ez,es,π—Œπ—Žπ–Όπ–Όβ’(n))≑es⁒(n,𝗂𝗇𝖽ℕ⁒(E,ez,es,n)) for any n:β„•.

The dependent function 𝗂𝗇𝖽ℕ⁒(E,ez,es) can thus be understood as being defined recursively on the argument x:β„•, via the functions ez and es which we call the recurrences. When x is zero, the function simply returns ez. When x is the successorMathworldPlanetmathPlanetmathPlanetmath of another natural number n, the result is obtained by taking the recurrence es and substituting the specific predecessor n and the recursive call value 𝗂𝗇𝖽ℕ⁒(E,ez,es,n).

The induction principles for all the examples mentioned above share this family resemblance. In Β§5.6 (http://planetmath.org/56thegeneralsyntaxofinductivedefinitions) we will discuss a general notion of β€œinductive definition” and how to derive an appropriate induction principle for it, but first we investigate various commonalities between inductive definitions.

For instance, we have remarked in every case in http://planetmath.org/node/87533Chapter 1 that from the induction principle we can derive a recursion principle in which the codomain is a simple type (rather than a family). Both induction and recursion principles may seem odd, since they yield only the existence of a function without seeming to characterize it uniquely. However, in fact the induction principle is strong enough also to prove its own uniqueness principle, as in the following theoremMathworldPlanetmath.

Theorem 5.1.1.

Let f,g:∏(x:N)E⁒(x) be two functions which satisfy the recurrences


up to propositional equality, i.e., such that


as well as


Then f and g are equal.


We use induction on the type family D(x):≑f(x)=g(x). For the base case, we have


For the inductive case, assume n:β„• such that f⁒(n)=g⁒(n). Then


The first and last equality follow from the assumptionsPlanetmathPlanetmath on f and g. The middle equality follows from the inductive hypothesis and the fact that application preserves equality. This gives us pointwise equality between f and g; invoking function extensionality finishes the proof. ∎

Note that the uniqueness principle applies even to functions that only satisfy the recurrences up to propositional equality, i.e.Β a path. Of course, the particular function obtained from the induction principle satisfies these recurrences judgmentally; we will return to this point in Β§5.5 (http://planetmath.org/55homotopyinductivetypes). On the other hand, the theorem itself only asserts a propositional equality between functions (see also http://planetmath.org/node/87832Exercise 5.2). From a homotopical viewpoint it is natural to ask whether this path is coherent, i.e.Β whether the equality f=g is unique up to higher paths; in Β§5.4 (http://planetmath.org/54inductivetypesareinitialalgebras) we will see that this is in fact the case.

Of course, similar uniqueness theorems for functions can generally be formulated and shown for other inductive types as well. In the next sectionPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath, we show how this uniqueness property, together with univalence, implies that an inductive type such as the natural numbers is completely characterized by its introduction, elimination, and computation rules.

Title 5.1 Introduction to inductive types