Todd Trimble Initial algebras and terminal coalgebras



Well-founded coalgebras

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

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

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

where ii is monic. This implies that PP preserves monos in particular and also intersections of subobjects.

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


Let θ:XPX\theta: X \to P X be a PP-coalgebra structure on XX. A subobject i:UXi: U \hookrightarrow X in CC is (θ\theta-)inductive if in the pullback

H j X θ PU Pi PX\array{ H & \stackrel{j}{\to} & X \\ \downarrow & & \downarrow^\mathrlap{\theta} \\ P U & \underset{P i}{\to} & P X }

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


(Taylor) If (X,θ:XPX)(X, \theta: X \to P X) is a well-founded PP-coalgebra and θ\theta is an isomorphism, then (X,θ 1:PXX)(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.

Some useful lemmas


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


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

H X θ X PU Pi PX\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:UXi: U \to X. Since i:UXi: U \to X is formed by pulling back j:VYj: V \to Y along f:XYf: X \to Y, it suffices to produce a map HVH \to V that fits into a commutative square

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

Gluing together the commutative squares

H X θ X PU Pi PX Pf PV Pj PY\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 ff is a coalgebra map, we may form a map from HH to the pullback JJ of θ Y\theta_Y and PjP j:

H X f J Y θ Y PV Pj PY\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:VYj: V \to Y is an inductive subobject, the map JYJ \to Y factors as a map k:JVk: J \to V followed by j:VYj: V \to Y. The map HJH \to J followed by k:JVk: J \to V gives us the desired HVH \to V.


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


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

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

is an inductive subobject. Since WW is well-founded, jj is an isomorphism. Applying PP to this pullback, we have a commutative square

PJ Pj PW Pθ PU Pi PPW\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:UPWi: U \to P W is inductive, the map Pj:PJPWP j: P J \to P W factors through i:UPWi: U \to P W. Since PjP j is an iso, ii is forced to be a monic retraction, and thus an iso itself, as was to be proved.

For the next lemma, assume the category CC 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 PCCoalg_P \to C preserves and reflects colimits. Let W=colim αW αW = colim_\alpha W_\alpha be such a colimit, and let i:UWi: U \to W be an inductive subobject. The pullbacks i α:U αW αi_\alpha: U_\alpha \to W_\alpha along the coalgebra maps W αWW_\alpha \to W are again inductive subobjects, and thus isomorphisms since the W αW_\alpha are well-founded. We have U=colim αU αU = colim_\alpha U_\alpha since colimits are stable under pullback (by local cartesian closure), and the induced comparison map i:UWi: U \to W between colimits in CC is an isomorphism since the i αi_\alpha are. Thus WW is well-founded.

Initial algebras inside fixpoints


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


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

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

W i X η θ PW Pi PX\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 PiP i is also monic since PP preserves monos. From lemma , the subcoalgebra PWP W is well-founded. It therefore contains and is contained in the maximal WW, so that η\eta is an isomorphism, as desired.


For CC a locally cartesian closed category, and f:BAf: B \to A a morphism of CC, recall that the polynomial endofunctor P f:CCP_f: C \to C is defined to be the composite

CB *C/BΠ fC/AΣ AC.C \stackrel{B^\ast}{\to} C/B \stackrel{\Pi_f}{\to} C/A \stackrel{\Sigma_A}{\to} C.

A WW-type is an initial algebra W(f)W(f) of a polynomial endofunctor P fP_f.


Let CC be a well-powered infinitary Π\Pi-pretopos. Then CC has all WW-types.


In the first place, CC 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 iB_i be a collection of objects of CC indexed over a set II. Since CC has small coproducts by asumption, we have a map in CC,

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

where ΔI= iI1\Delta I = \sum_{i \in I} 1, and where pp sends the summand B iB_i to ii (the i thi^{th} copy of 11). Then

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

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

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

(P f) n+1(1)(P f) n!(P f) n(1)P f(1)!1.\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 fP_f preserves this limit because (a) this is a connected limit, and (b) the functors B *B^\ast, Π f\Pi_f, and Σ A\Sigma_A all preserve connected limits. It follows from Adámek’s theorem that the limit XX, with coalgebra structure XP fXX \to P_f X the isomorphism that obtains by the limit preservation by P fP_f, is a terminal coalgebra.

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


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