Todd Trimble
Some notes on the theme of well-foundedness



In these notes, I would like to write down some details on a body of related results pertaining to corecursion and recursion theory. They include (but are not limited to) the following.

The point of this exercise is not so much for these results (important though they are) as it is to develop techniques for proving these and related results. These are supposed to be test cases for a general sort of problem which for now I’ll state only very imprecisely: how to construct initial algebras of inaccessible endofunctors on accessible categories. My hunch is that in many such situations, it is technically easier to attack the problem starting from the coalgebraic end, or at least this can free us from having to consider potentially tricky set-theoretic issues involving transfinite constructions over all ordinal ranks, and work rather more cleanly and conceptually.

Most of this is inspired by Paul Taylor’s idea of understanding recursion in terms of well-founded coalgebras. These notes can be seen as a detailed application of his ideas, or rather a categorified version of his ideas, in some special cases.

Another motivation for these notes is to rewrite certain aspects of Algebraic Set Theory (about which I am hardly expert) in terms I can more readily follow. In particular, I had been reading the book by Joyal and Moerdijk, where everything seems to come together in the final chapter on construction of models; here one really sees how the smallness axioms and representability results conspire in the construction of initial ZF-algebras. In my reading, many of the core concepts in this development (open maps of forests, simulations, well-foundedness, extensionality, etc.) can be expressed directly in the coalgebraic language, and in this way are conceptually unified.

Trees as terminal coalgebra

By forest, we mean simply a presheaf F:ω opSetF: \omega^{op} \to Set on the first infinite ordinal ω\omega. A tree can be understood in one of two ways:

It is clear that a forest admits an essentially unique decomposition as a coproduct of trees, namely its connected components.

Let s *:ForestForests^\ast: Forest \to Forest be the pulling back (precomposing) with the successor operation s:ωωs: \omega \to \omega:

s *=Set s op:Set ω opSet ω ops^\ast = Set^{s^{op}}: Set ^{\omega^{op}} \to Set^{\omega^{op}}

Concretely, s *(F)(n)=F(n+1)s^\ast(F)(n) = F(n+1) gives the shift functor s *s^\ast. This clearly has a right adjoint s *:ForestForests_\ast: Forest \to Forest, defined by the formula

s *(G)(n) = G(n1) (n1) = 1 (n=0)\array{ s_\ast(G)(n) & = & G(n-1) & (n \geq 1) \\ & = & 1 & (n = 0) }

Thus s *(G)s_\ast(G) is a tree for any forest GG. The following result is almost a tautology.


The adjunction s *:TreeForest:s *s^\ast: Tree \stackrel{\leftarrow}{\to} Forest: s_\ast is an adjoint equivalence.

The category of forests is in fact the free small-coproduct completion of the category of trees, so this proposition means that TreeTree (or ForestForest) is a fixpoint of the free small-coproduct cocompletion. In fact, we have the stronger result:


TreeTree (or ForestForest) is the terminal coalgebra (in a 2-dimensional sense) for the free small-coproduct cocompletion endofunctor Σ\Sigma on the 2-category CAT lsCAT_{ls} of locally small categories.


This follows from Adámek’s theorem. For a finite number nn, let [n][n] be the ordinal with nn elements, and let Set [n] opSet^{[n]^{op}} be the category of forests of height nn. There is an explicit equivalence

Set [n+1] opΣSet [n] op(1)Set^{[n+1]^{op}} \stackrel{\sim}{\to} \Sigma Set^{[n]^{op}} \qquad (1)

which results from the following comma category description of ΣC\Sigma C: the objects of ΣC\Sigma C are pairs (X,F:X dC)(X, F: X_d \to C) where XX is a set and X dX_d is the discrete category on XX, and morphisms (X,F)(X,F)(X, F) \to (X', F') are pairs (f,Φ)(f, \Phi) where ff is a function XXX \to X' and Φ\Phi is a natural transformation FFf dF \to F' \circ f_d. Letting CC be a (Grothendieck) topos, we may identify the category of functors X dCX_d \to C with the slice C/ΔXC/\Delta X, where Δ:SetC\Delta: Set \to C is the unique left exact left adjoint. In this way ΣC\Sigma C becomes an Artin gluing construction CΔC \downarrow \Delta. In the particular case where C=Set D opC = Set^{D^{op}} is a presheaf topos, this gluing construction is equivalent to Set D + opSet^{D_{+}^{op}} where D +D_+ is obtained by freely adjoining a (new) initial element to DD. This gives the equivalence (1).

Hence Σ n1Set [n] op\Sigma^n 1 \cong Set^{[n]^{op}}. The sequence

Σ n+11Σ n!Σ n1Σ1!1\ldots \Sigma^{n+1} 1 \stackrel{\Sigma^n !}{\to} \Sigma^n 1 \to \ldots \to \Sigma 1 \stackrel{!}{\to} 1

is identified with the sequence

Set [n+1] opSet i n opSet [n] opSet1\ldots Set^{[n+1]^{op}} \stackrel{Set^{i_{n}^{op}}}{\to} Set^{[n]^{op}} \to \ldots \to Set \to 1

where each i ni_n is the inclusion of an initial segment. The 2-limit of this sequence is equivalent to Set ω opSet^{\omega^{op}}, and it is not hard to see that the canonical functor ΣSet ω opSet ω op\Sigma Set^{\omega^{op}} \to Set^{\omega^{op}} which obtains from the 2-limit property is identified with the obvious equivalence Set ω + opSet ω opSet^{\omega_{+}^{op}} \simeq Set^{\omega^{op}}, induced by the inclusion ωω +\omega \stackrel{\sim}{\to} \omega_+ as initial segment. Thus, by Adámek’s theorem, Set ω opSet^{\omega^{op}} is the terminal coalgebra.

Well-founded trees as initial algebra

The idea in this section will be to exploit a relationship between “macrocosms” of well-founded (extensional) Σ\Sigma-subcoalgebras of the category of forests, and “microcosms” which consist of individual well-founded forests.

Well-founded coalgebras

In ordinary 1-category theory, Paul Taylor introduces the concept of well-founded coalgebra as follows.

Let CC be a finitely complete category, and let TT be an endofunctor on CC. We will suppose that TT preserves pullbacks of monomorphisms (that is, it preserves limits of cospans in which one of the cospan arrows is monic). In particular, this implies that TT preserves monos. An example is the covariant power-set functor P:SetSetP: Set \to Set.


Let θ:XTX\theta: X \to T X be a TT-coalgebra structure on XX. A subobject i:UXi: U \hookrightarrow X in CC is θ\theta-inductive if in the pullback

H j X θ TU Ti TX\array{ H & \stackrel{j}{\to} & X \\ \downarrow & & \downarrow^\mathrlap{\theta} \\ T U & \underset{T i}{\to} & T X }

the map jj factors through ii (note that jj is monic since TT preserves monos).

Alternatively, 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.

Theorem 1 (Taylor)

If (X,θ:XTX)(X, \theta: X \to T X) is a well-founded TT-coalgebra and θ\theta is an isomorphism, then (X,θ 1:TXX)(X, \theta^{-1}: T X \to X) is an initial algebra.

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


Now we categorify the results of the preceding subsection so as to apply to the context of 2-categories, at least in the special case CAT lsCAT_{ls} (locally small, but not necessarily small, categories). The role of “mono” will be played by fully faithful functors (so in effect, we are considering a factorization system on CAT lsCAT_{ls} given by essentially surjective functors followed by fully faithful functors). 1-pullbacks are categorified to weak pullbacks. Observe that the weak pullback of a fully faithful functor along any functor is again fully faithful.


The small-coproduct completion functor Σ:CAT lsCAT ls\Sigma: CAT_{ls} \to CAT_{ls} preserves weak pullbacks of fully faithful functors. In particular, Σ\Sigma preserves full-faithfulness.


Let TT be a 2-endofunctor on CAT lsCAT_{ls} that preserves weak pullbacks of fully faithful functors, and let (C,θ:CTC)(C, \theta: C \to T C) be a TT-coalgebra. A full subcategory i:UCi: U \hookrightarrow C is 2-inductive if in the pullback

H j C θ TU Ti TC\array{ H & \stackrel{j}{\to} & C \\ \downarrow & & \downarrow^\mathrlap{\theta} \\ T U & \underset{T i}{\to} & T C }

the functor jj factors through ii up to isomorphism (note that jj is fully faithful since TT preserves full faithfulness).

Alternatively, that for every weakly commutative square as above (not necessarily a weak pullback), jj factors through ii. A (2-)coalgebra (C,θ)(C, \theta) is well-founded if every inductive subobject of CC is equivalent to CC itself.


If (C,θ:CTC)(C, \theta: C \to T C) is a TT-coalgebra and θ\theta is an equivalence, then CC together with an inverse equivalence θ 1:TCC\theta^{-1}: T C \to C is an initial algebra iff (C,θ)(C, \theta) is a well-founded coalgebra.

The expectation is that the proof is a straightfoward categorification of the proof of theorem 1

WFFWFF as initial Σ\Sigma-algebra

We now wish to show that the category of well-founded forests (or well-founded trees) WFFWFF, as a full subcategory of the category of forests, is an initial algebra of the free small-coproduct completion Σ\Sigma. In particular, we will need that

For this we will need some preliminaries.

Forests as coalgebras

The data of a forest structure can be expressed internally as a function FF \to \mathbb{N} together with a map

α:s *FF\alpha: s^\ast F \to F

over \mathbb{N}, where s *Fs^\ast F is the evident pullback

s *F F s \array{ s^\ast F & \to & F \\ \downarrow & & \downarrow \\ \mathbb{N} & \underset{s}{\to} & \mathbb{N} }

Committing an abuse of language, if as before we also let s *=Set s op:Set ω opSet ω ops^\ast = Set^{s^{op}}: Set^{\omega^{op}} \to Set^{\omega^{op}} be the pulling back along the successor map ωω\omega \to \omega, then every forest FF is canonically an algebra of the endofunctor s *s^\ast, with structure map α:s *FF\alpha: s^\ast F \to F as before (but now seen as a map between presheaves over ω\omega). The graph of this map is a subobject

EF×s *FE \hookrightarrow F \times s^\ast F

which is classified by a map FPs *FF \to P s^\ast F in Set ω opSet^{\omega^{op}}, where PP is the covariant power-object functor. In this way, every forest FF carries a canonical Ps *P s^\ast-coalgebra structure. (Morphisms of forests are actually colax Ps *P s^\ast-coalgebra maps.) We observe that Ps *P s^\ast preserves the pulling back of monos.


A tree (or forest) FF is well-founded if it is well-founded as a Ps *P s^\ast-coalgebra.

(This definition is at the ordinary 1-categorical level, not the categorified level.)

Category of initial segments

Next, we associate to each forest FF a simple but fundamental category, the category of initial segments of FF (denoted by F\downarrow F), whose objects are elements (nodes) pp of FF, and whose morphisms pqp \to q are maps between the trees T pT qT_p \to T_q “above” the nodes pp and qq. To be just a bit more formal: for each forest

(π:F,s *FF)(\pi: F \to \mathbb{N}, s^\ast F \to F)

there is a canonical map FF 0=F 0F \to F_0 = F_0, because 00 is initial in ω\omega; this takes each node pF(n)p \in F(n) to the node at height 00 (“the root”) below it. If x:1F 0x: 1 \to F_0 is an element, we define the tree above xx to be the pullback

T x F 1 x F 0\array{ T_x & \to & F \\ \downarrow & & \downarrow \\ 1 & \underset{x}{\to} & F_0 }

considered as a subforest, in fact a connected component (a tree) of FF. This may be generalized: for each nn \in \mathbb{N}, let n *Fn^\ast F be an abbreviation for (s n) *F(s^n)^\ast F. Each pFp \in F may be regarded as a root of the forest (π(p)) *F(\pi(p))^\ast F, and we define the tree above pp to be

T p(π(p) *F) p.T_p \coloneqq (\pi(p)^\ast F)_p.

Thus we have an internal category F\downarrow F whose nodes are elements pFp \in F and whose morphisms are tree maps T pT qT_p \to T_q. This entire construction can be expressed in the internal language of ETCS, or indeed in the Mitchell-Bénabou language of a general topos in place of SetSet.

The point is that F\downarrow F has a Σ\Sigma-coalgebra construction that matches exactly the Ps *P s^\ast-coalgebra construction on FF. The functor FΣ(F)\downarrow F \to \Sigma(\downarrow F) takes a node pF np \in F_n (or, if you prefer, the tree T pT_p) to the formal coproduct

F(n+1n)(q)=pq\sum_{F(n+1 \geq n)(q) = p} q

(or, if you prefer, the formal coproduct of trees T qT_q where qq ranges over immediate predecessors of pp). This is practically the same thing as the Ps *P s^\ast-coalgebra structure FPs *FF \to P s^\ast F, which takes pFp \in F to the disjoint union

F(n+1n)(q)=p{q}.\bigvee_{F(n+1 \geq n)(q) = p} \{q\}.

According to the way we have defined the Σ\Sigma-coalgebra structure on F\downarrow F, the full inclusion i:FSet ω opi: \downarrow F \to Set^{\omega^{op}}, taking pp to T pT_p, is a Σ\Sigma-coalgebra map.

Well-foundedness of initial segments


If UU is a 2-inductive subobject of a Σ\Sigma-coalgebra CC, then for any Σ\Sigma-coalgebra map ϕ:DC\phi: D \to C, the weak pullback ϕ *UD\phi^\ast U \hookrightarrow D is a 2-inductive subobject of DD.



V D θ D Σ(ϕ *U) ΣD\array{ V & \to & D \\ \downarrow & & \downarrow^\mathrlap{\theta_D} \\ \Sigma(\phi^\ast U) & \to & \Sigma D }

commutes up to isomorphism. This is embedded in a larger diagram

V D θ D ϕ Σ(ϕ *U) ΣD C Σϕ θ C ΣU Σi ΣC\array{ V & \to & D & & \\ \downarrow & & \downarrow^\mathrlap{\theta_D} & \searrow^\mathrlap{\phi} & \\ \Sigma(\phi^\ast U) & \to & \Sigma D & & C \\ & \searrow & & \searrow^\mathrlap{\Sigma\phi} & \downarrow^\mathrlap{\theta_C} & \\ & & \Sigma U & \underset{\Sigma i}{\to} & \Sigma C }

and if UU is inductive in CC, the map from VV to CC factors through the full inclusion i:UCi: U \hookrightarrow C (up to isomorphism of course), and hence VDV \to D factors through ϕ *UD\phi^\ast U \to D. This is all we need.


Let FF be a forest. Then FF is a well-founded if and only if F\downarrow F is well-founded as a Σ\Sigma-coalgebra.

The proof will be omitted (at least for now).


Let CC be a Σ\Sigma-subcoalgebra of ForestForest. If every object of CC is a well-founded forest, then CC is a well-founded Σ\Sigma-coalgebra.


We must show that under the hypothesis, every inductive full subcategory UU of CC is an equivalence, or that the inclusion UCU \hookrightarrow C is essentially surjective. So, let FF be an arbitrary object of CC; the hypothesis is that FF is well-founded, so that i:FCi: \downarrow F \hookrightarrow C is a subcoalgebra that is well-founded by lemma 2. Letting UFU \cap \downarrow F be the weak intersection; the inclusion UFFU \cap \downarrow F \hookrightarrow \downarrow F is inductive by lemma 1. Putting these two facts together, the inclusion UFFU \cap \downarrow F \hookrightarrow \downarrow F is an equivalence. But this means that FC\downarrow F \hookrightarrow C factors through UCU \hookrightarrow C (up to isomorphism), which in turn implies that FF is contained in the essential image of UCU \hookrightarrow C, as was to be shown.


The category WFFWFF is a well-founded Σ\Sigma-subcoalgebra of Set ω opSet^{\omega^{op}}.


In the first place, the composite

WFFffSet ω opΣ(Set ω op)(2)WFF \stackrel{ff}{\hookrightarrow} Set^{\omega^{op}} \stackrel{\sim}{\to} \Sigma(Set^{\omega^{op}}) \qquad (2)

factors through the full inclusion Σ(WFF)Σ(Set ω op)\Sigma(WFF) \to \Sigma(Set^{\omega^{op}}); this boils down to the statement that if FF is a well-founded forest, then the forest

F(10)(q)=pT q\sum_{F(1 \geq 0)(q) = p} T_q

is also well-founded for any pF 0p \in F_0.

Thus we obtained a Σ\Sigma-coalgebra structure on WFFWFF, in fact a Σ\Sigma-subcoalgebra of Set ω opSet^{\omega^{op}}. It is well-founded by the previous theorem.

WFFWFF is a Σ\Sigma-fixpoint

Now we show only that the coalgebra structure WFFΣ(WFF)WFF \to \Sigma (WFF) is an equivalence.

The coalgebra structure WFFΣ(WFF)WFF \to \Sigma(WFF) is evidently full and faithful (since the composite in (2) is fully faithful). Thus we have only to show that it is essentially surjective.

However, this is clear: given an object (X,F:X dWFF)(X, F: X_d \to WFF) of Σ(WFF)\Sigma(WFF), the forest GG defined by

G 0=X,G n+1= x:XF(x) n,G_0 = X, \qquad G_{n+1} = \sum_{x: X} F(x)_n,

with transition maps defined in the obvious way, is also well-founded. This GG maps to the object (X,F)(X, F) in Σ(WFF)\Sigma(WFF), and therefore WFFΣ(WFF)WFF \to \Sigma(WFF) is essentially surjective.


WFFWFF, together with an essential inverse Σ(WFF)WFF\Sigma(WFF) \to WFF to its coalgebra structure, is an initial Σ\Sigma-algebra.


WFFWFF with its coalgebra structure is a Σ\Sigma-fixpoint that is also well-founded as a Σ\Sigma-coalgebra.

Junk from a prior revision

I am particularly interested in understanding better what is really going on in the chapter on Existence Theorems in AST, or at least try to develop it along clean (co)algebraic lines. The object is to construct initial ZF-structures of various kinds (with a successor, with a monotone successor, etc.) from the structure of a (Heyting) pretopos with a suitable notion of small map. One could think of the pretopos as a category of “classes”, and small maps as a function f:XYf: X \to Y between classes with small fibers, and the object is to construct, for example, a cumulative hierarchy out of this data.

The basic picture is more or less clear: a set as conceived in a material theory of well-founded sets is, by the extensionality and foundation axioms, completely determined by its membership tree. So, one could think of the structure of a material set as that of a well-founded tree. Except: trees must be identified according to the extensionality axiom; for example, we have the equality between sets

{a,a,b,c}={a,b,c,c}\{a, a, b, c\} = \{a, b, c, c\}

where each side of the set equation is a tree formed by attaching a root to the disjoint union of four trees. Such equations are closely related to the notions of simulation and bisimulation, so that the cumulative hierarchy may be constructed or construed as the class of bisimulation-equivalence classes of well-founded trees, and inclusions between such classes are given by simulations.

The last line is really a take-off point for algebraic set theory, or at least the AST approach to the cumulative hierarchy. For instance, the standard ZF axioms are shown to hold for the initial algebra of the small sup-cocompletion.

Remark: Joyal and Moerdijk actually have a more flexible approach: they define a ZF-algebra as a (small sup)-lattice LL equipped with a function s:LLs: L \to L (called “successor”), where a (small sup)-lattice is defined to be an algebra over the monad P sP_s. The initial algebra of the endofunctor P sP_s is the same as the initial ZF-algebra. However, ZF-algebras allow some extra generality: by adding extra assumptions on ss, such as that ss is monotone, or inflationary, etc., they are able to account for other classes of sets as suitable initial ZF-algebras. These include various notions of ordinal that are distinguished from one another when we move to an intuitionistic setting.

Initially, the role played by simulations and bisimulations in AST was quite mysterious to me; I really don’t think the underlying intuitions were explained too well by Joyal and Moerdijk. The tack I am hoping to take is that the initial algebra for the free small sup cocompletion is obtained by localizing the initial algebra for the free small coproduct cocompletion with respect to a suitable class of maps. Well, that’s not quite right. What we do is localize the category of well-founded trees and simulations with respect to the class of surjective simulations.

But the sweet way to describe all these things is coalgebraic.

More on recursion theory

Let CC be a category with pullbacks. Throughout this section, PP will be an endofunctor on CC that preserves inverse images of monos. In other words, we assume 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 algebras and coalgebras of PP and their morphisms in the usual way.


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 ii 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 evident 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 (PW,Pθ)(P W, P \theta).


We must prove that any inductive subobject i:UPWi: U \to P W is the entirety of WW. The map θ\theta is a coalgebra map, so by lemma 1, 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.


Revised on February 14, 2013 at 18:12:00 by Todd Trimble