Well-Founded Coalgebras Meet Kőnig’s Lemma

Urbat, Henning; Wißmann, Thorsten

doi:10.4230/LIPIcs.CSL.2026.24

Well-Founded Coalgebras Meet Kőnig’s Lemma

Henning Urbat

Friedrich-Alexander-Universität Erlangen-Nürnberg, Germany Thorsten Wißmann

Friedrich-Alexander-Universität Erlangen-Nürnberg, Germany

Abstract

Kőnig’s lemma is a fundamental result about trees with countless applications in mathematics and computer science. In contrapositive form, it states that if a tree is finitely branching and well-founded (i.e. has no infinite paths), then it is finite. We present a coalgebraic version of Kőnig’s lemma featuring two dimensions of generalization: from finitely branching trees to coalgebras for a finitary endofunctor $H$ , and from the base category of sets to a locally finitely presentable category ${\mathbb{C}}$ , such as the category of posets, nominal sets, or convex sets. Our coalgebraic Kőnig’s lemma states that, under mild assumptions on ${\mathbb{C}}$ and $H$ , every well-founded coalgebra for $H$ is the directed join of its well-founded subcoalgebras with finitely generated state space – in particular, the category of well-founded coalgebras is locally presentable. As applications, we derive versions of Kőnig’s lemma for graphs in a topos as well as for nominal and convex transition systems. Additionally, we show that the key construction underlying the proof gives rise to two simple constructions of the initial algebra (equivalently, the final recursive coalgebra) for the functor $H$ : The initial algebra is both the colimit of all well-founded and of all recursive coalgebras with finitely presentable state space. Remarkably, this result holds even in settings where well-founded coalgebras form a proper subclass of recursive ones. The first construction of the initial algebra is entirely new, while for the second one our approach yields a short and transparent new correctness proof.

Keywords and phrases:

Kőnig’s Lemma, Well-Foundedness, Coalgebra

Funding:

Henning Urbat: Deutsche Forschungsgemeinschaft (DFG, German Research Foundation) – project numbers 470467389 and 569130867.

Copyright and License:

2012 ACM Subject Classification:

Theory of computation

\rightarrow

Categorical semantics

Related Version:

Full paper with proofs in the appendix: https://arxiv.org/abs/2507.18539

Acknowledgements:

The authors thank Stefan Milius for inspiring discussions on well-founded coalgebras, and Dominik Kirst for pointing out the relevance of Kőnig’s lemma and its relatives in reverse constructive mathematics.

DOI:

10.4230/LIPIcs.CSL.2026.24

Event:

34th EACSL Annual Conference on Computer Science Logic (CSL 2026)

Editors:

Stefano Guerrini and Barbara König

Series and Publisher:

Leibniz International Proceedings in Informatics, Schloss Dagstuhl – Leibniz-Zentrum für Informatik

1 Introduction

In 1927, Dénes Kőnig [28] proved a result in graph theory, known as Kőnig’s lemma, that turned out to be of fundamental importance. In its most popular formulation, the lemma asserts that every infinite, finitely branching tree contains an infinite path. While this statement looks almost obvious (with a classical, non-constructive mindset at least), it isolates an important selection principle that appears in different shapes and forms throughout mathematics and computer science, for instance, in proofs of compactness and completeness theorems in logic [42], Ramsey theory [40], or the analysis of infinite runs and liveness properties of systems in verification [12] and automata theory [18, 22]. Kőnig’s lemma is moreover deeply tied with the foundations of set theory, specifically the axiom of countable choice [21, 24]. Variants such as the weak Kőnig’s lemma (the restriction to binary trees) and Brouwer’s fan theorem [11] have been extensively studied in (reverse) constructive mathematics and computability theory [16, 20].

Kőnig’s lemma applies to graphs, which are the simplest instance of state-based systems, that is, systems with a notion of state space and a notion of transition between states. Such systems can be uniformly modelled at categorical generality using coalgebras [23, 37]. A coalgebra is given by an endofunctor $H$ on a category ${\mathbb{C}}$ that specifies the system type, an object $C$ of ${\mathbb{C}}$ determining the state space, and a morphism $c\colon C\to HC$ determining the transition structure. By varying the base category ${\mathbb{C}}$ and the type functor $H$ , countless different incarnations of state-based systems emerge in the coalgebraic framework. For example, graphs are precisely coalgebras for the power set functor $\mathcal{P}$ on the category of sets, non-deterministic register automata [27] over an infinite alphabet $\mathds{A}$ of data values correspond to coalgebras for the functor $\{0,1\}\times\mathcal{P}^{\mathds{A}}$ on the topos of nominal sets [8] (with power object functor $\mathcal{P}$ ), and (determinized) probabilistic automata are coalgebras for a functor that involves the convex power set functor on the category of convex sets [9].

In the present work, we aim to address the following natural question:

Which coalgebras (beyond graphs) feature a Kőnig’s lemma?

To motivate our approach, let us revisit the case of graphs ( $\mathcal{P}$ -coalgebras). Note first that finitely branching graphs are precisely coalgebras for the finite power set functor $\mathcal{P}_{\omega}$ . We say that a graph is well-founded if it contains no infinite paths. Then König’s lemma can be restated, in contrapositive form and in coalgebraic terminology, as follows:

\emph{Every state of a well-founded $\mathcal{P}_{\omega}$-coalgebra lies in % some finite subcoalgebra}.

(1.1)

The initial observation towards a generalization of (1.1) is that the notion of well-foundedness is available for arbitrary coalgebras [41, 4]: A coalgebra $c\colon C\to HC$ is well-founded if it has no proper cartesian subcoalgebras (see Section 2 for details). Moreover, $\mathcal{P}_{\omega}$ is the prototypical finitary functor, that is, a functor that preserves filtered colimits. The first coalgebraic extension of Kőnig’s lemma, recently proved by Adámek, Milius, and Moss [4, Prop. 9.2.19], replaces the finite power set functor $\mathcal{P}_{\omega}$ with an arbitrary finitary set functor $H$ :

\emph{Every state of a well-founded $H$-coalgebra lies in some finite % subcoalgebra}.

(1.2)

The proof from op. cit. exploits the fact that every coalgebra $c\colon C\to HC$ for a finitary set functor can be associated with a canonical graph $\overline{c}\colon C\to\mathcal{P}_{\omega}C$ representing the transition structure of the coalgebra. In this way, (1.2) reduces to the classical Kőnig’s lemma (1.1).

The main contribution of our paper is a substantial generalization of (1.2) to coalgebras over abstract categories. This step involves two non-trivial challenges: First, canonical graphs are specific to coalgebras over the category of sets, so the reduction argument by Adámek et al. [4] no longer works. Second, it is not clear what a “finite” coalgebra is in a general category. To address these challenges, we base our theory on locally finitely presentable categories (which include, for instance, the categories of sets, nominal sets, and convex sets). The key feature of locally finitely presentable categories is that they come with two well-behaved abstract notions of “finite” object, namely finitely presentable and finitely generated objects. Finite coalgebras thus naturally generalize to coalgebras with either finitely presentable or finitely generated state space, or fp/fg-carried coalgebras for short. Our main result (Theorem 3.7) establishes Kőnig’s lemma at this level of generality:

Coalgebraic Kőnig’s Lemma.

Let ${\mathbb{C}}$ be a locally finitely presentable category with monic coproduct injections, and let $H$ be a finitary functor on ${\mathbb{C}}$ preserving binary intersections. Then every well-founded $H$ -coalgebra is the directed join of its fg-carried well-founded subcoalgebras.

In Section 4, we explore several instantiations of this result beyond the category of sets. Notably, we demonstrate that every locally finitely presentable topos features a Kőnig’s lemma for graphs, and we derive versions of Kőnig’s lemma for nominal and convex transition systems. The latter systems are infinitely branching, but their branching is finitely generated in an algebraic sense, which turns out to be enough to guarantee existence of infinite paths.

The core ingredient for our proof of the Coalgebraic Kőnig’s Lemma is a general construction on coalgebras, coproduct extension [6, 44, 32, 31], which allows to add new states to a coalgebra in a restricted way. The key observation is that coproduct extension preserves well-foundedness. This fact leads us to a further fundamental result on well-founded coalgebras, namely a new construction of the initial algebra for the functor $H$ (Theorem 5.2):

Initial Algebra Theorem.

Under the assumptions of the Coalgebraic Kőnig’s Lemma, the initial algebra for the functor $H$ is the colimit of all fp-carried well-founded coalgebras.

This theorem relates to a recent result by Wißmann and Milius [45], who showed that the initial algebra is the colimit of all fp-carried recursive coalgebras [41]. Under the assumptions of our Initial Algebra Theorem, well-founded coalgebras form a (in some instances proper) subclass of recursive ones. Thus, the Initial Algebra Theorem can be seen as an improvement of the corresponding result for recursive coalgebras because it operates with a smaller diagram, and more importantly, well-foundedness of a given coalgebra is typically much easier to prove than recursivity in settings where the two notions do not coincide. In addition, the idea underlying the proof of the Initial Algebra Theorem carries over to its recursive version and yields a transparent new proof of the latter that greatly simplifies the original argument [45].

2 Preliminaries

We start with some background on locally finitely presentable categories [7] and on well-founded and recursive coalgebras [4, 41]; see the cited textbooks for more details. Readers should be familiar with basic category theory [30], such as functors and (co)limits.

Locally Finitely Presentable Categories.

The results of our paper apply to coalgebras over locally finitely presentable categories, which are categories where every object can be approximated from below by suitably “finite” objects. For example, the category of sets is locally finitely presentable because every set is a union of finite sets, and the category of vector spaces is locally finitely presentable because every vector space is a union of finite-dimensional spaces. The categorical notion of finiteness is expressed abstractly using filtered colimits.

A category $I$ is filtered if (i) $I$ is non-empty, (ii) for any two objects $i,j\in I$ there exists a cospan $i\to k\leftarrow j$ in $I$ , and (iii) for every parallel pair $f,g\colon i\to j$ there exists a morphism $h\colon j\to k$ such that $h\circ f=h\circ g$ . For example, finitely cocomplete categories are filtered. A poset (viewed as a category) is filtered iff it is directed, i.e. every finite subset has an upper bound. A filtered diagram $D\colon I\to{\mathbb{C}}$ is a diagram whose scheme $I$ is filtered, and a filtered colimit is a colimit of a filtered diagram. A functor is finitary if it preserves filtered colimits.

Example 2.1 (Filtered Colimits in $\mathsf{Set}$ ).

In the category $\mathsf{Set}$ of sets and functions, the colimit of a filtered diagram $D\colon I\to\mathsf{Set}$ is given by $(\coprod_{i}D_{i})/{\approx}$ where $\approx$ is the equivalence relation with $(x,i)\approx(y,j)$ iff there exist morphisms $f\colon i\to k$ and $g\colon j\to k$ in $I$ such that $Df(x)=Dg(y)$ . The colimit injection $c_{i}\colon D_{i}\to(\coprod_{i}D_{i})/{\approx}$ sends $x\in D_{i}$ to the equivalence class of $(x,i)$ . An endofunctor $H$ on $\mathsf{Set}$ is finitary iff for every set $X$ and every $x\in HX$ , there exists a finite subset $m\colon M\hookrightarrow X$ such that $x\in Hm[HM]$ [5, Rem. 3.14].

An object $X$ of a category ${\mathbb{C}}$ is finitely presentable if its hom-functor ${\mathbb{C}}(X,-)\colon{\mathbb{C}}\to\mathsf{Set}$ is finitary. More explicitly, this means that given a filtered diagram $D\colon I\to{\mathbb{C}}$ with colimit cocone $(c_{i}\colon D_{i}\to C)_{i\in I}$ , every morphism from $X$ to $C$ factorizes essentially uniquely through the cocone $(c_{i})$ , that is, the following two statements hold:

1.

every morphism $f\colon X\to C$ factorizes as $f=c_{i}\circ g$ for some $i\in I$ and $g\colon X\to D_{i}$ ;
2.

for any two morphisms $g,g^{\prime}\colon X\to D_{i}$ with $i\in I$ and $c_{i}\circ g=c_{i}\circ g^{\prime}$ , there exists $k\colon i\to j$ in $I$ such that $Dk\circ g=Dk\circ g^{\prime}$ .

Besides finitely presentable objects, there is also the weaker notion of finitely generated object. An object $X$ of ${\mathbb{C}}$ is finitely generated if for every filtered diagram $D\colon I\to{\mathbb{C}}$ whose colimit cocone $(c_{i}\colon D_{i}\rightarrowtail C)_{i\in I}$ consists of monomorphisms, every morphism from $X$ to $C$ factorizes through some $c_{i}$ . (Here the essential uniqueness of the factorization comes for free because $c_{i}$ is monic.) We let ${\mathbb{C}}_{\mathrm{fp}},{\mathbb{C}}_{\mathrm{fg}}\hookrightarrow{\mathbb{C}}$ denote the full subcategories given by finitely presentable and finitely generated objects, respectively. Note that ${\mathbb{C}}_{\mathrm{fp}}\subseteq{\mathbb{C}}_{\mathrm{fg}}$ , but generally finitely presentable and finitely generated objects do not coincide.

Lemma 2.2.

The subcategories ${\mathbb{C}}_{\mathrm{fp}}$ , ${\mathbb{C}}_{\mathrm{fg}}\hookrightarrow{\mathbb{C}}$ have the following closure properties:

1.

Both ${\mathbb{C}}_{\mathrm{fp}}$ and ${\mathbb{C}}_{\mathrm{fg}}$ are closed under finite colimits [7, Prop. 1.3].
2.

${\mathbb{C}}_{\mathrm{fg}}$ is closed under strong quotients (represented by strong epimorphisms) [7, Prop. 1.69].

A category ${\mathbb{C}}$ is locally finitely presentable if it is cocomplete, and there exists a (small) set $\mathcal{A}$ of finitely presentable objects such that every object of ${\mathbb{C}}$ is a filtered colimit of objects in $\mathcal{A}$ , that is, a colimit of some filtered diagram $D\colon I\to{\mathbb{C}}$ such that $D_{i}\in\mathcal{A}$ for all $i\in I$ . Informally, this says that every object can be constructed from “finite” objects.

Example 2.3 (Locally Finitely Presentable Categories).

${\mathbb{C}}$	Objects	Morphisms	${\mathbb{C}}_{\mathrm{fp}}$ ( $={\mathbb{C}}_{\mathrm{fg}}$ )
$\mathsf{Set}$	sets	functions	finite sets
$\mathsf{Nom}$	nominal sets	equivariant maps	orbit-finite sets
$\mathsf{Conv}$	convex sets	affine maps	finitely generated convex sets

Figure 1: Locally finitely presentable categories.

In our applications (Section 4) we consider the locally finitely presentable categories of Figure 1. Their finitely presentable and finitely generated objects coincide and are described in the last column. The categories $\mathsf{Nom}$ of nominal sets and $\mathsf{Conv}$ of convex sets are discussed in more detail in Section 4.4 and Section 4.5. Let us mention that there are many more examples of locally finitely presentable categories, including all categories of algebras for an equational theory (such as monoids, rings, vector spaces), all categories of relational structures axiomatized by a finitary relational Horn theory (such as posets), and all presheaf categories $\mathsf{Set}^{\mathbb{D}}$ over a small category ${\mathbb{D}}$ [7]. In all these categories, filtered colimits are formed like in $\mathsf{Set}$ (Example 2.1).

Remark 2.4.

There is a more general notion of locally $\lambda$ -presentable category, for a regular cardinal $\lambda$ , where the role of filtered colimits is taken over by $\lambda$ -filtered colimits. Here a diagram scheme is $\lambda$ -filtered if condition (ii) in the above definition of a filtered category is strengthened to ( $\text{ii}_{\lambda}$ ): Every non-empty set of objects of cardinality less than $\lambda$ has a cospan over it. Locally finitely presentable categories correspond to the case $\lambda=\omega$ . A category is locally presentable if it is locally $\lambda$ -presentable for some $\lambda$ . An example of a locally ( $\omega_{1}$ -)presentable category that is not locally finitely presentable is the category of metric spaces and non-expansive maps. The results of our paper currently do not extend to arbitrary locally presentable categories; in fact, we use several results on well-founded coalgebras (see below) which rest on properties specific to ( $\omega$ -)filtered colimits.

Locally finitely presentable categories are, in many respects, convenient and well-behaved structures. Let us mention a few core results, whose proofs can be found in Adámek and Rosický [7] (Remark 1.56, Proposition 1.61, Proposition 1.62, Exercise 1.o).

Lemma 2.5.

Every locally finitely presentable category ${\mathbb{C}}$ is complete and well-powered, and every morphism in ${\mathbb{C}}$ has a (strong epi, mono)-factorization.

Since a locally finitely presentable category ${\mathbb{C}}$ is cocomplete and has (strong epi, mono)-factorizations, the poset $\operatorname{\mathrm{Sub}}(X)$ of subobjects of an object $X$ form a complete lattice: The join of a family of subobjects $m_{i}\colon X_{i}\rightarrowtail X$ ( $i\in I$ ) is the subobject $m\colon\bigvee_{i\in I}X_{i}\rightarrowtail X$ given by the (strong epi, mono)-factorization of the morphism $[m_{i}]_{i\in I}$ :

Directed joins of subobjects can be alternatively computed by just forming their colimit. In more detail, a directed family $m_{i}\colon X_{i}\rightarrowtail X$ ( $i\in I$ ) of subobjects can be regarded as a cocone over the directed diagram $D\colon I\to{\mathbb{C}}$ , $i\mapsto X_{i}$ , where $I$ is ordered by $i\leq j$ iff $m_{i}\leq m_{j}$ in the usual partial order of subobjects. Then the following statement holds:

Lemma 2.6.

Let ${\mathbb{C}}$ be locally finitely presentable. For any directed family $m_{i}\colon X_{i}\rightarrowtail X$ ( $i\in I$ ) of subobjects of an object $X$ , its join in $\operatorname{\mathrm{Sub}}(X)$ is the colimit of the induced diagram.

We also have a useful characterization of filtered colimits in general:

Lemma 2.7.

Let $D\colon I\to{\mathbb{C}}$ be a filtered diagram in a locally finitely presentable category ${\mathbb{C}}$ . A cocone $(c_{i}\colon D_{i}\to C)_{i\in I}$ over $D$ forms a colimit cocone iff for every $X\in{\mathbb{C}}_{\mathrm{fp}}$ , every morphism from $X$ to $C$ factorizes essentially uniquely through $(c_{i})$ .

Note that the left-to-right implication holds by the definition of a finitely presentable object. The reverse implication is the interesting part of the lemma.

Regarding finitary functors, the following result generalizing Example 2.1 applies:

Lemma 2.8 ([5, Thm. 3.4]).

Let ${\mathbb{C}}$ be a locally finitely presentable category with ${\mathbb{C}}_{\mathrm{fp}}={\mathbb{C}}_{\mathrm{fg}}$ , and let $H$ be a functor that preserves monomorphisms. Then $H$ is finitary iff for every object $X$ of ${\mathbb{C}}$ , every finitely generated subobject $s\colon S\rightarrowtail HX$ factorizes through $Hm\colon HM\rightarrowtail HX$ for some finitely generated subobject $m\colon M\rightarrowtail X$ .

This result applies, in particular, to mono-preserving functors on the categories of Figure 1.

Lastly, if a functor is not finitary, it can be canonically restricted to a finitary functor. In the following, let $[{\mathbb{C}},{\mathbb{C}}]$ denote the category of endofunctors on ${\mathbb{C}}$ and natural transformations, $[{\mathbb{C}},{\mathbb{C}}]_{\mathsf{fin}}$ its full subcategory given by finitary endofunctors, and ${\mathbb{C}}_{\mathrm{fp}}/X$ the full subcategory of the slice category ${\mathbb{C}}/X$ whose objects are morphisms $(f\colon P\to X)$ of ${\mathbb{C}}$ with $P\in{\mathbb{C}}_{\mathrm{fp}}$ .

Lemma 2.9 ([2, Cor. 2.8]).

If ${\mathbb{C}}$ is locally finitely presentable, then $[{\mathbb{C}},{\mathbb{C}}]_{\mathsf{fin}}$ is a coreflective subcategory of $[{\mathbb{C}},{\mathbb{C}}]$ . The coreflection of $H\colon{\mathbb{C}}\to{\mathbb{C}}$ is the functor $H_{\omega}\colon{\mathbb{C}}\to{\mathbb{C}}$ given by $H_{\omega}X=\operatorname{\mathsf{colim}}D_{X}$ for the diagram $D_{X}\colon{\mathbb{C}}_{\mathrm{fp}}/X\to{\mathbb{C}}$ mapping $(f\colon P\to X)\in{\mathbb{C}}_{\mathrm{fp}}/X$ to $H P$ .

The functor $H_{\omega}$ is called the finitary coreflection of $H$ . For example, the finitary coreflection of the power set functor $\mathcal{P}\colon\mathsf{Set}\to\mathsf{Set}$ is the finite power set functor $\mathcal{P}_{\omega}\colon\mathsf{Set}\to\mathsf{Set}$ .

Coalgebras and Algebras.

Coalgebras [23, 37] form a uniform categorical abstraction of state-based transition systems, such as graphs, labelled transition systems, Markov chains, and various kinds of automata. The idea is to model the state space of a system by an object of a suitable category ${\mathbb{C}}$ , and its transition type by an endofunctor on that category. Formally, a coalgebra for an endofunctor $H\colon{\mathbb{C}}\to{\mathbb{C}}$ is a pair $(C,c)$ consisting of an object $C$ (the state space) and a morphism $c\colon C\to HC$ (its structure). A morphism $h\colon(C,c)\to(D,d)$ of coalgebras is a morphism $h\colon C\to D$ of ${\mathbb{C}}$ such that $Hh\circ c=d\circ h$ . We let $\operatorname{\mathsf{Coalg}}(H)$ denote the category of coalgebras for $H$ and their morphisms.

Subcoalgebras of a coalgebra $(C,c)$ are represented by coalgebra morphisms $m\colon(S,s)\rightarrowtail(C,c)$ with $m$ monic in ${\mathbb{C}}$ , and strong quotients of $(C,c)$ are represented by coalgebra morphisms $e\colon(C,c)\twoheadrightarrow(Q,q)$ with $e$ strongly epic in ${\mathbb{C}}$ . If $H$ preserves monomorphisms, a subcoalgebra is uniquely determined by the object $S$ . If moreover ${\mathbb{C}}$ has (strong epi, mono)-factorizations, then every coalgebra morphism $h\colon(C,c)\to(D,d)$ factorizes uniquely as a strong quotient followed by a subcoalgebra: $h=(\begin{matrix}\includegraphics{dagpub-standalone-combined-2026-01-06-12-05-% 27-page-2.pdf2svg.svg}\end{matrix})$ . This factorization is called the image factorization of $h$ , and $m$ is the image of $h$ .

Example 2.10 (Graphs).

A coalgebra for the power set functor $\mathcal{P}$ on $\mathsf{Set}$ is precisely a (directed) graph. A coalgebra for the finite power set functor $\mathcal{P}_{\omega}$ (the finitary coreflection of $\mathcal{P}$ ) corresponds to a finitely branching graph, i.e. one where every node has only finitely many outgoing edges. Given a graph $(C,c)$ , we write $x\to y$ iff $y\in c(x)$ . A subcoalgebra of $(C,c)$ is a subset $S\subseteq C$ closed under successors: $x\in S$ and $x\to y$ implies $y\in S$ .

Example 2.11 (Automata and Transition Systems).

Various important types of automata and transition systems can be modelled as coalgebras for a set functor $H$ , including deterministic automata ( $HX=\{0,1\}\times X^{A}$ for a fixed finite input alphabet $A$ ), non-deterministic automata ( $HX=\{0,1\}\times(\mathcal{P}X)^{A}$ ), labelled transition systems ( $HX=(\mathcal{P}X)^{A}$ ), discrete labelled Markov chains ( $HX=(\mathcal{D}X)^{A}$ where $\mathcal{D}$ is the finite distribution functor), and many more [23, 37].

Examples of coalgebras beyond the category of sets are discussed later, e.g. graphs in a topos (Section 4.2), coalgebras in nominal sets which model automata and transition systems over infinite alphabets (Section 4.4), and coalgebras in convex sets, modelling systems that combine probabilistic and non-deterministic branching (Section 4.5).

We refer the reader to Jacobs [23] or Rutten [37] for general introductions to the rich theory of coalgebras. For our purposes, we only need to recall two basic results. The first one asserts that colimits in $\operatorname{\mathsf{Coalg}}(H)$ are formed in the underlying category:

Lemma 2.12 ([37, Prop. 4.7]).

The forgetful functor from $\operatorname{\mathsf{Coalg}}(H)$ to ${\mathbb{C}}$ creates colimits.

The second result concerns coalgebras with “finite” state space. A coalgebra is fp-carried if its state space is finitely presentable, and fg-carried if its state space is finitely generated. We let $\operatorname{\mathsf{Coalg}}_{\mathrm{fp}}(H),\operatorname{\mathsf{Coalg}}_{% \mathrm{fg}}(H)\hookrightarrow\operatorname{\mathsf{Coalg}}(H)$ denote the corresponding full subcategories.

Lemma 2.13 ([1, Lem. 3.2]).

Let $H\colon{\mathbb{C}}\to{\mathbb{C}}$ be a finitary endofunctor.

1.

Every $f p$ -carried coalgebra is a finitely presentable object of $\operatorname{\mathsf{Coalg}}(H)$ .
2.

If $H$ preserves monos, every fg-carried coalgebra is a finitely generated object of $\operatorname{\mathsf{Coalg}}(H)$ .

Dually to the notion of coalgebra, algebras for an endofunctor yield a categorical abstraction of algebraic structures. An algebra $(A,a)$ for $H\colon{\mathbb{C}}\to{\mathbb{C}}$ is given by an object $A$ (its carrier) and a morphism $a\colon HA\to A$ (its structure). A morphism $h\colon(A,a)\to(B,b)$ of algebras is a morphism $h\colon A\to B$ of $\mathbb{C}$ such that $h\circ a=b\circ Hh$ . Algebras for $H$ and their morphisms form a category $\operatorname{\mathsf{Alg}}(H)$ . An initial algebra $(I,i)$ is an initial object of $\operatorname{\mathsf{Alg}}(H)$ . By Lambek’s lemma [29], its structure $i\colon HI\to I$ is an isomorphism in ${\mathbb{C}}$ .

Example 2.14 ( $\Sigma$ -Algebras).

The prime example of functor algebras are algebras for a signature. An (algebraic) signature is given by a set $\Sigma$ of operation symbols and a map $\mathsf{ar}\colon\Sigma\to\mathbb{N}$ associating to every ${\mathop{\mathsf{f}}}\in\Sigma$ its arity. Every signature $\Sigma$ induces the polynomial endofunctor $H_{\Sigma}X=\coprod_{{\mathop{\mathsf{f}}}\in\Sigma}X^{\mathsf{ar}({\mathop{% \mathsf{f}}})}$ on $\mathsf{Set}$ . An algebra for $H_{\Sigma}$ is precisely an algebra for the signature $\Sigma$ : a set $A$ with an operation ${\mathop{\mathsf{f}}}^{A}\colon A^{n}\to A$ for every $n$ -ary operation symbol ${\mathop{\mathsf{f}}}\in\Sigma$ . The initial algebra for $H_{\Sigma}$ is the algebra of closed terms formed over the signature $\Sigma$ .

Well-Founded and Recursive Coalgebras.

The concept of “having no infinite paths” can be extended from graphs to arbitrary coalgebras [41]. A subcoalgebra $m\colon(S,s)\rightarrowtail(C,c)$ of a coalgebra $(C,c)$ is cartesian if the commutative diagram in Figure 3 is a pullback. A coalgebra $(C,c)$ is well-founded if it is has no proper cartesian subcoalgebras: for every cartesian subcoalgebra $m\colon(S,s)\rightarrowtail(C,c)$ , the monomorphism $m$ is an isomorphism.

Figure 2: A cartesian subcoalgebra.

Figure 3: A coalgebra-to-algebra morphism.

Example 2.15 (Graphs).

Let $(C,c)$ be a $\mathcal{P}$ -coalgebra, viewed as a graph. We note first that a subset $S\subseteq C$ carries a cartesian subcoalgebra iff, for all $x\in C$ ,

x\in S\iff\text{all successors of $x$ lie in $S$.}

(2.1)

Indeed, the left-to-right implication says that the square in Figure 3 commutes ( $S$ is a subcoalgebra), and the right-to-left implication says that it is a pullback. From this, it follows that

\text{$(C,c)$ is well-founded}\iff\text{$(C,c)$ has no infinite paths}.

For the left-to-right implication, suppose that $(C,c)$ is well-founded. Then the set $S\subseteq C$ of all states that lie on no infinite path is a cartesian subcoalgebra by (2.1), and so $S=C$ . For the right-to-left implication, we argue contrapositively. Suppose that $(C,c)$ is not well-founded, and let $S\subsetneq C$ be a proper cartesian subcoalgebra. Pick $x_{0}\in C\setminus S$ arbitrarily. By (2.1), some successor $x_{1}$ of $x_{0}$ lies in $C\setminus S$ . By (2.1) again, some successor $x_{2}$ of $x_{1}$ lies in $C\setminus S$ . Repeating this argument yields an infinite path $x_{0}\to x_{1}\to x_{2}\to\cdots$ .

Example 2.16 (Coalgebras for Set Functors).

For every functor $H\colon\mathsf{Set}\to\mathsf{Set}$ that preserves wide intersections and every set $X$ , there is map $\mathsf{supp}_{X}\colon HX\to\mathcal{P}X$ that sends an element $t\in HX$ to its support, the least subset $m\colon M\hookrightarrow X$ such that $t\in Hm[HM]$ . Every coalgebra $(C,c)$ for $H$ thus induces a coalgebra $(C,\mathsf{supp}_{C}\circ c)$ for $\mathcal{P}$ , the canonical graph of $(C,c)$ . A coalgebra for $H$ is well-founded iff its canonical graph is well-founded [41, Rem. 6.3.4].

One important application of well-founded graphs is the principle of well-founded induction and well-founded recursion. This principle can be understood at the level of coalgebras [41].

Given a coalgebra $(C,c)$ and an algebra $(A,a)$ for the same functor $H$ , a coalgebra-to-algebra morphism from $(C,c)$ to $(A,a)$ is a morphism $h\colon C\to A$ making the square in Figure 3 commute. A coalgebra $(C,c)$ is recursive if for every algebra $(A,a)$ there exists a unique coalgebra-to-algebra morphism from $(C,c)$ to $(A,a)$ .

Example 2.17 (Graphs).

Every well-founded $\mathcal{P}$ -coalgebra $(C,c)$ is recursive. Indeed, this amounts to saying that for every $a\colon\mathcal{P}A\to A$ , there is unique map $h\colon C\to A$ such that $h(x)=a(h[c(x)])$ for all $x\in C$ . This is precisely the principle of well-founded recursion. The special case where $a\colon\mathcal{P}\{0,1\}\to\{0,1\}$ sends $\emptyset$ , $\{1\}$ to $1$ and $\{0\}$ , $\{0,1\}$ to $0$ corresponds to well-founded induction: given a predicate $P\colon C\to\{0,1\}$ , one has

\big(\,\forall x\in C.\,(\forall y\in c(x).\,P(y)\implies P(x))\,\big)\quad% \implies\quad\big(\,\forall x\in C.\,P(x)\,\big).

In the following, we denote by

\operatorname{\mathsf{Coalg}}_{{\mathrm{fp}},{\mathrm{wf}}}(H),\,\operatorname% {\mathsf{Coalg}}_{{\mathrm{fg}},{\mathrm{wf}}}(H),\,\operatorname{\mathsf{% Coalg}}_{\mathrm{wf}}(H),\,\operatorname{\mathsf{Coalg}}_{{\mathrm{fp}},{% \mathrm{rec}}}(H),\,\operatorname{\mathsf{Coalg}}_{{\mathrm{fg}},{\mathrm{rec}% }}(H),\,\operatorname{\mathsf{Coalg}}_{\mathrm{rec}}(H)

the full subcategories of $\operatorname{\mathsf{Coalg}}(H)$ given by all (fp-carried, fg-carried) well-founded coalgebras, and analogously for recursive coalgebras.

We conclude with some general properties of well-founded and recursive coalgebras. First, colimits of recursive coalgebras are computed in the underlying category [4, Prop. 7.1.9]:

Lemma 2.18.

The subcategory $\operatorname{\mathsf{Coalg}}_{\mathrm{rec}}(H)\hookrightarrow\operatorname{% \mathsf{Coalg}}(H)$ is closed under colimits.

We also mention that recursive coalgebras bear a close connection with initial algebras: If $(I,i)$ is an initial algebra for $H$ , then $(I,i^{-1})$ is a final recursive coalgebra, and vice versa [13].

Regarding well-founded coalgebras, we need the results of the proposition below. We state them for a locally finitely presentable base category ${\mathbb{C}}$ , our setting of interest; however, they hold under slightly weaker assumptions [4, Cor. 8.4.3, Thm. 8.5.3]. In the following, an initial object $0$ is called simple if for every object $X$ the unique morphism $0\to X$ is monic.

Proposition 2.19.

Let ${\mathbb{C}}$ be a locally finitely presentable category with a simple initial object, and let $H\colon{\mathbb{C}}\to{\mathbb{C}}$ be an endofunctor that preserves monomorphisms.

1.

The subcategory $\operatorname{\mathsf{Coalg}}_{\mathrm{wf}}(H)\hookrightarrow\operatorname{% \mathsf{Coalg}}(H)$ is closed under colimits and strong quotients.
2.

Every well-founded coalgebra is recursive, that is, $\operatorname{\mathsf{Coalg}}_{\mathrm{wf}}(H)\subseteq\operatorname{\mathsf{% Coalg}}_{\mathrm{rec}}(H)$ .

3 Kőnig’s Lemma for Coalgebras

We are prepared to work towards the core result of our paper, Kőnig’s lemma for coalgebras over a locally finitely presentable category (Theorem 3.7). Let us first fix the global setup:

Assumption 3.1.

For the remainder of this paper, we fix a finitary endofunctor $H$ on a locally finitely presentable category ${\mathbb{C}}$ .

Most of our results require the following two additional conditions on ${\mathbb{C}}$ and $H$ :

( $\overset{\smash{\raisebox{-1.0pt}{$\scriptstyle+$}}}{\rightarrowtail}$ ): The injections ${\mathop{\mathsf{inl}}}\colon A\to A+B$ and ${\mathop{\mathsf{inr}}}\colon B\to A+B$ of binary coproducts in ${\mathbb{C}}$ are monic.
( $H\cap$ ): The functor $H$ preserves binary intersections (i.e. pullbacks of monomorphisms).

We will tag all results below with the conditions they require (on top of the global conditions given by Section 3). For example, Proposition 3.6 requires both ( $\overset{\smash{\raisebox{-1.0pt}{$\scriptstyle+$}}}{\rightarrowtail}$ ) and ( $H\cap$ ).

Remark 3.2.

The two extra conditions ( $\overset{\smash{\raisebox{-1.0pt}{$\scriptstyle+$}}}{\rightarrowtail}$ ) and ( $H\cap$ ) are fairly mild:

1.

Condition ( $\overset{\smash{\raisebox{-1.0pt}{$\scriptstyle+$}}}{\rightarrowtail}$ ) holds in every extensive category with finite limits [14, Prop. 3.3]. Recall that a category ${\mathbb{C}}$ is extensive [14] if it has finite coproducts and for any pair of objects $A$ , $B$ the functor ${\mathbb{C}}/A\times{\mathbb{C}}/B\xrightarrow{+}{\mathbb{C}}/(A+B)$ on slice categories sending $(f\colon X\to A)$ , $(g\colon Y\to B)$ to $(f+g\colon X+Y\to A+B)$ is an equivalence of categories. Informally, this means that coproducts behave like disjoint unions. The categories of sets, posets, and nominal sets are extensive, as is every elementary topos [25]. There are also many non-extensive categories with ( $\overset{\smash{\raisebox{-1.0pt}{$\scriptstyle+$}}}{\rightarrowtail}$ ), including the categories of vector spaces or convex sets (Section 4.5).
2.

Condition ( $H\cap$ ) “almost” holds for every functor $H\colon\mathsf{Set}\to\mathsf{Set}$ . By a classical result due to Trnková [43] (see also [4, Prop. 8.1.13]), every set functor $H$ can be modified, by changing its action on the empty set and functions with empty domain, to a functor $\widetilde{H}$ that preserves binary intersections. Since $\operatorname{\mathsf{Coalg}}(H)\cong\operatorname{\mathsf{Coalg}}(\widetilde{% H})$ , one can thus assume that $H$ preserves binary intersections without loss of generality for coalgebraic results.

Remark 3.3.

1.

Condition ( $\overset{\smash{\raisebox{-1.0pt}{$\scriptstyle+$}}}{\rightarrowtail}$ ) implies that the initial object $0$ is simple: given $X\in{\mathbb{C}}$ , the unique morphism $0\to X$ is the coproduct injection ${\mathop{\mathsf{inl}}}\colon 0\to 0+X\cong X$ , hence monic.
2.

Condition ( $H\cap$ ) implies that $H$ preserves monomorphisms. This follows from the fact that $m\colon A\to B$ is monic iff the pair ${\mathsf{id}}_{A},{\mathsf{id}}_{A}$ is a pullback of $m, m$ .

We start with a simple construction, the coproduct extension of a coalgebra. It appeared earlier in the theory of iterative algebras [6, 44] and underlies both our proof of the coalgebraic Kőnig’s lemma and the initial algebra constructions presented in Section 5.

Construction 3.4 (Coproduct Extension).

The coproduct extension of an $H$ -coalgebra $(C,c)$ by a morphism $p\colon X\to HC$ is the coalgebra $(C+X,c_{p})$ whose structure is given by

c_{p}\,\equiv\,(\,C+X\xrightarrow{[c,p]}HC\xrightarrow{H{\mathop{\mathsf{inl}}% }}H(C+X)\,).

Let us immediately note an expected property of coproduct extensions:

Lemma 3.5.

The coproduct injection ${\mathop{\mathsf{inl}}}\colon(C,c)\to(C+X,c_{p})$ is a coalgebra morphism.

Informally, a coproduct extension adds to a given coalgebra $(C,c)$ a set $X$ of new states and lets every new state transition arbitrarily into states from $C$ , while leaving transitions of states in $C$ unchanged. This construction should not introduce any infinite paths to the given coalgebra, which is confirmed by the following result:

Proposition 3.6 ( $\overset{\smash{\raisebox{-1.0pt}{$\scriptstyle+$}}}{\rightarrowtail}$ , $H\cap$ ).

For every well-founded coalgebra $(C,c)$ and every morphism $p\colon X\to HC$ , the coproduct extension $(C+X,c_{p})$ is a well-founded coalgebra.

Proof sketch.

Let $m\colon(S,s)\rightarrowtail(C+X,c_{p})$ be a cartesian subcoalgebra. We need to prove that $m$ is an isomorphism. Form the two intersections in ${\mathbb{C}}$ shown below; note that the coproduct injections ${\mathop{\mathsf{inl}}}$ and ${\mathop{\mathsf{inr}}}$ are monic by assumption ( $\overset{\smash{\raisebox{-1.0pt}{$\scriptstyle+$}}}{\rightarrowtail}$ ).

\begin{matrix}\includegraphics{dagpub-standalone-combined-2026-01-06-12-05-27-% page-5.pdf2svg.svg}\end{matrix}\qquad\begin{matrix}\includegraphics{dagpub-% standalone-combined-2026-01-06-12-05-27-page-6.pdf2svg.svg}\end{matrix}

One can show that both $r_{S\cap C}$ and $r_{S\cap X}$ are isomorphisms. In the case of $r_{S\cap C}$ , this follows from the observation that the subobject $r_{S\cap C}\colon S\cap C\rightarrowtail C$ carries a cartesian subcoalgebra of the well-founded coalgebra $(C,c)$ . We conclude that $m$ is a split epimorphism:

m\circ[l_{S\cap C}\circ r_{S\cap C}^{-1},l_{S\cap X}\circ r_{S\cap X}^{-1}]=[{% \mathop{\mathsf{inl}}},{\mathop{\mathsf{inr}}}]={\mathsf{id}}_{C+X},

and since $m$ is also monic, it is an isomorphism as required. $\hfill\blacktriangleleft$

Figure 4: Join of subcoalgebras.

Figure 5: Cartesianess.

$k\mapsto(-|k|{-}1,|k|{+}1)$

Figure 6: A coalgebra.

Recall the classical Kőnig’s lemma: In a finitely branching well-founded graph (equivalently, a well-founded $\mathcal{P}_{\omega}$ -coalgebra), every node lies in some finite subcoalgebra. The following theorem generalizes Kőnig’s lemma to coalgebras over locally finitely presentable categories:

Theorem 3.7 (Coalgebraic Kőnig’s Lemma, $\overset{\smash{\raisebox{-1.0pt}{$\scriptstyle+$}}}{\rightarrowtail}$ , $H\cap$ ).

Every well-founded $H$ -coalgebra is the directed join of its fg-carried well-founded subcoalgebras.

Here the join is formed in the complete lattice of subcoalgebras of the given coalgebra. As a minor subtlety, we note that subcoalgebras of well-founded coalgebras generally need not be well-founded; this would require stronger assumptions [4, Prop. 8.4.7]. Therefore, it is crucial that Theorem 3.7 considers well-founded (not arbitrary) subcoalgebras.

Proof sketch.

Let $(C,c)$ be a well-founded coalgebra, and let $m_{i}\colon(C_{i},c_{i})\rightarrowtail(C,c)$ ( $i\in I$ ) be the family of all fg-carried well-founded subcoalgebras of $(C,c)$ . Under the usual subobject ordering, the family forms a directed poset; this follows easily from the closure properties of ${\mathbb{C}}_{\mathrm{fg}}$ (Lemma 2.2) and $\operatorname{\mathsf{Coalg}}_{{\mathrm{wf}}}(H)$ (Proposition 2.19.1). Form the (directed) join of all $m_{i}$ in in the complete lattice of subcoalgebras of $(C,c)$ (see Figure 6). This join is computed at the level of the subobject lattice of $C\in{\mathbb{C}}$ (Lemma 2.12). Since directed joins of subobjects in locally finitely presentable categories are directed colimits (Lemma 2.6), we see that $(n_{i})_{i\in I}$ is a colimit cocone. It suffices to show that $m$ is a cartesian subcoalgebra, since this implies that $m$ is an isomorphism and hence proves the theorem.

For the proof that $m$ is cartesian (Figure 6), one needs to show that the commutative square below forms a pullback, that is, given $f\colon X\to H(\bigvee C_{i})$ and $g\colon X\to C$ with $Hm\circ f=c\circ g$ , one needs to construct the mediating morphism $k\colon X\to\bigvee C_{i}$ . This is achieved by first constructing $k$ for the case $X\in{\mathbb{C}}_{\mathrm{fg}}$ . Here one factorizes the morphism $f$ as $X\xrightarrow{p}HC_{i}\xrightarrow{Hn_{i}}H(\bigvee_{i}C_{i})$ for some $p$ and $i$ , using that $(Hn_{i})$ is a colimit cocone since the functor $H$ is finitary, and then analyses the coproduct extension $(C_{i}+X,(c_{i})_{p})$ . The general case $X\in{\mathbb{C}}$ follows from the case of finitely generated objects by expressing $X$ as the colimit of its finitely generated subobjects. This is the point in the proof where we need that ${\mathbb{C}}$ is locally finitely presentable. $\hfill\blacktriangleleft$

As an immediate consequence, we get a property of the category of well-founded coalgebras:

Corollary 3.8 ( $\overset{\smash{\raisebox{-1.0pt}{$\scriptstyle+$}}}{\rightarrowtail}$ , $H\cap$ ).

If ${\mathbb{C}}_{\mathrm{fp}}={\mathbb{C}}_{\mathrm{fg}}$ , then $\operatorname{\mathsf{Coalg}}_{\mathrm{wf}}(H)$ is locally finitely presentable.

Proof.

The category $\operatorname{\mathsf{Coalg}}_{\mathrm{wf}}(H)$ is cocomplete because it is closed under colimits in $\operatorname{\mathsf{Coalg}}(H)$ (Proposition 2.19.1). All coalgebras in $\operatorname{\mathsf{Coalg}}_{{\mathrm{fp}},{\mathrm{wf}}}(H)$ are finitely presentable objects of $\operatorname{\mathsf{Coalg}}_{\mathrm{wf}}(H)$ ; this follows from the fact that all coalgebras in $\operatorname{\mathsf{Coalg}}_{\mathrm{fp}}(H)$ are finitely presentable objects of $\operatorname{\mathsf{Coalg}}(H)$ (Lemma 2.13) and that $\operatorname{\mathsf{Coalg}}_{\mathrm{wf}}(H)$ is closed under (filtered) colimits in $\operatorname{\mathsf{Coalg}}(H)$ . By Theorem 3.7, every object of $\operatorname{\mathsf{Coalg}}_{\mathrm{wf}}(H)$ is a filtered colimit of objects in $\operatorname{\mathsf{Coalg}}_{{\mathrm{fp}},{\mathrm{wf}}}(H)=\operatorname{% \mathsf{Coalg}}_{{\mathrm{fg}},{\mathrm{wf}}}(H)$ . Thus $\operatorname{\mathsf{Coalg}}_{\mathrm{wf}}(H)$ is locally finitely presentable. $\hfill\blacktriangleleft$

Without the restrictive assumption that ${\mathbb{C}}_{\mathrm{fp}}={\mathbb{C}}_{\mathrm{fg}}$ , we get a slightly weaker result. It makes use of the following characterization of locally presentable categories (cf. Section 2):

Theorem 3.9 (Local Generation Theorem [7, Thm. 1.70]).

A category is locally presentable iff it is cocomplete and, for some regular cardinal $\lambda$ , there exists a set $\mathcal{A}$ of $\lambda$ -generated objects such that every object is the $\lambda$ -directed colimit of the diagram of its subobjects from $\mathcal{A}$ .

Note that the “if” direction of the theorem does not claim that the category is locally $\lambda$ -presentable. We now instantiate this theorem to the category $\operatorname{\mathsf{Coalg}}_{\mathrm{wf}}(H)$ , $\lambda=\omega$ , and $\mathcal{A}=\operatorname{\mathsf{Coalg}}_{{\mathrm{fg}},{\mathrm{wf}}}(H)$ . The coalgebras in $\mathcal{A}$ are finitely generated objects of $\operatorname{\mathsf{Coalg}}_{\mathrm{wf}}(H)$ because they are finitely generated in $\operatorname{\mathsf{Coalg}}(H)$ (Lemma 2.13) and $\operatorname{\mathsf{Coalg}}_{\mathrm{wf}}(H)$ is closed under filtered colimits in $\operatorname{\mathsf{Coalg}}(H)$ (Proposition 2.19.1). Every coalgebra in $\operatorname{\mathsf{Coalg}}_{\mathrm{wf}}(H)$ is the directed colimit of its subobjects from $\mathcal{A}$ (Theorem 3.7). Thus, the Local Generation Theorem yields:

Corollary 3.10 ( $\overset{\smash{\raisebox{-1.0pt}{$\scriptstyle+$}}}{\rightarrowtail}$ , $H\cap$ ).

The category $\operatorname{\mathsf{Coalg}}_{\mathrm{wf}}(H)$ is locally presentable.

We conclude this section with the observation that the coalgebraic Kőnig’s lemma no longer holds when well-founded coalgebras are replaced with recursive ones, even in $\mathsf{Set}$ :

Example 3.11 (Kőnig’s Lemma Fails for Recursive Coalgebras).

Consider the set functor

HX={\{*\}}+{\{\,(x_{1},x_{2})\in X\times X\mid x_{1}\neq x_{2}\,\}}

which is the quotient of $X\times X$ identifying all elements on the diagonal with a constant $*$ . Clearly, $H$ is finitary and preserves binary intersections. Let $(C,c)$ be the coalgebra with state space $C:=\mathbb{Z}\setminus{\{0\}}$ and the transition structure $c\colon C\to HC$ , $c(k)=(-|k|-1,|k|+1)$ visualized in Figure 6. The only finite subcoalgebra of $(C,c)$ is the empty coalgebra; thus, $(C,c)$ is not the union of its finite recursive subcoalgebras. However, $(C,c)$ is recursive: For every $H$ -algebra $(A,a)$ , the constant map $h\colon(C,c)\to(A,a)$ defined by $h(k):=a(*)$ is the unique coalgebra-to-algebra morphism. Indeed, $h$ is such a morphism because $(Hh\circ c)(k)=*\in HA$ and so $(a\circ Hh\circ c)(k)=a(*)=h(k)$ for all $k\in C$ . To prove uniqueness, suppose that $g\colon(C,c)\to(A,a)$ is a coalgebra-to-algebra morphism, and let $k\in C$ . Since $c(|k|+1)=c(-|k|-1)$ , we necessarily have $g(|k|+1)=g(-|k|-1)$ by $g=a\circ HG\circ c$ . Thus, $Hg(c(k))=*\in HA$ and again by $g=a\circ HG\circ c$ , we obtain

g(k)=(a\circ Hg\circ c)(k)=a(*)=h(k).

4 Applications of the Coalgebraic Kőnig’s Lemma

We present a few selected instantiations of our coalgebraic Kőnig’s lemma (Theorem 3.7).

4.1 Coalgebras for Set Functors

For the category ${\mathbb{C}}=\mathsf{Set}$ , we recover a recent result by Adámek et al. [4, Prop, 9.2.19] as a special case of Theorem 3.7:

Theorem 4.1 (Kőnig’s Lemma for Coalgebras in $\mathsf{Set}$ ).

If $H$ is a finitary set functor, then every state of a well-founded $H$ -coalgebra lies in some finite subcoalgebra.

Indeed, by Section 3.2 we can safely assume that a finitary set functor $H$ preserves binary intersections (by modifying $H$ on the empty set). Thus Theorem 3.7 applies.

4.2 Graphs in a Topos

While Theorem 4.1 extends Kőnig’s lemma from graphs to coalgebras in $\mathsf{Set}$ , we now take an orthogonal direction: we stick with graphs but interpret them in a locally finitely presentable elementary topos ${\mathbb{C}}$ [26]. (We assume basic familiarity with topos theory in this subsection.) Examples of locally finitely presentable toposes include the topos of sets, nominal sets (see Section 4.4), any presheaf topos $\mathsf{Set}^{\mathbb{D}}$ , or any coherent Grothendieck topos [25, Rem. D.3.3.12].

Graphs in a topos are coalgebras for the covariant power object functor $\mathcal{P}\colon{\mathbb{C}}\to{\mathbb{C}}$ [25, Sec. A.2.3]; the latter maps each object $C$ to its power object $\mathcal{P}C=\Omega^{C}$ , where $\Omega$ is the subobject classifier. By cartesian closure, a coalgebra $c\colon C\to\mathcal{P}C=\Omega^{C}$ corresponds to a morphism from $C\times C$ to $\Omega$ and thus to a subobject of $C\times C$ , that is, a relation on $C$ . The role of the finite power set functor (modelling finitely branching graphs) is now played by the finitary coreflection $\mathcal{P}_{\omega}$ of $\mathcal{P}$ (Lemma 2.9). Note that $\mathcal{P}_{\omega}$ is generally different from the Kuratowski functor $\mathcal{K}\colon{\mathbb{C}}\to{\mathbb{C}}$ , which captures Kuratowski-finite subobjects [26, Thm. 9.16].

To see that $\mathcal{P}_{\omega}$ -coalgebras indeed model “finite” branching, let $i\colon\mathcal{P}_{\omega}\to\mathcal{P}$ denote the co-universal natural transformation witnessing that $\mathcal{P}_{\omega}$ is the finitary coreflection of $\mathcal{P}$ . Every $\mathcal{P}_{\omega}$ -coalgebra $c\colon C\to\mathcal{P}_{\omega}C$ can be viewed as a $\mathcal{P}$ -coalgebra $i_{C}\circ c\colon C\to\mathcal{P}C$ and therefore as a relation $m_{c}\colon E_{c}\rightarrowtail C\times C$ . Given $s\colon I\to C$ we let $m_{c,I}\colon E_{c,I}\rightarrowtail I\times C$ denote the preimage of $m_{c}$ under $s\times{\mathsf{id}}$ :

We then have the following simple result. Informally, it expresses that if we consider a finitely indexed family $(s_{i})_{i\in I}$ of states in $C$ , then their successors can also be finitely indexed.

Lemma 4.2.

Let ${\mathbb{C}}$ be a locally finitely presentable topos, and let $c\colon C\to\mathcal{P}_{\omega}C$ be a coalgebra for $\mathcal{P}_{\omega}$ . Then for every $s\colon I\to C$ ( $I\in{\mathbb{C}}_{\mathrm{fp}}$ ) there exists $t\colon J\to C$ ( $J\in{\mathbb{C}}_{\mathrm{fp}}$ ) such that $m_{c,I}\colon E_{c,s}\rightarrowtail I\times C$ factorizes through ${\mathsf{id}}\times t\colon I\times J\to I\times C$ .

Applying the coalgebraic Kőnig’s lemma to the case of $\mathcal{P}_{\omega}$ -coalgebras yields:

Theorem 4.3 (Kőnig’s Lemma for Graphs in a Topos).

Let ${\mathbb{C}}$ be a locally finitely presentable topos. Every well-founded $\mathcal{P}_{\omega}$ -coalgebra is the join of its fg-carried well-founded subcoalgebras.

4.3 Binary Trees

An important special case of Kőnig’s lemma, studied in constructive mathematics [16], is its restriction to binary trees – the weak Kőnig’s lemma. Here a binary tree is one where every node has at most two children, and children are ordered, that is, binary trees form coalgebras for $HX=X\times X+X+1$ on $\mathsf{Set}$ . For locally finitely presentable categories with nice coproducts (cf. Section 3), the generalized Kőnig’s lemma also has a weak version:

Theorem 4.4 (Coalgebraic Weak Kőnig’s Lemma).

Let ${\mathbb{C}}$ be a locally finitely presentable and extensive category. Then every well-founded coalgebra for the functor $HX=X\times X+X+1$ on ${\mathbb{C}}$ is the join of its fg-carried well-founded subcoalgebras.

This theorem extends to polynomial functors $HX=\coprod_{i\in I}X^{n_{i}}$ where $I$ is finite and $n_{i}\in\mathbb{N}$ .

4.4 Nominal Transition Systems

Nominal sets [36] are a categorical framework to reason about variable names and binding (like in the $\lambda$ -calculus) and have also served as a basis for the study of automata and transition systems over infinite alphabets, whose elements represent data values [8].

Parametric in a fixed countably infinite set of atoms $\mathbb{A}$ – intuitively the variable names or alphabet – a nominal set consists of a set $X$ with a group action $\textnormal{`$\cdot$'}\colon\mathfrak{S}(\mathbb{A})\times X\to X$ for the group $\mathfrak{S}(\mathbb{A})$ of finite permutations $\pi\colon\mathbb{A}\to\mathbb{A}$ , satisfying the following finite support property: for each $x\in X$ , there is a finite set $S\subseteq\mathbb{A}$ such that $\text{if }\pi(a)=a\text{ for all }a\in S\text{ then }\pi\cdot x=x.$

Intuitively, elements of nominal sets are syntactic objects holding atoms from $\mathbb{A}$ , which can be renamed using finite permutations. The finite support property means that each element in a nominal set can hold only finitely many atoms. For example, the set $\mathbb{A}^{*}$ of finite words over $\mathbb{A}$ forms a nominal set with group action $\pi\cdot(a_{1}\cdots a_{n})=\pi(a_{1})\cdots\pi(a_{n})$ . Similarly, the terms of the $\lambda$ -calculus (modulo $\alpha$ -equivalence) with variables from $\mathbb{A}$ form a nominal set whose group action is capture-avoiding renaming of free variables, e.g. $(a\,b)\cdot(\lambda a.\,a\,b)=\lambda c.\,c\,a$ .

Nominal sets form a full subcategory $\mathsf{Nom}$ of the category of $\mathfrak{S}(\mathbb{A})$ -actions and equivariant maps (that is, maps preserving the group action). The category $\mathsf{Nom}$ is a locally finitely presentable boolean topos with the subobject classifier $\Omega=2$ being the two-element set (with trivial action). Finitely presentable and finitely generated objects are precisely the orbit-finite nominal sets [36, Thm. 5.16], that is, those nominal sets having only finitely many elements up to renaming. For example, $\mathbb{A}^{*}$ is not orbit-finite, but the nominal set $\mathbb{A}^{n}$ of words of fixed length $n$ is. We call a subset $M\subseteq X$ of a nominal set orbit-finite if ${\big\{{\{\pi\cdot x\mid\pi\in\mathfrak{S}(\mathbb{A})\}}\mid x\in M\big\}}$ is a finite set, and finitely supported if it satisfies the finite support property w.r.t. the group action $\pi\cdot M={\{\pi\cdot x\mid x\in M\}}$ . The power object functor $\mathcal{P}$ on $\mathsf{Nom}$ is given by $\mathcal{P}X={\{M\subseteq X\mid\text{$M$ finitely supported}\}}$ , and its finitary coreflection by $\mathcal{P}_{\omega}X={\{M\subseteq X\mid\text{$M$ finitely supported and % orbit-finite}\}}$ .

Applying Theorem 3.7 to the category of nominal sets gives the following general result:

Theorem 4.5 (Kőnig’s Lemma for Coalgebras in $\mathsf{Nom}$ ).

If $H$ is a finitary functor on $\mathsf{Nom}$ preserving binary intersections, then every state of a well-founded $H$ -coalgebra lies in some orbit-finite subcoalgebra.

Coalgebras for finitary functors on $\mathsf{Nom}$ admit possibly infinite branching as long as it is finite up to renaming (cf. [33, Sec. 6.2]). For illustration, let us consider coalgebras for the functor $(\mathcal{P}_{\omega})^{\mathbb{A}}$ on $\mathsf{Nom}$ . (Here $(-)^{\mathbb{A}}$ denotes the exponential.) They admit a simple concrete description: A nominal labelled transition system (NLTS) is given by a nominal set $C$ of states and a family of relations $\mathord{\xrightarrow{a}}\subseteq C\times C$ ( $a\in\mathbb{A}$ ) such that $x\xrightarrow{a}y$ implies $\pi\cdot x\xrightarrow{\pi(a)}\pi\cdot y$ for all $\pi\in\mathfrak{S}(\mathbb{A})$ . It is image-orbit-finite if for all $x\in C$ and $a\in\mathbb{A}$ the set ${\{y\in C\mid x\xrightarrow{a}y\}}$ is orbit-finite.

An NLTS can be viewed as an ordinary LTS by forgetting the group action.

Lemma 4.6.

Coalgebras for $\smash{(\mathcal{P}_{\omega})^{\mathbb{A}}}$ are in bijective correspondence with image-orbit-finite NLTS. Moreover, a coalgebra is well-founded iff the corresponding LTS has no infinite paths.

Note that an image-orbit-finite NLTS is generally not finitely branching as an LTS, both due to the infinity of the label set $\mathbb{A}$ and due to the fact that each state $x$ has a possibly infinite set of $a$ -successors for a given label $a$ . Thus, the classical Kőnig’s lemma does not apply here. However, the orbit-finite branching and equivariance of transitions is enough to get following result, which is an instance of Theorem 4.5:

Theorem 4.7 (Kőnig’s Lemma for Nominal LTS).

Every state of a well-founded image-orbit-finite NLTS lies in some orbit-finite subcoalgebra.

4.5 Convex Transition Systems

The category of convex sets [39] provides a natural setting for studying probabilistic automata and transition systems, in particular systems that combine probabilistic choice with non-determinism [9, 35, 34, 10]. Sets of probability distributions are modelled as objects in the category, while non-determinism is captured by a convex version of the power set functor.

A convex set is a set $X$ equipped with a family of binary operations $+_{r}\colon X\times X\rightarrow X$ ( $r\in[0,1]$ ) subject to the following equations, where $s^{\prime}=r+s-rs\neq 0$ and $r^{\prime}=\frac{r}{s^{\prime}}$ :

x+_{r}x=x,\quad x+_{0}y=y,\quad x+_{r}y=y+_{1-r}x,\quad x+_{r}(y+_{s}z)=(x+_{r% ^{\prime}}y)+_{s^{\prime}}z.

(4.1)

Convex sets are an algebraic model of structures that admit convex combinations of elements. The prototypical example of convex sets are convex subsets $X\subseteq\mathbb{R}^{n}$ with the operations $\vec{x}+_{r}\vec{y}:=r\cdot\vec{x}+(1-r)\cdot\vec{y}$ . Another example is the set $\mathcal{D}X$ of finitely supported probability distributions on a set $X$ (i.e. maps $\varphi\colon X\to[0,1]$ such $\varphi(x)=0$ for all but finitely many $x\in X$ and $\sum_{x\in X}\varphi(x)=1$ ) with convex structure given by $\varphi+_{r}\psi=\big(x\mapsto r\cdot\varphi(x)+(1-r)\cdot\psi(x)\big)$ .

A map $f\colon X\rightarrow Y$ between convex sets is affine if $f(x+_{r}x^{\prime})=f(x)+_{r}f(x^{\prime})$ for $x,x^{\prime}\in X$ and $r\in[0,1]$ . We let $\mathsf{Conv}$ denote the category of convex sets and affine maps. It is locally finitely presentable (as is every algebraic category given by a finitary equational theory [7]), and finitely presentable convex sets coincide with finitely generated ones [38, Cor. 5.5]. Note that in algebraic categories, finitely generated objects are the algebras with a finite set of generators [7, Ex. 1.68]. Thus a convex set $X$ is finitely generated iff there exists a finite subset $X_{0}\subseteq X$ such that every $x\in X$ is an (iterated) convex combination of elements of $X_{0}$ .

The convex analogue of the finite power set functor $\mathcal{P}_{\omega}$ is the convex power set functor $\mathcal{P}_{\mathsf{c},\omega}$ on $\mathsf{Conv}$ . It maps a convex set $X$ to the convex set $\mathcal{P}_{\mathsf{c},\omega}X$ of all finitely generated (not finite!) convex subsets of $X$ . The operation $+_{r}$ on $\mathcal{P}_{\mathsf{c},\omega}X$ is given by $S+_{r}T={\{x+_{r}y\mid x\in S,\,y\in T\}}$ for $r\in(0,1)$ , and determined by the second and third axiom of (4.1) for $r\in\{0,1\}$ (e.g. $\emptyset+_{0}S=S=S+_{1}\emptyset$ ). The functor $\mathcal{P}_{\mathsf{c},\omega}$ is the composite of the non-empty convex power set functor and the black-hole extension functor $(-)+1$ from [9, Sec. 5].

A coalgebra $c\colon C\to\mathcal{P}_{\mathsf{c},\omega}C$ is an fg-branching convex graph, that is, a graph where (i) the set $C$ of nodes carries the structure of a convex set, (ii) for every node $x$ the set $c(x)$ of successors forms a finitely generated convex subset of $C$ , and (iii) $c(x+_{r}y)=c(x)+_{r}c(y)$ for all $x,y\in C$ and $r\in[0,1]$ . An fg-branching convex graph can be viewed as an ordinary graph by forgetting the convex structure on $C$ . Well-foundedness is then the expected concept:

Lemma 4.8.

A coalgebra $c\colon C\to\mathcal{P}_{\mathsf{c},\omega}C$ is well-founded iff it has no infinite paths.

When regarded as an ordinary graph, an fg-branching convex graph is generally not finitely branching. However, the fg-branching property is enough to get a Kőnig’s lemma. Indeed, applying Theorem 3.7 to the category $\mathsf{Conv}$ and the functor $\mathcal{P}_{\mathsf{c},\omega}$ yields:

Theorem 4.9 (Kőnig’s Lemma for Convex Graphs).

Every node of a well-founded fg-branching convex graph lies in some fg-carried $\mathcal{P}_{\mathsf{c},\omega}$ -subcoalgebra.

5 Initial Algebras From Finite Well-Founded and Recursive Coalgebras

In this section we establish our second fundamental result about well-founded coalgebras: the initial algebra for $H$ can be constructed as the colimit of all fp-carried well-founded coalgebras. Note that, in contrast, Theorem 3.7 involves fg-carried well-founded coalgebras. The proof is another intricate application of coproduct extension (Section 3).

Construction 5.1.

Let $(T,t)$ be the colimit of all coalgebras in $\operatorname{\mathsf{Coalg}}_{{\mathrm{fp}},{\mathrm{wf}}}(H)$ , i.e. the colimit of the embedding $D\colon\operatorname{\mathsf{Coalg}}_{{\mathrm{fp}},{\mathrm{wf}}}(H)% \hookrightarrow\operatorname{\mathsf{Coalg}}(H)$ . We denote the colimit injections by

c^{\#}\colon(C,c)\to(T,t)\qquad\text{where}\qquad(C,c)\in\operatorname{\mathsf% {Coalg}}_{{\mathrm{fp}},{\mathrm{wf}}}(H).

This colimit is formed at the level of the underlying category ${\mathbb{C}}$ (Lemma 2.12). Moreover, if ${\mathbb{C}}$ has a simple initial object, e.g. if ( $\overset{\smash{\raisebox{-1.0pt}{$\scriptstyle+$}}}{\rightarrowtail}$ ) holds (Section 3), the colimit is filtered because the category $\operatorname{\mathsf{Coalg}}_{{\mathrm{fp}},{\mathrm{wf}}}(H)$ is finitely cocomplete. Indeed, both ${\mathbb{C}}_{\mathrm{fp}}\hookrightarrow{\mathbb{C}}$ and $\operatorname{\mathsf{Coalg}}_{\mathrm{wf}}(H)\hookrightarrow\operatorname{% \mathsf{Coalg}}(H)$ are closed under finite colimits (Lemma 2.13, Proposition 2.19).

We then have the following characterization of the initial algebra for $H$ :

Theorem 5.2 (First Initial Algebra Theorem, $\overset{\smash{\raisebox{-1.0pt}{$\scriptstyle+$}}}{\rightarrowtail}$ , $H\cap$ ).

The initial algebra for $H$ is the colimit of all fp-carried well-founded coalgebras, that is, the coalgebra structure $t\colon T\to HT$ is an isomorphism and the algebra $(T,t^{-1})$ is initial for $H$ .

The crucial part of this theorem is the “Lambek lemma” for the coalgebra $(T,t)$ :

Lemma 5.3 ( $\overset{\smash{\raisebox{-1.0pt}{$\scriptstyle+$}}}{\rightarrowtail}$ , $H\cap$ ).

The coalgebra structure $t\colon T\to HT$ is an isomorphism.

Proof sketch.

Let $U\colon\operatorname{\mathsf{Coalg}}(H)\to{\mathbb{C}}$ be the forgetful functor. Then $(c^{\#})$ is a colimit cocone over $U D$ and $(Hc^{\#}\circ c)$ is a cocone over $U D$ , and $t$ is the unique mediating morphism such that the diagram below commutes for every $(C,c)\in\operatorname{\mathsf{Coalg}}_{{\mathrm{fp}},{\mathrm{wf}}}(H)$ . It suffices to prove that $(Hc^{\#}\circ c)$ forms a colimit cocone over $U D$ ; then $t$ is an isomorphism by uniqueness of colimits. To this end, we verify the criterion of Lemma 2.7: for $X\in{\mathbb{C}}_{\mathrm{fp}}$ , every morphism $q\colon X\to HT$ factorizes essentially uniquely through the cocone $(Hc^{\#}\circ c)$ .

To construct the factorization, we first observe that since $(c^{\#})$ is a filtered colimit and $H$ is finitary, $(Hc^{\#})$ is a filtered colimit. Therefore, since $X\in{\mathbb{C}}_{\mathrm{fp}}$ , the morphism $q$ factorizes as $q=Hc^{\#}\circ p$ for some $(C,c)\in\operatorname{\mathsf{Coalg}}_{{\mathrm{fp}},{\mathrm{wf}}}(H)$ and $p\colon X\to HC$ . Consider the coproduct extension $(C+X,c_{p})$ of $(C,c)$ by $p$ (Section 3). Note that $(C+X,c_{p})\in\operatorname{\mathsf{Coalg}}_{{\mathrm{fp}},{\mathrm{wf}}}(H)$ because coproduct extension preserves well-foundedness (Proposition 3.6) and ${\mathbb{C}}_{\mathrm{fp}}\hookrightarrow{\mathbb{C}}$ is closed under finite coproducts (Lemma 2.2). It is not difficult to see that $q\colon X\to HT$ satisfies $q=(\,X\xrightarrow{{\mathop{\mathsf{inr}}}}C+X\xrightarrow{c_{p}}H(C+X)% \xrightarrow{Hc_{p}^{\#}}HT\,)$ ; hence $q$ factorizes through $(Hc^{\#}\circ c)$ . $\hfill\blacktriangleleft$

From the “Lambek lemma”, the First Initial Algebra Theorem is immediate:

Proof of Theorem 5.2.

The coalgebra $(T,t)$ is well-founded because it is a colimit of well-founded coalgebras (Proposition 2.19.1), and so it is recursive (Proposition 2.19.2). Clearly, every recursive coalgebra whose structure is an isomorphism is initial as an algebra. $\hfill\blacktriangleleft$

Wißmann and Milius [45] have recently shown an analogue of Theorem 5.2 for recursive instead of well-founded coalgebras. Consider the following modification of Section 5:

Construction 5.4.

Let $(\overline{T},\overline{t})$ be the colimit of all coalgebras in $\operatorname{\mathsf{Coalg}}_{{\mathrm{fp}},{\mathrm{rec}}}(H)$ , i.e. the colimit of the embedding $\overline{D}\colon\operatorname{\mathsf{Coalg}}_{{\mathrm{fp}},{\mathrm{rec}}}% (H)\hookrightarrow\operatorname{\mathsf{Coalg}}(H)$ .

This colimit is filtered because $\operatorname{\mathsf{Coalg}}_{{\mathrm{fp}},{\mathrm{rec}}}(H)$ is finitely cocomplete, using that both ${\mathbb{C}}_{\mathrm{fp}}\hookrightarrow{\mathbb{C}}$ and $\operatorname{\mathsf{Coalg}}_{\mathrm{rec}}(H)\hookrightarrow\operatorname{% \mathsf{Coalg}}(H)$ are closed under finite colimits (Lemma 2.2, Lemma 2.18). It turns out that Section 5 also yields the initial algebra:

Theorem 5.5 (Second Initial Algebra Theorem [45]).

The initial algebra for $H$ is the colimit of all fp-carried recursive coalgebras, that is, the coalgebra structure $\overline{t}\colon\overline{T}\to H\overline{T}$ is an isomorphism and the algebra $(\overline{T},\overline{t}^{-1})$ is initial for $H$ .

We stress that Theorem 5.5 does not need any conditions on ${\mathbb{C}}$ and $H$ beyond those of Section 3. However, in the case where the additional conditions ( $\overset{\smash{\raisebox{-1.0pt}{$\scriptstyle+$}}}{\rightarrowtail}$ ) and ( $H\cap$ ) are satisfied, the first initial algebra theorem can be regarded as an improvement of the second one, as it constructs the initial algebra from a smaller diagram. Indeed, under these conditions well-founded coalgebras form a subclass of recursive ones (Proposition 2.19), and this subclass is generally proper, as witnessed by the coalgebra in Example 3.11.

The idea underlying our proof of Theorem 5.2 carries over easily to the recursive case and leads to a new proof of Theorem 5.5 that is substantially shorter and simpler than the original one [45]. Essentially, the only thing we need to observe is that coproduct extension not only preserves well-foundedness (Proposition 3.6), but also recursivity:

Proposition 5.6.

For every recursive coalgebra $(C,c)$ and every morphism $p\colon X\to HC$ , the coproduct extension $(C+X,c_{p})$ is a recursive coalgebra.

Using this result, we can now proceed exactly like in the proof of Theorem 5.2. First, we establish the “Lambek lemma” for the coalgebra $(\overline{T},\overline{t})$ :

Lemma 5.7.

The coalgebra structure $\overline{t}\colon\overline{T}\to H\overline{T}$ is an isomorphism.

The proof is identical to that of Lemma 5.3, except than one considers $\operatorname{\mathsf{Coalg}}_{{\mathrm{fp}},{\mathrm{rec}}}(H)$ and $\overline{D}$ instead of $\operatorname{\mathsf{Coalg}}_{{\mathrm{fp}},{\mathrm{wf}}}(H)$ and $D$ , and uses Proposition 5.6 to show $(C+X,c_{p})\in\operatorname{\mathsf{Coalg}}_{{\mathrm{fp}},{\mathrm{rec}}}(H)$ .

From the “Lambek lemma”, the Second Initial Algebra Theorem is now again immediate:

Proof of Theorem 5.5.

The coalgebra $(\overline{T},\overline{t})$ is recursive because it is a colimit of recursive coalgebras (Lemma 2.18). Therefore $(\overline{T},\overline{t}^{-1})$ is an initial algebra. $\hfill\blacktriangleleft$

Remark 5.8.

It is instructive to compare Theorem 5.2 and 5.5 with the well-known iterative construction of initial algebras due to Adámek [3]: For every finitary endofunctor $H$ on a cocomplete category ${\mathbb{C}}$ , the initial algebra is the colimit of the $\omega$ -chain

(0,\mathord{\mathchoice{\raisebox{0.0pt}{$\displaystyle% \mathinvertedexclamationmark$}}{\raisebox{0.0pt}{$\textstyle% \mathinvertedexclamationmark$}}{\raisebox{0.0pt}{$\scriptstyle% \mathinvertedexclamationmark$}}{\raisebox{0.0pt}{$\scriptscriptstyle% \mathinvertedexclamationmark$}}})\xrightarrow{\smash{\mathord{\mathchoice{% \raisebox{0.0pt}{$\displaystyle\mathinvertedexclamationmark$}}{\raisebox{0.0pt% }{$\textstyle\mathinvertedexclamationmark$}}{\raisebox{0.0pt}{$\scriptstyle% \mathinvertedexclamationmark$}}{\raisebox{0.0pt}{$\scriptscriptstyle% \mathinvertedexclamationmark$}}}}}(H0,H\mathord{\mathchoice{\raisebox{0.0pt}{$% \displaystyle\mathinvertedexclamationmark$}}{\raisebox{0.0pt}{$\textstyle% \mathinvertedexclamationmark$}}{\raisebox{0.0pt}{$\scriptstyle% \mathinvertedexclamationmark$}}{\raisebox{0.0pt}{$\scriptscriptstyle% \mathinvertedexclamationmark$}}})\xrightarrow{\smash{H\mathord{\mathchoice{% \raisebox{0.0pt}{$\displaystyle\mathinvertedexclamationmark$}}{\raisebox{0.0pt% }{$\textstyle\mathinvertedexclamationmark$}}{\raisebox{0.0pt}{$\scriptstyle% \mathinvertedexclamationmark$}}{\raisebox{0.0pt}{$\scriptscriptstyle% \mathinvertedexclamationmark$}}}}}(HH0,HH\mathord{\mathchoice{\raisebox{0.0pt}% {$\displaystyle\mathinvertedexclamationmark$}}{\raisebox{0.0pt}{$\textstyle% \mathinvertedexclamationmark$}}{\raisebox{0.0pt}{$\scriptstyle% \mathinvertedexclamationmark$}}{\raisebox{0.0pt}{$\scriptscriptstyle% \mathinvertedexclamationmark$}}})\xrightarrow{\smash{HH\mathord{\mathchoice{% \raisebox{0.0pt}{$\displaystyle\mathinvertedexclamationmark$}}{\raisebox{0.0pt% }{$\textstyle\mathinvertedexclamationmark$}}{\raisebox{0.0pt}{$\scriptstyle% \mathinvertedexclamationmark$}}{\raisebox{0.0pt}{$\scriptscriptstyle% \mathinvertedexclamationmark$}}}}}\cdots\xrightarrow{\smash{H^{n-1}\mathord{% \mathchoice{\raisebox{0.0pt}{$\displaystyle\mathinvertedexclamationmark$}}{% \raisebox{0.0pt}{$\textstyle\mathinvertedexclamationmark$}}{\raisebox{0.0pt}{$% \scriptstyle\mathinvertedexclamationmark$}}{\raisebox{0.0pt}{$% \scriptscriptstyle\mathinvertedexclamationmark$}}}}}(H^{n}0,H^{n}\mathord{% \mathchoice{\raisebox{0.0pt}{$\displaystyle\mathinvertedexclamationmark$}}{% \raisebox{0.0pt}{$\textstyle\mathinvertedexclamationmark$}}{\raisebox{0.0pt}{$% \scriptstyle\mathinvertedexclamationmark$}}{\raisebox{0.0pt}{$% \scriptscriptstyle\mathinvertedexclamationmark$}}})\xrightarrow{\smash{H^{n}% \mathord{\mathchoice{\raisebox{0.0pt}{$\displaystyle% \mathinvertedexclamationmark$}}{\raisebox{0.0pt}{$\textstyle% \mathinvertedexclamationmark$}}{\raisebox{0.0pt}{$\scriptstyle% \mathinvertedexclamationmark$}}{\raisebox{0.0pt}{$\scriptscriptstyle% \mathinvertedexclamationmark$}}}}}\cdots

in $\operatorname{\mathsf{Coalg}}(H)$ , where $0$ is the initial object of ${\mathbb{C}}$ and $\mathord{\mathchoice{\raisebox{0.0pt}{$\displaystyle% \mathinvertedexclamationmark$}}{\raisebox{0.0pt}{$\textstyle% \mathinvertedexclamationmark$}}{\raisebox{0.0pt}{$\scriptstyle% \mathinvertedexclamationmark$}}{\raisebox{0.0pt}{$\scriptscriptstyle% \mathinvertedexclamationmark$}}}\colon 0\to H0$ is the unique morphism. Similar to Theorem 5.2 and 5.5, this construction approximates the initial algebra from below: intuitively, one thinks of the initial algebra as the set of all finite trees with branching type $H$ , and of $H^{n}0$ as the set of trees of height less than $n$ . The approximating coalgebras $(H^{n}0,H^{n}\mathord{\mathchoice{\raisebox{0.0pt}{$\displaystyle% \mathinvertedexclamationmark$}}{\raisebox{0.0pt}{$\textstyle% \mathinvertedexclamationmark$}}{\raisebox{0.0pt}{$\scriptstyle% \mathinvertedexclamationmark$}}{\raisebox{0.0pt}{$\scriptscriptstyle% \mathinvertedexclamationmark$}}})$ are recursive [13, Prop. 6], but in contrast to Theorem 5.2 and 5.5, they are generally neither well-founded nor fp-carried.

6 Conclusion and Future Work

We have established two novel results in the theory of well-founded coalgebras over locally finitely presentable categories. Our first contribution is a coalgebraic version of Kőnig’s lemma, lifting a previous result for coalgebras over sets [4] to full categorical generality. We have illustrated the scope of our coalgebraic Kőnig’s lemma by exploring systems with state spaces beyond sets, such as graphs in a topos, and nominal and convex transition systems. As our second contribution, we devised a new construction of the initial algebra for a finitary functor as the colimit of all well-founded coalgebras with finitely presentable state space.

One key application of well-foundedness is termination analysis of programs [15], which amounts to associating cleverly chosen well-founded relations to the state graph of a program. We aim to explore a coalgebraic perspective on termination analysis techniques, in particular in relation with the recent advances in modelling stateful languages as coalgebras [19].

A further interesting route is studying connections between well-founded coalgebras and well-structured transition systems [17], which involve a well-quasi-order on states and provide a uniform framework for a class of decidability results in verification, e.g. for Petri nets.

References

[1] J. Adámek and H.-E. Porst. On tree coalgebras and coalgebra presentations. Theoretical Computer Science, 311(1):257–283, 2004. doi:10.1016/S0304-3975(03)00378-5.
[2] Jirí Adámek, Stefan Milius, and Jirí Velebil. Free iterative theories: a coalgebraic view. Math. Struct. Comput. Sci., 13(2):259–320, 2003. doi:10.1017/S0960129502003924.
[3] Jiří Adámek. Free algebras and automata realizations in the language of categories. Comment. Math. Univ. Carol., 15(4):589–602, 1974.
[4] Jiří Adámek, Stefan Milius, and Lawrence S. Moss. Initial Algebras and Terminal Coalgebras: The Theory of Fixed Points of Functors. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2025. doi:10.1017/9781108884112.
[5] Jiří Adámek, Stefan Milius, Lurdes Sousa, and Thorsten Wißmann. On finitary functors. Theory Appl. Categ., 34(35):1134–1164, October 2019.
[6] Jiří Adámek, Stefan Milius, and Jiří Velebil. Iterative algebras at work. Math. Struct. Comput. Sci., 16(6):1085–1131, 2006. doi:10.1017/S0960129506005706.
[7] Jiří Adámek and Jiří Rosický. Locally Presentable and Accessible Categories. London Mathematical Society Lecture Note Series. Cambridge University Press, 1994. doi:10.1017/CBO9780511600579.
[8] Mikołaj Bojańczyk, Bartek Klin, and Sławomir Lasota. Automata theory in nominal sets. Log. Methods Comput. Sci., 10(3), 2014. doi:10.2168/LMCS-10(3:4)2014.
[9] Filippo Bonchi, Alexandra Silva, and Ana Sokolova. The power of convex algebras. In 28th International Conference on Concurrency Theory (CONCUR 2017), volume 85 of LIPIcs, pages 23:1–23:18. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2017. doi:10.4230/LIPIcs.CONCUR.2017.23.
[10] Filippo Bonchi, Ana Sokolova, and Valeria Vignudelli. The theory of traces for systems with nondeterminism, probability, and termination. Log. Methods Comput. Sci., 18(2), 2022. doi:10.46298/lmcs-18(2:21)2022.
[11] Luitzen E. J. Brouwer. Über Definitionsbereiche von Funktionen. Math. Ann., 97(1):60–75, 1927. doi:10.1007/BF01447860.
[12] Doron Bustan, Sasha Rubin, and Moshe Y. Vardi. Verifying $\omega$ -regular properties of Markov chains. In 16th International on Computer Aided Verification (CAV 2004), volume 3114 of Lect. Notes Comput. Sci., pages 189–201. Springer, 2004. doi:10.1007/978-3-540-27813-9_15.
[13] Venanzio Capretta, Tarmo Uustalu, and Varmo Vene. Recursive coalgebras from comonads. Inf. Comput., 204(4):437–468, 2006. doi:10.1016/J.IC.2005.08.005.
[14] Aurelio Carboni, Stephen Lack, and R.F.C. Walters. Introduction to extensive and distributive categories. J. Pure Appl. Algebra, 84(2):145–158, 1993. doi:10.1016/0022-4049(93)90035-R.
[15] Byron Cook, Andreas Podelski, and Andrey Rybalchenko. Proving program termination. Commun. ACM, 54(5):88–98, 2011. doi:10.1145/1941487.1941509.
[16] Hannes Diener and Hajime Ishihara. Bishop-style constructive reverse mathematics. In Vasco Brattka and Peter Hertling, editors, Handbook of Computability and Complexity in Analysis, pages 347–365. Springer, 2021. doi:10.1007/978-3-030-59234-9_10.
[17] A. Finkel and Ph. Schnoebelen. Well-structured transition systems everywhere! Theor. Comput. Sci., 256(1):63–92, 2001. doi:10.1016/S0304-3975(00)00102-X.
[18] Tomasz Gogacz, Henryk Michalewski, Matteo Mio, and Michał Skrzypczak. Measure properties of game tree languages. In 39th International Symposium on Mathematical Foundations of Computer Science (MFCS 2014), volume 8635 of Lect. Notes Comput. Sci., pages 303–314. Springer, 2014. doi:10.1007/978-3-662-44522-8_26.
[19] Sergey Goncharov, Stefan Milius, Lutz Schröder, Stelios Tsampas, and Henning Urbat. Bialgebraic reasoning on stateful languages, 2025. To appear in 30th ACM SIGPLAN International Conference on Functional Programming (IFCP 2025). doi:10.48550/arXiv.2503.10955.
[20] Denis R. Hirschfeldt. Slicing the Truth: On the Computable and Reverse Mathematics of Combinatorial Principles. World Scientific, 2014. doi:10.1142/9208.
[21] Paul Howard and Jean E. Rubin. Consequences of the Axiom of Choice. American Mathematical Society, 1998. doi:10.1017/S1079898600003449.
[22] Tomasz Idziaszek, Michał Skrzypczak, and Mikołaj Bojańczyk. Regular languages of thin trees. Theory Comput. Syst., 58(4):614–663, 2016. doi:10.1007/S00224-014-9595-Z.
[23] Bart Jacobs. Introduction to Coalgebra: Towards Mathematics of States and Observation. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2016. doi:10.1017/CBO9781316823187.
[24] Thomas Jech. Set Theory: The Third Millennium Edition. Springer, 2002. doi:10.1007/3-540-44761-X.
[25] Peter T Johnstone. Sketches of an elephant. Oxford logic guides. Oxford Univ. Press, New York, NY, 2002. doi:10.1017/S1079898600003462.
[26] Peter T Johnstone. Topos Theory. Dover Publications, 2014.
[27] Michael Kaminski and Nissim Francez. Finite-memory automata. Theor. Comput. Sci., 134(2):329–363, 1994. doi:10.1016/0304-3975(94)90242-9.
[28] Dénes Kőnig. Über eine Schlussweise aus dem Endlichen ins Unendliche. Acta Sci. Math. (Szeged), 3(2-3):121–130, 1927.
[29] Joachim Lambek. A fixpoint theorem for complete categories. Mathematische Zeitschrift, 103:151–161, 1968. doi:10.1007/BF01110627.
[30] Saunders Mac Lane. Categories for the Working Mathematician, volume 5 of Graduate Texts in Mathematics. Springer, 2 edition, 1978. doi:10.1007/978-1-4757-4721-8.
[31] Stefan Milius, Dirk Pattinson, and Thorsten Wißmann. A new foundation for finitary corecursion – the locally finite fixpoint and its properties. In Bart Jacobs and Christof Löding, editors, Proc. 19th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2016), volume 9634 of LNCS, pages 107–125. Springer, April 2016. doi:10.1007/978-3-662-49630-5_7.
[32] Stefan Milius, Dirk Pattinson, and Thorsten Wißmann. A new foundation for finitary corecursion and iterative algebras. Information and Computation, pages 1–28, 2020. Article 104456. doi:10.1016/j.ic.2019.104456.
[33] Stefan Milius, Lutz Schröder, and Thorsten Wißmann. Regular behaviours with names. Applied Categorical Structures, 24(5):663–701, August 2016. doi:10.1007/s10485-016-9457-8.
[34] Matteo Mio, Ralph Sarkis, and Valeria Vignudelli. Combining nondeterminism, probability, and termination: Equational and metric reasoning. In 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2021), pages 1–14, 2021. doi:10.1109/LICS52264.2021.9470717.
[35] Matteo Mio and Valeria Vignudelli. Monads and Quantitative Equational Theories for Nondeterminism and Probability. In 31st International Conference on Concurrency Theory (CONCUR 2020), volume 171 of LIPIcs, pages 28:1–28:18. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2020. doi:10.4230/LIPIcs.CONCUR.2020.28.
[36] Andrew M. Pitts. Nominal Sets: Names and Symmetry in Computer Science. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2013. doi:10.1017/CBO9781139084673.
[37] Jan J. M. M. Rutten. Universal coalgebra: a theory of systems. Theor. Comput. Sci., 249(1):3–80, 2000. doi:10.1016/S0304-3975(00)00056-6.
[38] Ana Sokolova and Harald Woracek. Congruences of convex algebras. Journal of Pure and Applied Algebra, 219(8):3110–3148, 2015. doi:10.1016/j.jpaa.2014.10.005.
[39] Marshall H. Stone. Postulates for the barycentric calculus. Ann. Mat. Pura Appl., 29(1):25–30, 1949. doi:10.1007/BF02413910.
[40] László Székely. Ramsey theory (Lecture notes). https://people.math.sc.edu/laszlo/Ramsey2.pdf, 2023.
[41] Paul Taylor. Practical Foundations of Mathematics. Cambridge Studies in Advanced Mathematics. Cambridge University Press, 1999. doi:10.2307/3621547.
[42] Paul Teller. A Modern Formal Logic Primer: Predicate Logic and Metatheory, Volume II. Prentice Hall, 1989.
[43] Věra Trnková. On descriptive classification of set-functors. I. Comment. Math. Univ. Carol., 12(1):143–174, 1971.
[44] Henning Urbat. Finite Behaviours and Finitary Corecursion. In 7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017), volume 72 of LIPIcs, pages 24:1–24:16. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2017. doi:10.4230/LIPIcs.CALCO.2017.24.
[45] Thorsten Wißmann and Stefan Milius. Initial algebras unchained - A novel initial algebra construction formalized in Agda. In 9th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2024). ACM, 2024. doi:10.1145/3661814.3662105.

[bib.bib1] [1] J. Adámek and H.-E. Porst. On tree coalgebras and coalgebra presentations. Theoretical Computer Science, 311(1):257–283, 2004. doi:10.1016/S0304-3975(03)00378-5.

[bib.bib2] [2] Jirí Adámek, Stefan Milius, and Jirí Velebil. Free iterative theories: a coalgebraic view. Math. Struct. Comput. Sci., 13(2):259–320, 2003. doi:10.1017/S0960129502003924.

[bib.bib3] [3] Jiří Adámek. Free algebras and automata realizations in the language of categories. Comment. Math. Univ. Carol., 15(4):589–602, 1974.

[bib.bib4] [4] Jiří Adámek, Stefan Milius, and Lawrence S. Moss. Initial Algebras and Terminal Coalgebras: The Theory of Fixed Points of Functors. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2025. doi:10.1017/9781108884112.

[bib.bib5] [5] Jiří Adámek, Stefan Milius, Lurdes Sousa, and Thorsten Wißmann. On finitary functors. Theory Appl. Categ., 34(35):1134–1164, October 2019.

[bib.bib6] [6] Jiří Adámek, Stefan Milius, and Jiří Velebil. Iterative algebras at work. Math. Struct. Comput. Sci., 16(6):1085–1131, 2006. doi:10.1017/S0960129506005706.

[bib.bib7] [7] Jiří Adámek and Jiří Rosický. Locally Presentable and Accessible Categories. London Mathematical Society Lecture Note Series. Cambridge University Press, 1994. doi:10.1017/CBO9780511600579.

[bib.bib8] [8] Mikołaj Bojańczyk, Bartek Klin, and Sławomir Lasota. Automata theory in nominal sets. Log. Methods Comput. Sci., 10(3), 2014. doi:10.2168/LMCS-10(3:4)2014.

[bib.bib9] [9] Filippo Bonchi, Alexandra Silva, and Ana Sokolova. The power of convex algebras. In 28th International Conference on Concurrency Theory (CONCUR 2017), volume 85 of LIPIcs, pages 23:1–23:18. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2017. doi:10.4230/LIPIcs.CONCUR.2017.23.

[bib.bib10] [10] Filippo Bonchi, Ana Sokolova, and Valeria Vignudelli. The theory of traces for systems with nondeterminism, probability, and termination. Log. Methods Comput. Sci., 18(2), 2022. doi:10.46298/lmcs-18(2:21)2022.

[bib.bib11] [11] Luitzen E. J. Brouwer. Über Definitionsbereiche von Funktionen. Math. Ann., 97(1):60–75, 1927. doi:10.1007/BF01447860.

[bib.bib12] [12] Doron Bustan, Sasha Rubin, and Moshe Y. Vardi. Verifying $\omega$ -regular properties of Markov chains. In 16th International on Computer Aided Verification (CAV 2004), volume 3114 of Lect. Notes Comput. Sci., pages 189–201. Springer, 2004. doi:10.1007/978-3-540-27813-9_15.

[bib.bib13] [13] Venanzio Capretta, Tarmo Uustalu, and Varmo Vene. Recursive coalgebras from comonads. Inf. Comput., 204(4):437–468, 2006. doi:10.1016/J.IC.2005.08.005.

[bib.bib14] [14] Aurelio Carboni, Stephen Lack, and R.F.C. Walters. Introduction to extensive and distributive categories. J. Pure Appl. Algebra, 84(2):145–158, 1993. doi:10.1016/0022-4049(93)90035-R.

[bib.bib15] [15] Byron Cook, Andreas Podelski, and Andrey Rybalchenko. Proving program termination. Commun. ACM, 54(5):88–98, 2011. doi:10.1145/1941487.1941509.

[bib.bib16] [16] Hannes Diener and Hajime Ishihara. Bishop-style constructive reverse mathematics. In Vasco Brattka and Peter Hertling, editors, Handbook of Computability and Complexity in Analysis, pages 347–365. Springer, 2021. doi:10.1007/978-3-030-59234-9_10.

[bib.bib17] [17] A. Finkel and Ph. Schnoebelen. Well-structured transition systems everywhere! Theor. Comput. Sci., 256(1):63–92, 2001. doi:10.1016/S0304-3975(00)00102-X.

[bib.bib18] [18] Tomasz Gogacz, Henryk Michalewski, Matteo Mio, and Michał Skrzypczak. Measure properties of game tree languages. In 39th International Symposium on Mathematical Foundations of Computer Science (MFCS 2014), volume 8635 of Lect. Notes Comput. Sci., pages 303–314. Springer, 2014. doi:10.1007/978-3-662-44522-8_26.

[bib.bib19] [19] Sergey Goncharov, Stefan Milius, Lutz Schröder, Stelios Tsampas, and Henning Urbat. Bialgebraic reasoning on stateful languages, 2025. To appear in 30th ACM SIGPLAN International Conference on Functional Programming (IFCP 2025). doi:10.48550/arXiv.2503.10955.

[bib.bib20] [20] Denis R. Hirschfeldt. Slicing the Truth: On the Computable and Reverse Mathematics of Combinatorial Principles. World Scientific, 2014. doi:10.1142/9208.

[bib.bib21] [21] Paul Howard and Jean E. Rubin. Consequences of the Axiom of Choice. American Mathematical Society, 1998. doi:10.1017/S1079898600003449.

[bib.bib22] [22] Tomasz Idziaszek, Michał Skrzypczak, and Mikołaj Bojańczyk. Regular languages of thin trees. Theory Comput. Syst., 58(4):614–663, 2016. doi:10.1007/S00224-014-9595-Z.

[bib.bib23] [23] Bart Jacobs. Introduction to Coalgebra: Towards Mathematics of States and Observation. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2016. doi:10.1017/CBO9781316823187.

[bib.bib24] [24] Thomas Jech. Set Theory: The Third Millennium Edition. Springer, 2002. doi:10.1007/3-540-44761-X.

[bib.bib25] [25] Peter T Johnstone. Sketches of an elephant. Oxford logic guides. Oxford Univ. Press, New York, NY, 2002. doi:10.1017/S1079898600003462.

[bib.bib26] [26] Peter T Johnstone. Topos Theory. Dover Publications, 2014.

[bib.bib27] [27] Michael Kaminski and Nissim Francez. Finite-memory automata. Theor. Comput. Sci., 134(2):329–363, 1994. doi:10.1016/0304-3975(94)90242-9.

[bib.bib28] [28] Dénes Kőnig. Über eine Schlussweise aus dem Endlichen ins Unendliche. Acta Sci. Math. (Szeged), 3(2-3):121–130, 1927.

[bib.bib29] [29] Joachim Lambek. A fixpoint theorem for complete categories. Mathematische Zeitschrift, 103:151–161, 1968. doi:10.1007/BF01110627.

[bib.bib30] [30] Saunders Mac Lane. Categories for the Working Mathematician, volume 5 of Graduate Texts in Mathematics. Springer, 2 edition, 1978. doi:10.1007/978-1-4757-4721-8.

[bib.bib31] [31] Stefan Milius, Dirk Pattinson, and Thorsten Wißmann. A new foundation for finitary corecursion – the locally finite fixpoint and its properties. In Bart Jacobs and Christof Löding, editors, Proc. 19th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2016), volume 9634 of LNCS, pages 107–125. Springer, April 2016. doi:10.1007/978-3-662-49630-5_7.

[bib.bib32] [32] Stefan Milius, Dirk Pattinson, and Thorsten Wißmann. A new foundation for finitary corecursion and iterative algebras. Information and Computation, pages 1–28, 2020. Article 104456. doi:10.1016/j.ic.2019.104456.

[bib.bib33] [33] Stefan Milius, Lutz Schröder, and Thorsten Wißmann. Regular behaviours with names. Applied Categorical Structures, 24(5):663–701, August 2016. doi:10.1007/s10485-016-9457-8.

[bib.bib34] [34] Matteo Mio, Ralph Sarkis, and Valeria Vignudelli. Combining nondeterminism, probability, and termination: Equational and metric reasoning. In 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2021), pages 1–14, 2021. doi:10.1109/LICS52264.2021.9470717.

[bib.bib35] [35] Matteo Mio and Valeria Vignudelli. Monads and Quantitative Equational Theories for Nondeterminism and Probability. In 31st International Conference on Concurrency Theory (CONCUR 2020), volume 171 of LIPIcs, pages 28:1–28:18. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2020. doi:10.4230/LIPIcs.CONCUR.2020.28.

[bib.bib36] [36] Andrew M. Pitts. Nominal Sets: Names and Symmetry in Computer Science. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2013. doi:10.1017/CBO9781139084673.

[bib.bib37] [37] Jan J. M. M. Rutten. Universal coalgebra: a theory of systems. Theor. Comput. Sci., 249(1):3–80, 2000. doi:10.1016/S0304-3975(00)00056-6.

[bib.bib38] [38] Ana Sokolova and Harald Woracek. Congruences of convex algebras. Journal of Pure and Applied Algebra, 219(8):3110–3148, 2015. doi:10.1016/j.jpaa.2014.10.005.

[bib.bib39] [39] Marshall H. Stone. Postulates for the barycentric calculus. Ann. Mat. Pura Appl., 29(1):25–30, 1949. doi:10.1007/BF02413910.

[bib.bib40] [40] László Székely. Ramsey theory (Lecture notes). https://people.math.sc.edu/laszlo/Ramsey2.pdf, 2023.

[bib.bib41] [41] Paul Taylor. Practical Foundations of Mathematics. Cambridge Studies in Advanced Mathematics. Cambridge University Press, 1999. doi:10.2307/3621547.

[bib.bib42] [42] Paul Teller. A Modern Formal Logic Primer: Predicate Logic and Metatheory, Volume II. Prentice Hall, 1989.

[bib.bib43] [43] Věra Trnková. On descriptive classification of set-functors. I. Comment. Math. Univ. Carol., 12(1):143–174, 1971.

[bib.bib44] [44] Henning Urbat. Finite Behaviours and Finitary Corecursion. In 7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017), volume 72 of LIPIcs, pages 24:1–24:16. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2017. doi:10.4230/LIPIcs.CALCO.2017.24.

[bib.bib45] [45] Thorsten Wißmann and Stefan Milius. Initial algebras unchained - A novel initial algebra construction formalized in Agda. In 9th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2024). ACM, 2024. doi:10.1145/3661814.3662105.

Well-Founded Coalgebras Meet Kőnig’s Lemma

Abstract

Keywords and phrases:

Funding:

Copyright and License:

2012 ACM Subject Classification:

Related Version:

Acknowledgements:

DOI:

Event:

Editors:

Series and Publisher:

1 Introduction

Coalgebraic Kőnig’s Lemma.

Initial Algebra Theorem.

2 Preliminaries

Locally Finitely Presentable Categories.

Example 2.1 (Filtered Colimits in 𝖲𝖾𝗍).

Lemma 2.2.

Example 2.3 (Locally Finitely Presentable Categories).

Remark 2.4.

Lemma 2.5.

Lemma 2.6.

Lemma 2.7.

Lemma 2.8 ([5, Thm. 3.4]).

Lemma 2.9 ([2, Cor. 2.8]).

Coalgebras and Algebras.

Example 2.10 (Graphs).

Example 2.11 (Automata and Transition Systems).

Lemma 2.12 ([37, Prop. 4.7]).

Lemma 2.13 ([1, Lem. 3.2]).

Example 2.14 (Σ-Algebras).

Well-Founded and Recursive Coalgebras.

Example 2.15 (Graphs).

Example 2.16 (Coalgebras for Set Functors).

Example 2.17 (Graphs).

Lemma 2.18.

Proposition 2.19.

3 Kőnig’s Lemma for Coalgebras

Assumption 3.1.

Remark 3.2.

Remark 3.3.

Construction 3.4 (Coproduct Extension).

Lemma 3.5.

Proposition 3.6 (↣+, H∩).

Proof sketch.

Theorem 3.7 (Coalgebraic Kőnig’s Lemma, ↣+, H∩).

Proof sketch.

Corollary 3.8 (↣+, H∩).

Proof.

Theorem 3.9 (Local Generation Theorem [7, Thm. 1.70]).

Corollary 3.10 (↣+, H∩).

Example 3.11 (Kőnig’s Lemma Fails for Recursive Coalgebras).

4 Applications of the Coalgebraic Kőnig’s Lemma

4.1 Coalgebras for Set Functors

Theorem 4.1 (Kőnig’s Lemma for Coalgebras in 𝖲𝖾𝗍).

4.2 Graphs in a Topos

Lemma 4.2.

Theorem 4.3 (Kőnig’s Lemma for Graphs in a Topos).

4.3 Binary Trees

Theorem 4.4 (Coalgebraic Weak Kőnig’s Lemma).

4.4 Nominal Transition Systems

Theorem 4.5 (Kőnig’s Lemma for Coalgebras in 𝖭𝗈𝗆).

Lemma 4.6.

Theorem 4.7 (Kőnig’s Lemma for Nominal LTS).

4.5 Convex Transition Systems

Lemma 4.8.

Theorem 4.9 (Kőnig’s Lemma for Convex Graphs).

5 Initial Algebras From Finite Well-Founded and Recursive Coalgebras

Construction 5.1.

Theorem 5.2 (First Initial Algebra Theorem, ↣+, H∩).

Lemma 5.3 (↣+, H∩).

Proof sketch.

Proof of Theorem 5.2.

Construction 5.4.

Theorem 5.5 (Second Initial Algebra Theorem [45]).

Proposition 5.6.

Lemma 5.7.

Proof of Theorem 5.5.

Remark 5.8.

Example 2.1 (Filtered Colimits in $\mathsf{Set}$ ).

Example 2.14 ( $\Sigma$ -Algebras).

Proposition 3.6 ( $\overset{\smash{\raisebox{-1.0pt}{$\scriptstyle+$}}}{\rightarrowtail}$ , $H\cap$ ).

Theorem 3.7 (Coalgebraic Kőnig’s Lemma, $\overset{\smash{\raisebox{-1.0pt}{$\scriptstyle+$}}}{\rightarrowtail}$ , $H\cap$ ).

Corollary 3.8 ( $\overset{\smash{\raisebox{-1.0pt}{$\scriptstyle+$}}}{\rightarrowtail}$ , $H\cap$ ).

Corollary 3.10 ( $\overset{\smash{\raisebox{-1.0pt}{$\scriptstyle+$}}}{\rightarrowtail}$ , $H\cap$ ).

Theorem 4.1 (Kőnig’s Lemma for Coalgebras in $\mathsf{Set}$ ).

Theorem 4.5 (Kőnig’s Lemma for Coalgebras in $\mathsf{Nom}$ ).

Theorem 5.2 (First Initial Algebra Theorem, $\overset{\smash{\raisebox{-1.0pt}{$\scriptstyle+$}}}{\rightarrowtail}$ , $H\cap$ ).

Lemma 5.3 ( $\overset{\smash{\raisebox{-1.0pt}{$\scriptstyle+$}}}{\rightarrowtail}$ , $H\cap$ ).