We first recall some *coalgebraic* aspects of recursion theory, as set out by Paul Taylor in his book.

We assume throughout that $C$ is a category with pullbacks, and that $P: C \to C$ is an endofunctor with the property that $P$ preserves pullback squares of the form

$\array{
A & \to & B \\
\downarrow & & \downarrow \\
C & \underset{i}{\to} & D
}$

where $i$ is monic. This implies that $P$ preserves monos in particular and also intersections of subobjects.

We define $P$-algebras and $P$-coalgebras and morphisms of such in the usual way.

Let $\theta: X \to P X$ be a $P$-coalgebra structure on $X$. A subobject $i: U \hookrightarrow X$ in $C$ is ($\theta$-)**inductive** if in the pullback

$\array{
H & \stackrel{j}{\to} & X \\
\downarrow & & \downarrow^\mathrlap{\theta} \\
P U & \underset{P i}{\to} & P X
}$

the map $j$ factors through $i$ (note that $j$ is monic since $P$ preserves monos). Equivalently, that for every commutative square as above (not necessarily a pullback square), $j$ factors through $i$. A coalgebra $(X, \theta)$ is **well-founded** if the only inductive subobject of $X$ is $X$ itself.

**Example:**Suppose $X$ is an initial algebra for the endofunctor $P$, with algebra structure map $\alpha: P X \to X$. By Lambek’s theorem, $\alpha$ is invertible, so that $X$ carries a coalgebra structure $\theta = \alpha^{-1}: X \to P X$. It is easy to check that an inductive subobject gives a subalgebra $i: U \to X$, but a subalgebra of an initial algebra must be the initial algebra itself. Hence $(X, \theta)$ is well-founded.

**(Taylor)** If $(X, \theta: X \to P X)$ is a well-founded $P$-coalgebra and $\theta$ is an isomorphism, then $(X, \theta^{-1}: P X \to X)$ is an initial algebra.

The proof may be found in section 6.3 of Taylor’s book Practical Foundations of Mathematics.

The pullback of an inductive subobject $j: V \hookrightarrow Y$ along a coalgebra map $f: X \to Y$ is an inductive subobject $i: U \to X$.

Let $\theta_X: X \to P X$ and $\theta_Y: Y \to P Y$ be the coalgebra structures. Given a commutative square

$\array{
H & \to & X \\
\downarrow & & \downarrow \mathrlap{\theta_X} \\
P U & \underset{P i}{\to} & P X
}$

we must show that the top arrow factors through $i: U \to X$. Since $i: U \to X$ is formed by pulling back $j: V \to Y$ along $f: X \to Y$, it suffices to produce a map $H \to V$ that fits into a commutative square

$\array{
H & \to & X \\
\downarrow & & \downarrow \mathrlap{f} \\
V & \underset{j}{\to} & Y
}$

Gluing together the commutative squares

$\array{
H & \to & X \\
\downarrow & & \downarrow \mathrlap{\theta_X} \\
P U & \stackrel{P i}{\to} & P X \\
\downarrow & & \downarrow \mathrlap{P f} \\
P V & \underset{P j}{\to} & P Y
}$

and using the fact that $f$ is a coalgebra map, we may form a map from $H$ to the pullback $J$ of $\theta_Y$ and $P j$:

$\array{
H & \to & X \\
\downarrow & & \downarrow \mathrlap{f} \\
J & \to & Y \\
\downarrow & & \downarrow \mathrlap{\theta_Y} \\
P V & \underset{P j}{\to} & P Y
}$

and now using the fact that $j: V \to Y$ is an inductive subobject, the map $J \to Y$ factors as a map $k: J \to V$ followed by $j: V \to Y$. The map $H \to J$ followed by $k: J \to V$ gives us the desired $H \to V$.

If a coalgebra $(W, \theta: W \to P W)$ is well-founded, then so is the coalgebra $(P W, P \theta)$.

We must prove that any inductive subobject $i: U \to P W$ is the entirety of $P W$. The map $\theta$ is a coalgebra map, so by lemma , the map $j: J \to W$ formed by the pullback

$\array{
J & \stackrel{j}{\to} & W \\
\downarrow & & \downarrow \mathrlap{\theta} \\
U & \underset{i}{\to} & P W
}$

is an inductive subobject. Since $W$ is well-founded, $j$ is an isomorphism. Applying $P$ to this pullback, we have a commutative square

$\array{
P J & \stackrel{P j}{\to} & P W \\
\downarrow & & \downarrow \mathrlap{P\theta} \\
P U & \underset{P i}{\to} & P P W
}$

but because $i: U \to P W$ is inductive, the map $P j: P J \to P W$ factors through $i: U \to P W$. Since $P j$ is an iso, $i$ is forced to be a monic retraction, and thus an iso itself, as was to be proved.

For the next lemma, assume the category $C$ is locally cartesian closed.

A small colimit of well-founded coalgebras (in the category of coalgebras) is again well-founded.

Notice that the underlying functor $Coalg_P \to C$ preserves and reflects colimits. Let $W = colim_\alpha W_\alpha$ be such a colimit, and let $i: U \to W$ be an inductive subobject. The pullbacks $i_\alpha: U_\alpha \to W_\alpha$ along the coalgebra maps $W_\alpha \to W$ are again inductive subobjects, and thus isomorphisms since the $W_\alpha$ are well-founded. We have $U = colim_\alpha U_\alpha$ since colimits are stable under pullback (by local cartesian closure), and the induced comparison map $i: U \to W$ between colimits in $C$ is an isomorphism since the $i_\alpha$ are. Thus $W$ is well-founded.

Suppose $C$ is well-powered, locally cartesian closed, and admits small coproducts and coequalizers of congruences. Suppose there exists a $P$-fixpoint $(X, \theta: X \cong P X)$ (e.g., a terminal $P$-coalgebra). Then there exists an initial $P$-algebra, and this is embedded in $X$.

Under the colimit conditions on $C$, we may form unions of subobjects, and so subobject lattices are small and small-cocomplete. By lemma , the union $W$ of all well-founded subcoalgebras of $X$ is again a well-founded coalgebra; it is thus the maximal well-founded subcoalgebra. We claim this is the initial $P$-algebra.

Indeed, by theorem , it suffices to show that the coalgebra structure $\eta: W \to P W$ is an isomorphism. From the diagram

$\array{
W & \stackrel{i}{\hookrightarrow} & X \\
\mathllap{\eta} \downarrow & & \downarrow \mathrlap{\stackrel{\cong}{\theta}} \\
P W & \underset{P i}{\hookrightarrow} & P X
}$

we see $\eta$ is monic. The map $P i$ is also monic since $P$ preserves monos. From lemma , the subcoalgebra $P W$ is well-founded. It therefore contains and is contained in the maximal $W$, so that $\eta$ is an isomorphism, as desired.

For $C$ a locally cartesian closed category, and $f: B \to A$ a morphism of $C$, recall that the **polynomial endofunctor** $P_f: C \to C$ is defined to be the composite

$C \stackrel{B^\ast}{\to} C/B \stackrel{\Pi_f}{\to} C/A \stackrel{\Sigma_A}{\to} C.$

A **$W$-type** is an initial algebra $W(f)$ of a polynomial endofunctor $P_f$.

Let $C$ be a well-powered infinitary $\Pi$-pretopos. Then $C$ has all $W$-types.

In the first place, $C$ is complete. For that, it suffices to show it has all small products (since it is already finitely complete and thus has equalizers).

Let $B_i$ be a collection of objects of $C$ indexed over a set $I$. Since $C$ has small coproducts by asumption, we have a map in $C$,

$p: \sum_{i \in I} B_i \to \Delta I,$

where $\Delta I = \sum_{i \in I} 1$, and where $p$ sends the summand $B_i$ to $i$ (the $i^{th}$ copy of $1$). Then

$\prod_{i \in I} B_i = \Pi_! p$

is the product, where $!$ is the unique map $\Delta I \to 1$. Indeed, maps $X \to \Pi_! p$ are in natural bijection with maps $!^\ast X \to p$ in $E/\Delta(I) \simeq E^I$ (this equivalence holds by infinite extensivity), i.e., with an $I$-indexed family of maps $X \to B_i$, as required.

Now let $f: B \to A$ be a morphism of $C$, and $P_f$ the associated polynomial endofunctor. Since $C$ is complete, we may form the limit of the countable chain

$\ldots \to (P_f)^{n+1}(1) \stackrel{(P_f)^n !}{\to} (P_f)^n(1) \to \ldots \to P_f (1) \stackrel{!}{\to} 1.$

Moreover, $P_f$ preserves this limit because (a) this is a connected limit, and (b) the functors $B^\ast$, $\Pi_f$, and $\Sigma_A$ all preserve connected limits. It follows from Adámek’s theorem that the limit $X$, with coalgebra structure $X \to P_f X$ the isomorphism that obtains by the limit preservation by $P_f$, is a terminal coalgebra.

It now follows from theorem that there is an initial algebra $W(f)$ for $P_f$. This completes the proof.

- Paul Taylor,
*Practical Foundations of Mathematics*, Cambridge University Press, 1999.

Revised on June 11, 2022 at 16:27:52
by
Christian Sattler