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 (denoted $\dot{U}$) describing the grammar of these functors, an interpretation function $[[\_]]$ mapping codes to functors, and a fixed point constructor.

Agda syntax

Suppose we have the the following data declaration is providided where ${\Phi }_i$ are telescopes that may refer to $T$ in a strictly positive position only.

$$\begin{array}{rl}& \mathsf{data}T:{\mathcal{U}}_1\mathsf{where}\\ & {\mathsf{c}}_1:{\Phi }_1\to T\\ & ⋮\\ & {\mathsf{c}}_n:{\Phi }_n\to T\end{array}$$

Strict positivity

Strict positivity of telescopes Suppose that we remove the requirement of strict positivity. Then an initial algebra semantics can produce inconsistent terms.

Semantics

Semantically, we interpret an inductive type as the Algebra on an Endofunctor of an endofunctor.

Let $\mathcal{C}$ be the ambient category (e.g., a locally cartesian closed category for 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.

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. See Algebra on an Endofunctor. ↩