Induction principle (type theory)

In dependent type theory, the induction principle of a type defines the behaviour of its dependent pattern-matching and recursion analogously to the usual meaning of "induction principle" in mathematics.[cite:@hottbook]

Idea

Consider the typical induction principle of the natural numbers:

To show that a predicate $P$ holds for all natural numbers, one must

1. prove $P(0)$, and

2. prove $P(k)$ implies $P(k+1)$ for all $n\in \mathbb{N}$.

The latter proof defines a "domino effect" on the natural numbers and the former knocks down the first domino: we proved $P(0)$, which implies $P(1)$, which implies $P(2)$, ... and so on.

In type theory, this induction principle is expressed as a dependent functionIf we were to instead define ${\mathrm{ind}}_{\mathbb{N}}$ as a non-dependent function we would be left with the less powerful recursion principle.

$${\mathrm{ind}}_{\mathbb{N}}:\prod _{P:\mathbb{N}\to 𝒰}P0\to (\prod _{k:\mathbb{N}}Pk\to P(k+1))\to \prod _{n:\mathbb{N}}Pn$$

defined by the equations

The induction principle of the naturals is just one instance of a larger idea; in type theory, every inductively-defined type has an induction principle.