The feature serves a role similar to data structures in a programming language and allows a type theory to add concepts like numbers, relations, and trees.
As the name suggests, inductive types can be self-referential, but usually only in a way that permits structural recursion.
It can be defined in Coq as follows: Here, a natural number is created either from the constant "0" or by applying the function "S" to another natural number.
"S" is the successor function which represents adding 1 to a number.
Since their introduction, inductive types have been extended to encode more and more structures, while still being predicative and supporting structural recursion.
Inductive types usually come with a function to prove properties about them.
This is the familiar induction principle for natural numbers.
[1] They generalize natural numbers, lists, binary trees, and other "tree-shaped" data types.
Given a type A : U and a dependent family B : A → U, one can form a W-type
The type A may be thought of as "labels" for the (potentially infinitely many) constructors of the inductive type being defined, whereas B indicates the (potentially infinite) arity of each constructor.
[2] Each W-type is isomorphic to the initial algebra of a so-called polynomial functor.
One may define the natural numbers as the W-type
with f : 2 → U is defined by f(12) = 0 (representing the constructor for zero, which takes no arguments), and f(22) = 1 (representing the successor function, which takes one argument).
corresponds to the constructor for the empty list, whereas the value of
corresponds to the constructor that appends a to the beginning of another list.
We can also write this rule in the style of a natural deduction proof,
The elimination rule for W-types works similarly to structural induction on trees.
In extensional type theories, W-types (resp.
M-types) can be defined up to isomorphism as initial algebras (resp.
finality) corresponds directly to the appropriate induction principle.
[3] In intensional type theories with the univalence axiom, this correspondence holds up to homotopy (propositional equality).
[4][5][6] M-types are dual to W-types, they represent coinductive (potentially infinite) data such as streams.
[8] This technique allows some definitions of multiple types that depend on each other.
For example, defining two parity predicates on natural numbers using two mutually inductive types in Coq: Induction-recursion started as a study into the limits of ITT.
Once found, the limits were turned into rules that allowed defining new inductive types.
Universe types can be defined using induction-recursion.
This is a current research area in Homotopy Type Theory (HoTT).
HoTT differs from ITT by its identity type (equality).
A simple example is the circle type, which is defined with two constructors, a basepoint; and a loop; The existence of a new constructor for the identity type makes circle a higher inductive type.