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 category of trees is the terminal coalgebra for the small coproduct completion (as an endofunctor on locally small categories).
The category of well-founded trees is the initial algebra for the small coproduct completion endofunctor on locally small categories.
The category of bisimulation classes of well-founded trees is the initial algebra for the small sup-cocompletion endofunctor $P$ on “locally small” (i.e., possibly large) posets.
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.
By forest, we mean simply a presheaf $F: \omega^{op} \to Set$ on the first infinite ordinal $\omega$. A tree can be understood in one of two ways:
A tree $T$ is a connected forest (meaning $\hom(T, -): Forest \to Set$ preserves arbitrary coproducts).
A tree $T$ is a forest such that $T(0)$ is terminal.
It is clear that a forest admits an essentially unique decomposition as a coproduct of trees, namely its connected components.
Let $s^\ast: Forest \to Forest$ be the pulling back (precomposing) with the successor operation $s: \omega \to \omega$:
Concretely, $s^\ast(F)(n) = F(n+1)$ gives the shift functor $s^\ast$. This clearly has a right adjoint $s_\ast: Forest \to Forest$, defined by the formula
Thus $s_\ast(G)$ is a tree for any forest $G$. The following result is almost a tautology.
The adjunction $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 $Tree$ (or $Forest$) is a fixpoint of the free small-coproduct cocompletion. In fact, we have the stronger result:
$Tree$ (or $Forest$) is the terminal coalgebra (in a 2-dimensional sense) for the free small-coproduct cocompletion endofunctor $\Sigma$ on the 2-category $CAT_{ls}$ of locally small categories.
This follows from Adámek’s theorem. For a finite number $n$, let $[n]$ be the ordinal with $n$ elements, and let $Set^{[n]^{op}}$ be the category of forests of height $n$. There is an explicit equivalence
which results from the following comma category description of $\Sigma C$: the objects of $\Sigma C$ are pairs $(X, F: X_d \to C)$ where $X$ is a set and $X_d$ is the discrete category on $X$, and morphisms $(X, F) \to (X', F')$ are pairs $(f, \Phi)$ where $f$ is a function $X \to X'$ and $\Phi$ is a natural transformation $F \to F' \circ f_d$. Letting $C$ be a (Grothendieck) topos, we may identify the category of functors $X_d \to C$ with the slice $C/\Delta X$, where $\Delta: Set \to C$ is the unique left exact left adjoint. In this way $\Sigma C$ becomes an Artin gluing construction $C \downarrow \Delta$. In the particular case where $C = Set^{D^{op}}$ is a presheaf topos, this gluing construction is equivalent to $Set^{D_{+}^{op}}$ where $D_+$ is obtained by freely adjoining a (new) initial element to $D$. This gives the equivalence (1).
Hence $\Sigma^n 1 \cong Set^{[n]^{op}}$. The sequence
is identified with the sequence
where each $i_n$ is the inclusion of an initial segment. The 2-limit of this sequence is equivalent to $Set^{\omega^{op}}$, and it is not hard to see that the canonical functor $\Sigma Set^{\omega^{op}} \to Set^{\omega^{op}}$ which obtains from the 2-limit property is identified with the obvious equivalence $Set^{\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^{\omega^{op}}$ is the terminal coalgebra.
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.
In ordinary 1-category theory, Paul Taylor introduces the concept of well-founded coalgebra as follows.
Let $C$ be a finitely complete category, and let $T$ be an endofunctor on $C$. We will suppose that $T$ 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 $T$ preserves monos. An example is the covariant power-set functor $P: Set \to Set$.
Let $\theta: X \to T X$ be a $T$-coalgebra structure on $X$. A subobject $i: U \hookrightarrow X$ in $C$ is $\theta$-inductive if in the pullback
the map $j$ factors through $i$ (note that $j$ is monic since $T$ preserves monos).
Alternatively, 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.
If $(X, \theta: X \to T X)$ is a well-founded $T$-coalgebra and $\theta$ is an isomorphism, then $(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_{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_{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 $\Sigma: CAT_{ls} \to CAT_{ls}$ preserves weak pullbacks of fully faithful functors. In particular, $\Sigma$ preserves full-faithfulness.
Let $T$ be a 2-endofunctor on $CAT_{ls}$ that preserves weak pullbacks of fully faithful functors, and let $(C, \theta: C \to T C)$ be a $T$-coalgebra. A full subcategory $i: U \hookrightarrow C$ is 2-inductive if in the pullback
the functor $j$ factors through $i$ up to isomorphism (note that $j$ is fully faithful since $T$ preserves full faithfulness).
Alternatively, that for every weakly commutative square as above (not necessarily a weak pullback), $j$ factors through $i$. A (2-)coalgebra $(C, \theta)$ is well-founded if every inductive subobject of $C$ is equivalent to $C$ itself.
If $(C, \theta: C \to T C)$ is a $T$-coalgebra and $\theta$ is an equivalence, then $C$ together with an inverse equivalence $\theta^{-1}: T C \to C$ is an initial algebra iff $(C, \theta)$ is a well-founded coalgebra.
The expectation is that the proof is a straightfoward categorification of the proof of theorem 1
We now wish to show that the category of well-founded forests (or well-founded trees) $WFF$, 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
$WFF$ is a well-founded $\Sigma$-coalgebra,
The coalgebra structure $WFF \to \Sigma (WFF)$ is an equivalence.
For this we will need some preliminaries.
The data of a forest structure can be expressed internally as a function $F \to \mathbb{N}$ together with a map
over $\mathbb{N}$, where $s^\ast F$ is the evident pullback
Committing an abuse of language, if as before we also let $s^\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 $F$ is canonically an algebra of the endofunctor $s^\ast$, with structure map $\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
which is classified by a map $F \to P s^\ast F$ in $Set^{\omega^{op}}$, where $P$ is the covariant power-object functor. In this way, every forest $F$ carries a canonical $P s^\ast$-coalgebra structure. (Morphisms of forests are actually colax $P s^\ast$-coalgebra maps.) We observe that $P s^\ast$ preserves the pulling back of monos.
A tree (or forest) $F$ is well-founded if it is well-founded as a $P s^\ast$-coalgebra.
(This definition is at the ordinary 1-categorical level, not the categorified level.)
Next, we associate to each forest $F$ a simple but fundamental category, the category of initial segments of $F$ (denoted by $\downarrow F$), whose objects are elements (nodes) $p$ of $F$, and whose morphisms $p \to q$ are maps between the trees $T_p \to T_q$ “above” the nodes $p$ and $q$. To be just a bit more formal: for each forest
there is a canonical map $F \to F_0 = F_0$, because $0$ is initial in $\omega$; this takes each node $p \in F(n)$ to the node at height $0$ (“the root”) below it. If $x: 1 \to F_0$ is an element, we define the tree above $x$ to be the pullback
considered as a subforest, in fact a connected component (a tree) of $F$. This may be generalized: for each $n \in \mathbb{N}$, let $n^\ast F$ be an abbreviation for $(s^n)^\ast F$. Each $p \in F$ may be regarded as a root of the forest $(\pi(p))^\ast F$, and we define the tree above $p$ to be
Thus we have an internal category $\downarrow F$ whose nodes are elements $p \in F$ and whose morphisms are tree maps $T_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 $Set$.
The point is that $\downarrow F$ has a $\Sigma$-coalgebra construction that matches exactly the $P s^\ast$-coalgebra construction on $F$. The functor $\downarrow F \to \Sigma(\downarrow F)$ takes a node $p \in F_n$ (or, if you prefer, the tree $T_p$) to the formal coproduct
(or, if you prefer, the formal coproduct of trees $T_q$ where $q$ ranges over immediate predecessors of $p$). This is practically the same thing as the $P s^\ast$-coalgebra structure $F \to P s^\ast F$, which takes $p \in F$ to the disjoint union
According to the way we have defined the $\Sigma$-coalgebra structure on $\downarrow F$, the full inclusion $i: \downarrow F \to Set^{\omega^{op}}$, taking $p$ to $T_p$, is a $\Sigma$-coalgebra map.
If $U$ is a 2-inductive subobject of a $\Sigma$-coalgebra $C$, then for any $\Sigma$-coalgebra map $\phi: D \to C$, the weak pullback $\phi^\ast U \hookrightarrow D$ is a 2-inductive subobject of $D$.
Suppose
commutes up to isomorphism. This is embedded in a larger diagram
and if $U$ is inductive in $C$, the map from $V$ to $C$ factors through the full inclusion $i: U \hookrightarrow C$ (up to isomorphism of course), and hence $V \to D$ factors through $\phi^\ast U \to D$. This is all we need.
Let $F$ be a forest. Then $F$ is a well-founded if and only if $\downarrow F$ is well-founded as a $\Sigma$-coalgebra.
The proof will be omitted (at least for now).
Let $C$ be a $\Sigma$-subcoalgebra of $Forest$. If every object of $C$ is a well-founded forest, then $C$ is a well-founded $\Sigma$-coalgebra.
We must show that under the hypothesis, every inductive full subcategory $U$ of $C$ is an equivalence, or that the inclusion $U \hookrightarrow C$ is essentially surjective. So, let $F$ be an arbitrary object of $C$; the hypothesis is that $F$ is well-founded, so that $i: \downarrow F \hookrightarrow C$ is a subcoalgebra that is well-founded by lemma 2. Letting $U \cap \downarrow F$ be the weak intersection; the inclusion $U \cap \downarrow F \hookrightarrow \downarrow F$ is inductive by lemma 1. Putting these two facts together, the inclusion $U \cap \downarrow F \hookrightarrow \downarrow F$ is an equivalence. But this means that $\downarrow F \hookrightarrow C$ factors through $U \hookrightarrow C$ (up to isomorphism), which in turn implies that $F$ is contained in the essential image of $U \hookrightarrow C$, as was to be shown.
The category $WFF$ is a well-founded $\Sigma$-subcoalgebra of $Set^{\omega^{op}}$.
In the first place, the composite
factors through the full inclusion $\Sigma(WFF) \to \Sigma(Set^{\omega^{op}})$; this boils down to the statement that if $F$ is a well-founded forest, then the forest
is also well-founded for any $p \in F_0$.
Thus we obtained a $\Sigma$-coalgebra structure on $WFF$, in fact a $\Sigma$-subcoalgebra of $Set^{\omega^{op}}$. It is well-founded by the previous theorem.
Now we show only that the coalgebra structure $WFF \to \Sigma (WFF)$ is an equivalence.
The coalgebra structure $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_d \to WFF)$ of $\Sigma(WFF)$, the forest $G$ defined by
with transition maps defined in the obvious way, is also well-founded. This $G$ maps to the object $(X, F)$ in $\Sigma(WFF)$, and therefore $WFF \to \Sigma(WFF)$ is essentially surjective.
$WFF$, together with an essential inverse $\Sigma(WFF) \to WFF$ to its coalgebra structure, is an initial $\Sigma$-algebra.
$WFF$ with its coalgebra structure is a $\Sigma$-fixpoint that is also well-founded as a $\Sigma$-coalgebra.
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: 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
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 $L$ equipped with a function $s: L \to L$ (called “successor”), where a (small sup)-lattice is defined to be an algebra over the monad $P_s$. The initial algebra of the endofunctor $P_s$ is the same as the initial ZF-algebra. However, ZF-algebras allow some extra generality: by adding extra assumptions on $s$, such as that $s$ 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.
Let $C$ be a category with pullbacks. Throughout this section, $P$ will be an endofunctor on $C$ that preserves inverse images of monos. In other words, we assume $P$ preserves pullback squares of the form
where $i$ is monic. This implies that $P$ preserves monos in particular and also intersections of subobjects.
We define algebras and coalgebras of $P$ and their morphisms in the usual way.
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
we must show that the top arrow factors through $i: U \to X$. Since $i$ 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
Gluing together the evident commutative squares
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$:
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 $(P W, P \theta)$.
We must prove that any inductive subobject $i: U \to P W$ is the entirety of $W$. The map $\theta$ is a coalgebra map, so by lemma 1, the map $j: J \to W$ formed by the pullback
is an inductive subobject. Since $W$ is well-founded, $j$ is an isomorphism. Applying $P$ to this pullback, we have a commutative square
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.