# Inductive type

In type theory, a system has **inductive types** if it has facilities for creating a new type along with constants and functions that create terms of that type. 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.

The standard example is encoding the natural numbers using Peano's encoding.

```
Inductive nat : Type :=
| 0 : nat
| S : nat -> nat.
```

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. Thus, "0" is zero, "S 0" is one, "S (S 0)" is two, "S (S (S 0))" is three, and so on.

Since their introduction, inductive types have been extended to encode more and more structures, while still being predicative and supporting structural recursion.

## Contents

## Elimination

Inductive types usually come with a function to prove properties about them. Thus, "nat" may come with:

```
nat_elim : (forall P : nat -> Prop, (P 0) -> (forall n, P n -> P (S n)) -> (forall n, P n)).
```

This is the expected function for structural recursion for the type "nat".

## Implementations

### W types

W Types were well-founded types in intuitionistic type theory (ITT).

### Mutually inductive definitions

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:

```
Inductive even : nat -> Prop :=
| zero_is_even : even O
| S_of_odd_is_even : (forall n:nat, odd n -> even (S n))
with odd : nat -> Prop :=
| S_of_even_is_odd : (forall n:nat, even n -> odd (S n)).
```

### Induction-recursion

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. These types could depend upon a function and the function on the type, as long as both were defined simultaneously.

Universe types can be defined using induction-recursion.

### Induction-induction

Induction-induction allows definition of a type and a family of types at the same time. So, a type A and a family of types .

### Higher inductive types

This is a current research area in Homotopy Type Theory (HoTT). HoTT differs from ITT by its identity type (equality). Higher inductive types not only define a new type with constants and functions that create the type, but also new instances of the identity type that relate them.

A simple example is the circle type, which is defined with two constructors, a basepoint;

*base*:*circle*

and a loop;

*loop*:*base*=*base*.

The existence of a new constructor for the identity type makes circle a higher inductive type.

## See also

- Coinduction permits (effectively) infinite structures in type theory.