Inductive Type

Idea

In type theory, an inductive type is a way of constructing a uniform tree structure that is well-founded: all paths from the root are finite.

Inductive types can be encoded using Tarski universe. We model inductive types as the least fixed points of strictly positive endofunctors. This approach relies on a universe of codes (often denoted $U$) describing the grammar of these functors, an interpretation function $[[\_]]$ mapping codes to functors, and a fixed point constructor.

Syntax

We define the type of codes $U:{\mathcal{U}}_1$ inductively. This universe typically supports constants, the identity functor (recursive positions), sums, and products. A common minimal presentation equivalent to W-types: ¹

$$\begin{array}{rlr}\mathsf{data}& U:{\mathcal{U}}_1\mathsf{where}& \\ & \dot{\iota }:(A:\mathcal{U})\to U& \text{(Constant)}\\ & \dot{I}:U& \text{(Identity/Recursive)}\\ & \dot{\Sigma }:(A:\mathcal{U})\to (A\to U)\to U& \text{(Dependent Sum)}\\ & \dot{\Pi }:(A:\mathcal{U})\to (A\to U)\to U& \text{(Dependent Product)}\end{array}$$

A code is finitary, when $\dot{\Pi }$ is only used with finite $A$, otherwise it is infinitiary.

Interpretation

We interpret codes recursively as endofunctors $[[\_]]:U\to \mathcal{U}\to \mathcal{U}$:

$$\begin{array}{rl}[[\dot{\iota }A]]X& =A\\ [[\dot{I}]]X& =X\\ [[\dot{\Sigma }AD]]X& ={\Sigma }_{a:A}([[Da]]X)\\ [[\dot{\Pi }AD]]X& ={\Pi }_{a:A}([[Da]]X)\end{array}$$

Formation Rules

The generic inductive type $\mu D$ is the least fixed point of the functor described by $D:U$.

$$\begin{array}{rl}\mathsf{data}& \mu (D:U):{\mathcal{U}}_1\mathsf{where}\\ & \mathsf{in}:[[D]](\mu D)\to \mu D\end{array}$$ $$\frac{}{\Gamma ,D:U⊢\mu D:\mathcal{U}}$$

Introduction Rules

The type $\mu D$ has a single constructor $\mathsf{in}$, which wraps an element of the functor applied to the fixed point itself.

$$\frac{\Gamma ⊢e:[[D]](\mu D)}{\Gamma ⊢\text{in}(e):\mu D}$$

Note: The familiar constructors of specific types (like $0$ and $\mathsf{suc}$) are derived by composing $\mathsf{in}$ with the injection forms of the functor’s sum structure.

Elimination Rule

To eliminate $\mu D$ into a motive $P:\mu D\to \mathcal{U}$, we require an algebra compatible with the functor’s action on dependent types.

We define the lifting of the functor to dependent types, denoted $[[D{]]}^{♯}$. If $h:{\Pi }_{(x:\mu D)}P(x)$, then $[[D{]]}^{♯}(h)$ transforms data of type $[[D]](\mu D)$ into data over the motive.

$\frac{\Gamma ⊢\alpha :{\Pi }_{(y:[[D]](\mu D))}\left([[D{]]}^{♯}(\lambda x.P(x))y\to P(\mathsf{in}y)\right)}{\Gamma ⊢{\mathsf{ind}}_{\mu D}(\alpha ):{\Pi }_{(x:\mu D)}P(x)}$

Computation Rule

${\mathsf{ind}}_{\mu D}(\alpha ,\mathsf{in}(y))\equiv \alpha (y,[[D{]]}^{♯}({\mathsf{ind}}_{\mu D}(\alpha ))y)$

Examples

Natural Numbers

We encode $\mathbb{N}$ as a choice between a unit (zero) and a recursive position (successor). Using a binary sum operator (derived from $\sigma$ over $\mathsf{Bool}$):

$$\begin{array}{rl}\dot{\mathbb{N}}& :\equiv {\dot{\Sigma }}_2[\dot{\iota }\top ,\dot{I}]\\ \mathbb{N}& :\equiv \mu \dot{\mathbb{N}}\end{array}$$

Formation Rule

$\frac{}{\Gamma ⊢\mathbb{N}:\mathcal{U}}$

Introduction Rules

$\frac{}{\Gamma ⊢0:\mathbb{N}}\frac{\Gamma ⊢n:\mathbb{N}}{\Gamma ⊢\text{suc}(n):\mathbb{N}}$

Elimination Rule

The elimination rule asserts that to define a dependent function $f:{\prod }_{(x:\mathbb{N})}P(x)$, it suffices to define it for the constructors.

$\frac{\Gamma ,n:\mathbb{N}⊢P(n):\mathcal{U}\Gamma ⊢c_0:P(0)\Gamma ⊢c_s:{\prod }_{(n:\mathbb{N})}P(n)\to P(\text{suc}(n))}{\Gamma ⊢{\text{elim}}_{\mathbb{N}}(c_0,c_s):{\prod }_{(n:\mathbb{N})}P(n)}$

Computation Rules

Applying the eliminator to a constructor reduces to the corresponding case:

$$\begin{array}{rl}{\text{elim}}_{\mathbb{N}}(c_0,c_s,0)& \equiv c_0\\ {\text{elim}}_{\mathbb{N}}(c_0,c_s,\text{suc}(n))& \equiv c_s(n,{\text{elim}}_{\mathbb{N}}(c_0,c_s,n))\end{array}$$

Semantics

Semantically, we interpret an inductive type as the initial algebra of an endofunctor.

Let $\mathcal{C}$ be the ambient category (e.g., a locally cartesian closed category for dependent type theory). Let $F:\mathcal{C}\to \mathcal{C}$ be a strictly positive endofunctor representing the type’s signature.

F-Algebra

An F-algebra is a pair $(A,\alpha )$, where $A$ is an object in $\mathcal{C}$ and $\alpha :F(A)\to A$ is a morphism (the constructor). See Algebra (Category Theory).

Initiality

The inductive type $\mu F$ is the carrier of the initial $F$-algebra ² $(\mu F,\text{in})$. For any other algebra $(A,\alpha )$, there exists a unique homomorphism $r:\mu F\to A$ making the diagram commute: $r\circ \text{in}=\alpha \circ Fr$

• Existence of $h$ provides the recursion principle.
• Uniqueness of $h$ implies the uniqueness of the recursive definition (related to $\eta$-laws).
• Commutativity corresponds to the computation rule.

In extensional type theory, initiality corresponds exactly to the induction principle. In HoTT, we require the type to be a homotopy initial algebra. For general dependent theories, we often model these via W-types (well-founded trees), which represent the initial algebras for polynomial functors.

See also

• Inductive-Inductive Type
• Quotient Inductive Type
• W Type

References

• kaposi2019-finitary-induction-induction
• forsberg2013-inductive-inductive-thesis

Footnotes

1. from forsberg2013-inductive-inductive-thesis based on dybjer1999-inductive-recursive. ↩

2. See Initial Algebra. ↩