nLab initial algebra of an endofunctor

Definition

An initial algebra for an endofunctor $F$ on a category $C$ is an initial object in the category of algebras of $F$. These play a role in particular as the categorical semantics for inductive types.

Properties

Relation to algebras over a monad

The concept of an algebra of an endofunctor is arguably somewhat odd, a more natural concept being that of an algebra over a monad. However, the former can often be reduced to the latter.

Proposition

If $\mathcal{C}$ is a complete category, then the category of algebras of an endofunctor $F : \mathcal{C} \to \mathcal{C}$ is equivalent to the category of algebras over a monad of the free monad on $F$, if the latter exists.

The proof is fairly straightforward, see for instance (Maciej) or at free monad.

The existence of free monads, on the other hand, can be a tricky question. One general technique is the transfinite construction of free algebras.

Lambek’s theorem

Theorem

If $F$ has an initial algebra $\alpha: F(X) \to X$, then $X$ is isomorphic to $F(X)$ via $\alpha$.

Remark

In this sense, $X$ is a fixed point of $F$. Being initial, $X$ is the smallest fixed point of $F$ in that there is a map from $X$ to any other fixed point (indeed, any other algebra), and this map is an injection if $C$ is Set.

Remark

The dual concept is terminal coalgebra, which is the largest fixed point of $F$.

Proof

Given an initial algebra structure $\alpha: F(X) \to X$, define an algebra structure on $F(X)$ to be $F(\alpha): F(F(X)) \to F(X)$. By initiality, there exists an $F$-algebra map $i: X \to F(X)$, so that

$$\array{ F(X) & \overset{F(i)}{\to} & F(F(X)) \\ \alpha \downarrow & & \downarrow F(\alpha) \\ X & \underset{i}{\to} & F(X) }$$

commutes. Now it is trivial, in fact tautological that $\alpha$ is itself an $F$-algebra map $F(X) \to X$. Thus $\alpha \circ i = 1_X$, since both sides of the equation are $F$-algebra maps $X \to X$ and $X$ is initial. As a result, $F(\alpha) \circ F(i) = 1_{F(X)}$, so that $i \circ \alpha = 1_{F(X)}$ according to the commutative square. Hence $\alpha$ is an isomorphism, with inverse $i$.

Adámek’s theorem

In many cases, initial algebras can be constructed in a recursive/iterative fashion using Adámek's fixed point theorem.

Semantics for inductive types

Initial algebras of endofunctors provide categorical semantics for extensional inductive types. The generalization to weak initial algebras captures the notion in intensional type theory and homotopy type theory.

Examples

Natural numbers

The archetypical example of an initial algebra is the set of natural numbers natural numbers object.

Proposition

Let $\mathcal{T}$ be topos and let $F : \mathcal{T} \to \mathcal{T}$ the functor given by

$$F : X \mapsto * \coprod X$$

(i.e. the functor underlying the “maybe monad”). Then an initial algebra over $F$ is precisely a natural number object $\mathbb{N}$ in $\mathcal{T}$.

Proof

By definition, an $F$-algebra is an object $X$ equipped with a morphism

$$(0,s) : * \coprod X \to X \,,$$

hence equivalently with a point $0 : * \to X$ and an endomorphism $s : X \to X$. Initiality means that for any other $F$-algebra $(0_Y, s_Y) : * \coprod Y \to Y$, there is a unique morphism $f : X \to Y$ such that the diagram

$$\array{ * &\stackrel{0}{\to}& X &\stackrel{s}{\to}& X \\ \downarrow && \downarrow^{\mathrlap{f}} && \downarrow^{\mathrlap{f}} \\ * &\stackrel{0}{\to}& Y &\stackrel{s}{\to}& Y }$$

commutes. This is the very definition of natural number object $X = \mathbb{N}$.

Bi-pointed sets

Another example of an initial algebra is the bi-pointed set $\mathbf{2}$.

Proposition

Let $\mathcal{T}$ be topos and let $F : \mathcal{T} \to \mathcal{T}$ the functor given by

$$F : X \mapsto * \coprod *$$

Then an initial algebra over $F$ is precisely a bi-pointed object $\mathbf{2}$ in $\mathcal{T}$.

More examples

Theorem applies (in particular) to any functor $F: Set \to Set$ which is a colimit of finitely representable functors $hom(n, -): X \mapsto X^n$, as in the following examples.

Example

Let $A$ be a set, and let $F: Set \to Set$ be the functor $F(X) = 1 + A \times X$. Then the initial $F$-algebra is $A^*$, the free monoid on $A$. The $F$-algebra structure is

$$(e, m| ): 1 + A \times A^* \to A^*$$

where $e: 1 \to A^*$ is the identity and $m|: A \times A^* \to A^*$ is the restriction of the monoid multiplication along the evident inclusion $i \times 1: A \times A^* \to A^* \times A^*$.

This “fixed point” of $F$ can be thought of as the result of the (slightly nonsensical) calculation

$$1 + A \times X = X \Rightarrow X = \frac1{1 - A} = 1 + A + A^2 + \ldots = A^*$$

which can be made rigorous by interpreting the initial equality as defining the solution $X$ by recursion, and applying the theorem above.

Example

Let $F: Set \to Set$ be the functor $F(X) = 1 + X^2$. Then the initial $F$-algebra is the set $T$ of isomorphism classes of finite (planar, rooted) binary trees. The $F$-algebra structure is

$$(r, j): 1 + T^2 \to T$$

where $r: 1 \to T$ names the tree consisting of just a root vertex, and $j: T^2 \to T$ creates a tree $t \vee t'$ from two trees $t$, $t'$ by joining their roots to a new root, so that the root of $t$ becomes the left child and the root of $t'$ the right child of the new root.

The recursive equation

$$T = 1 + T^2$$

would seem to imply that the structure $T$ behaves something like a structural “sixth root of unity”, and indeed the structural isomorphism $T \cong F(T)$ allows one to exhibit an isomorphism

$$T = T^7$$

constructively, as famously explored by Andreas Blass in the paper “Seven trees in one”.

Example

Let $F: Set \to Set$ be the functor $F(X) = X^*$ (the free monoid from an earlier example). Then the initial $F$-algebra is the set of isomorphism classes of finite planar rooted trees (not necessarily binary as in the previous example).

Example

Let $C$ be the coslice category $\mathbb{Z} \downarrow Ab$, and let $F: C \to C$ be the functor which pushes out along the multiplication-by-$p$ map $p \cdot -: \mathbb{Z} \to \mathbb{Z}$. Then the initial $F$-algebra is the Pruefer group $\mathbb{Z}[p^{-1}]/\mathbb{Z}$. See the discussion at the n-Category Café, starting here.

Example

Let $Ban$ be the category of complex Banach spaces and maps of norm bounded above by $1$, and let $F: \mathbb{C} \downarrow Ban \to \mathbb{C} \downarrow Ban$ be the squaring functor $X \mapsto X \times X$. Then the initial $F$-algebra is $L^1([0, 1])$ (with respect to the usual Lebesgue measure). This result is due to Tom Leinster; see this MathOverflow discussion.

Example

A list of notable endofunctors, and their initial algebras/terminal coalgebras.

Nonexistent (co)algebras are labelled with ‘/’, and unknown ones with ‘?’.

Base category	Endofunctor	Initial Algebra	Final Coalgebra	Note, reference
Set	Const $A$	$A$	$A$
Set	$X \mapsto X$	$\varnothing$	$1$
Set	$X \mapsto 1 + X$	$\mathbb{N}$	Conatural numbers $\mathbb{N}^\infty$	extended natural number
Set	$X \mapsto A + X$	$A \times \mathbb{N}$	$A \times \mathbb{N} + 1$, ie conatural numbers “terminated” (when they aren’t $\infty$) with $A$	partial map classifier
Set	$X \mapsto X + X$ or $X \mapsto 2 \times X$	$\emptyset$	$2^\mathbb{N}$ (i.e. one definition of Stream $2$)
Set	$X \mapsto A \times X$	$\emptyset$	$A^\mathbb{N}$ (i.e. one definition of Stream $A$)	sequence, writer monad, stream
Set	$X \mapsto X \times X$ or $X \mapsto [2, X]$	$\emptyset \simeq [2, \emptyset]$	1 (the unique infinite unlabelled binary tree)
Set	$X \mapsto [A, X]$	$[A, \emptyset]$	1	reader monad
Set	$X \mapsto 1 + A \times X$	List $A$	another definition of Stream $A$; i.e. potentially infinite List $A$	list, stream
Set	$X \mapsto 1 + A \times X^2$	Finite binary tree with $A$-labelled nodes	Potentially infinite binary tree with $A$-labelled nodes	tree
Set	$X \mapsto B + A \times X^n$	Finite $n$-ary tree with $A$-labelled nodes and $B$-labelled leaves	Potentially infinite $n$-ary tree with $A$-labelled nodes with and $B$-labelled leaves
Set	$X \mapsto B + A \times \text{List}(X)$	Finite tree with $A$-labelled nodes and $B$-labelled leaves	Potentially infinite tree with $A$-labelled nodes with and $B$-labelled leaves	The number of subtrees is not fixed to a particular $n$, it could be any number
Set	$X \mapsto O \times [I, X]$	$O \times [I, \emptyset]$	Potentially infinite Moore machine
Set	$X \mapsto [I, O \times X]$	$[I, \emptyset]$	Potentially infinite Mealy machine
Set	$X \mapsto \mathcal{P}(X)$	/	/
Set	$X \mapsto \mathcal{P}_{\text{fin}}(X)$	Finite rooted forests	Potentially infinite finitely-branching rooted forests
Set	polynomial endofunctor	W-type	M-type
Bipointed Sets	$X \mapsto X \vee X$	dyadic rational numbers in the interval $[0,1]$	The closed interval $[0,1] \subseteq \mathbb{R}$	coalgebra of the real interval
linearly ordered sets	$X \mapsto \omega \cdot X$, where $\omega \cdot X$ is the cartesian product of the natural numbers with the underlying set of $X$, equipped with the lexicographic order.	$\emptyset$	The non-negative real numbers $\mathbb{R}_{\geq 0}$	real number
Archimedean ordered fields	$X \mapsto X$ the identity functor	The rational numbers $\mathbb{Q}$	The real numbers $\mathbb{R}$
Archimedean ordered fields	$X \mapsto \mathcal{D}(X)$ where $\mathcal{D}(X)$ is the Archimedean ordered field of two-sided Dedekind cuts of $X$	The real numbers $\mathbb{R}$	The real numbers $\mathbb{R}$
Archimedean ordered fields	$X \mapsto \mathcal{C}(X)$ where $\mathcal{C}(X)$ is the quotient of Cauchy sequences in the Archimedean ordered field $X$	The HoTT book real numbers $\mathbb{R}_H$	The Dedekind real numbers $\mathbb{R}$	These are the same objects in the presence of excluded middle or countable choice.
Any category	The constant functor $X \mapsto A$ given object $A$	$A$	$A$
Any category	The identity functor $X \mapsto X$	initial object	terminal object
Any extensive category	$X \mapsto 1 + X$ given terminal object $1$ and coproduct $+$	natural numbers object	?
Any closed abelian category	$X \mapsto I \sqcup (A \otimes X)$ given tensor unit $I$, tensor product $\otimes$, coproduct $\sqcup$, and object $A$	tensor algebra of $A$	cofree coalgebra over $A$	tensor algebra, cofree coalgebra
$\infty$-Grpd	$X \mapsto \Sigma X$	sphere spectrum $\mathbb{S}$	?	suspension

Related entries

• list of notable initial algebras and terminal coalgebras

• inductive type

• inductive-recursive type, algebraically compact category

• higher inductive type, initial algebra of a presentable ∞-monad

References

General

• Andreas Blass, Seven Trees in One (arXiv:9405205)

A textbook account of the basic theory is in Chapter 10 of

• Steve Awodey, Category theory lecture notes (2011) (web)

The relation to free monads is discussed in

• Maciej, Free monads and their algebras

Original references on initial algebras include

• Věra Pohlová. “On sums in generalized algebraic categories.” Czechoslovak Mathematical Journal 23.2 (1973): 235-251. http://eudml.org/doc/12718.

• Jiří Adámek, Free algebras and automata realizations in the language of categories, Commentationes Mathematicae Universitatis Carolinae 15.4 (1974): 589-602.

• Jiří Adámek, Věra Trnková, Automata and algebras in categories Vol. 37. Springer Science & Business Media, 1990.

Categorical semantics of $\mathcal{W}$-types

The observation that the categorical semantics of well-founded inductive types ($\mathcal{W}$-types) is given by initial algebras over polynomial endofunctors on the type system:

• Peter Dybjer, Representing inductively defined sets by wellorderings in Martin-Löf’s type theory, Theoretical Computer Science 176 1–2 (1997) 329-335 $[$doi:10.1016/S0304-3975(96)00145-4$]$

• Ieke Moerdijk, Erik Palmgren, Wellfounded trees in categories, Annals of Pure and Applied Logic 104 1-3 (2000) 189-218 $[$doi:10.1016/S0168-0072(00)00012-9$]$

Further discussion:

• Michael Abbott, Thorsten Altenkirch, Neil Ghani, Containers: Constructing strictly positive types, Theoretical Computer Science 342 1 (2005) 3-27 $[$doi:10.1016/j.tcs.2005.06.002$]$

• Benno van den Berg, Ieke Moerdijk, $W$-types in sheaves [arXiv:0810.2398]

Generalization to inductive families (dependent $\mathcal{W}$-types):

• Nicola Gambino, Martin Hyland, Wellfounded Trees and Dependent Polynomial Functors, in: Types for Proofs and Programs TYPES 200, Lecture Notes in Computer Science 3085, Springer (2004) $[$doi:10.1007/978-3-540-24849-1_14$]$

• Michael Abbott, Thorsten Altenkirch, Neil Ghani: Representing Nested Inductive Types using W-types, in: Automata, Languages and Programming, ICALP 2004, Lecture Notes in Computer Science, 3142, Springer (2004) $[$doi:10.1007/978-3-540-27836-8_8, pdf$]$

  exposition: Inductive Types for Free – Representing nested inductive types using W-types, talk at ICALP (2004) $[$pdf$]$

Generalization to homotopy-initial algebras as categorical semantics for $\mathcal{W}$-types in homotopy type theory:

• Steve Awodey, Nicola Gambino, Kristina Sojakova, Inductive types in homotopy type theory, LICS’12: (2012) 95–104 $[$arXiv:1201.3898, doi:10.1109/LICS.2012.21, Coq code$]$

• Benno van den Berg, Ieke Moerdijk, W-types in Homotopy Type Theory, Mathematical Structures in Computer Science 25 Special Issue 5: From type theory and homotopy theory to Univalent Foundations of Mathematics (2015) 1100-1115 $[$arXiv:1307.2765, doi:10.1017/S0960129514000516$]$

• Kristina Sojakova, Higher Inductive Types as Homotopy-Initial Algebras, ACM SIGPLAN Notices 50 1 (2015) 31–42 $[$arXiv:1402.0761, doi:10.1145/2775051.2676983$]$

• Steve Awodey, Nicola Gambino, Kristina Sojakova, Homotopy-initial algebras in type theory, Journal of the ACM 63 6 (2017) 1–45 $[$arXiv:1504.05531, doi:10.1145/3006383$]$

Towards combining generalization to dependent and homotopical W-types:

• Christian Sattler, On relating indexed W-types with ordinary ones, in Types for Proofs and Programs – TYPES 2015 (2015) 71-72 $[$pdf, pdf$]$