{'fraction_non_alphanumeric': 0.056779484328306346, 'fraction_numerical': 0.008200708874834943, 'mean_word_length': 3.5767175572519085, 'pattern_counts': {'":': 0, '<': 5, '<?xml version=': 0, '>': 6, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 52, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Arboreal Categories: An Axiomatic Theory of Resources

Game comonads provide a categorical syntax-free approach to finite model theory, and their Eilenberg-Moore coalgebras typically encode important combinatorial parameters of structures. In this paper, we develop a framework whereby the essential properties of these categories of coalgebras are captured in a purely axiomatic fashion. To this end, we introduce arboreal categories, which have an intrinsic process structure, allowing dynamic notions such as bisimulation and back-and-forth games, and resource notions such as number of rounds of a game, to be defined. These are related to extensional or"static"structures via arboreal covers, which are resource-indexed comonadic adjunctions. These ideas are developed in a general, axiomatic setting, and applied to relational structures, where the comonadic constructions for pebbling, Ehrenfeucht-Fra\"iss\'e and modal bisimulation games recently introduced by Abramsky et al. are recovered, showing that many of the fundamental notions of finite model theory and descriptive complexity arise from instances of arboreal covers.


Introduction
In previous work ([ADW17, AS18, AS21]), it has been shown how a range of model comparison games which play a central role in finite model theory, including Ehrenfeucht-Fraïssé, pebbling, and bisimulation games, can be captured in terms of resource-indexed comonads on the category of relational structures and homomorphisms. This was done for k-pebble games in [ADW17], and extended to Ehrenfeucht-Fraïssé games, and bisimulation games for the modal fragment, in [AS18]. In subsequent work, this has been further extended to games for generalized quantifiers [D21], guarded fragments of first-order logic [AM21a], hybrid and bounded fragments [AM21b], and bounded conjunction finite variable logic [MS22]. An important feature of this comonadic analysis is that it leads to novel characterisations of important combinatorial parameters such as tree-width and tree-depth. The coalgebras for each of these comonads correspond to certain forms of tree decompositions of structures, with the resource index matching the corresponding combinatorial parameter.
This leads to the question motivating the present paper: Can we capture the significant common elements of these constructions?
Our aim is to develop an elegant axiomatic account, based on clear conceptual principles, which will yield all these examples and more, and allow a deeper and more general understanding of resources.
Conceptually, a key ingredient is the assignment of a process structure-an intensional description-to an extensional object, such as a function, a set, or a relational structure. It is this process structure, unfolding in space and time, to which a resource parameter can be applied, which can then be transferred to the extensional object. At the basic level of computability, this happens when we assign a Turing machine description or a Gödel number to a recursive function. It is then meaningful to assign a complexity measure to the function. The same phenomenon arises in semantics: for example, the notion of sequentiality is applicable to a process computing a higher-order function. Reifying these processes in the form of game semantics led to a resolution of the famous full abstraction problem for PCF [AJM00,HO00], and to a wealth of subsequent results [SIG17].
It is now becoming clear that this phenomenon is at play in the game comonads described in [ADW17, AS18, AS21, D21, AM21a]. They build tree-structured covers of a given, purely extensional relational structure. Such a tree cover will in general not have the full properties of the original structure, but be a "best approximation" in some resource-restricted setting. More precisely, this means that we have an adjunction, yielding the corresponding comonad. The objects of the category where the approximations live have an intrinsic tree structure, which can be captured axiomatically. The tree encodes a process for generating (parts of) the relational structure, to which resource notions can be applied.
In this paper, we make this intuition precise. We introduce a notion of arboreal category, and show how all the examples of game comonads considered to date arise from arboreal covers, i.e. adjunctions between extensional categories of relational structures, and arboreal categories. Importantly, these adjunctions are comonadic, and the categories of coalgebras provide a setting for a general notion of bisimulation, which yields a wide range of logical equivalences in the examples. This notion refines the open maps formulation of bisimulation [JNW93,JNW96] with the condition that the maps are pathwise embeddings, generalizing the ideas introduced in [AS21]. This allows a much wider range of logical equivalences to be captured.
After recalling some preliminary facts on proper factorisation systems in Section 2, we shall develop the axiomatization of paths in Section 3. In Section 4 we introduce open pathwise embeddings and bisimulations, and this leads us to the notion of arboreal category. The latter is defined in Section 5, and in Section 6 we establish the correspondence between bisimulations and back-and-forth equivalences in arboreal categories. Finally, in Section 7, we show how many of the fundamental notions of finite model theory and descriptive complexity arise from instances of arboreal covers. We shall use the concrete constructions in finite model theory as running examples throughout.

Preliminaries
We shall assume familiarity with some standard notions in category theory. All needed background can be found in [AHS04,ML98]. All categories under consideration are assumed to be locally small and well-powered, i.e. every object has a set of subobjects (as opposed to a proper class).
Example 2.1. The extensional categories of primary interest in this paper are categories of relational structures. A relational vocabulary σ is a set of relation symbols R, each with a specified positive integer arity. A σ-structure A is given by a set A, the universe of the structure, and for each R in σ with arity n, a relation R A ⊆ A n . A homomorphism h : A → B is a function h : A → B such that, for each relation symbol R of arity n in σ, for all a 1 , . . . , a n in A, R A (a 1 , . . . , a n ) ⇒ R B (h(a 1 ), . . . , h(a n )). We write Struct(σ) for the category of σ-structures and homomorphisms. The Gaifman graph of a structure A is a graph with vertices A, such that two distinct elements are adjacent if they both occur in some tuple a ∈ R A for some relation symbol R in σ.
2.1. Proper factorisation systems. We recall the notion of weak factorisation system in a category C. Given arrows e and m in C, we say that e has the left lifting property with respect to m, or that m has the right lifting property with respect to e, if for every commutative square as on the left-hand side below there exists a (not necessarily unique) diagonal filler, i.e. an arrow d such that the right-hand diagram above commutes. If this is the case, we write e m. For any class H of morphisms in C, let H (respectively H ) be the class of morphisms having the left (respectively right) lifting property with respect to every morphism in H.
Definition 2.2. A pair of classes of morphisms (Q, M) in a category C is a weak factorisation system provided it satisfies the following conditions: (i) Every morphism f in C can be written as f = m • e with e ∈ Q and m ∈ M.
(ii) Q = M and M = Q . A proper factorisation system is a weak factorisation system (Q, M) such that every arrow in Q is an epimorphism and every arrow in M a monomorphism. A proper factorisation system is stable 1 if, for any e ∈ Q and m ∈ M with common codomain, the pullback of e along m exists and belongs to Q.
factors as A ∼ = Im(m) → B. Taking Q to be the surjective homomorphisms and M to be the embeddings gives a proper factorisation system in Struct(σ). This factorisation system is stable because pullbacks in Struct(σ) are computed in the category of sets and functions, where (surjections, injections) is a stable proper factorisation system. Next, we state some well known properties of weak factorisation systems (cf. [FK72] or [Rie]): Lemma 2.5. Let (Q, M) be a weak factorisation system in C. The following statements hold: (a) Q and M are closed under compositions.
The pullback of an M-morphism along any morphism, if it exists, is again in M. Moreover, if (Q, M) is proper, the following hold for all composable morphisms f, g in C: Throughout this paper, we will refer to M-morphisms as embeddings and denote them by . Q-morphisms will be referred to as quotients and denoted by .
Assume C is a category admitting a proper factorisation system (Q, M). In the same way that one usually defines the poset of subobjects of a given object X ∈ C, we can define the poset of M-subobjects of X. Given embeddings m : S X and n : T X, let us say that m n provided there is a morphism i : S → T such that m = n • i. S X T m i n (Note that, if it exists, i is necessarily an embedding by Lemma 2.5(e).) This yields a preorder on the class of all embeddings with codomain X. The symmetrization ∼ of can be characterised as follows: m ∼ n if, and only if, there exists an isomorphism i : S → T such that m = n•i. Let S X be the class of ∼-equivalence classes of embeddings with codomain X, equipped with the natural partial order ≤ induced by . We shall systematically represent a ∼-equivalence class by any of its representatives. As C is well-powered and every embedding is a monomorphism, we see that S X is a set.
For any morphism f : X → Y and embedding m : S X, we can consider the (Q, M)- (Note that the map ∃ f is well-defined because factorisations are unique up to isomorphism.) Further, if (Q, M) is stable and f is a quotient, we let f * : S Y → S X be the monotone map sending n : T Y to its pullback along f .
Lemma 2.6. Let C be a category equipped with a stable proper factorisation system, and let f : X Y be a quotient in C. The following is an adjoint pair of monotone maps: Proof. This is a well known fact for posets of subobjects, see e.g. [MLM94, Proposition 3 p. 186], and the same reasoning applies in our situation. For the sake of completeness, we provide a detailed proof.
Fix arbitrary embeddings m : S X and n : T Y . We must prove that Since the square on the right-hand side above commutes, there exists a diagonal filler T → ∃ f f * T . Note that this diagonal filler must be both a quotient and an embedding, hence an isomorphism. Therefore, ∃ f f * n = n in S Y .

Path Categories
Throughout this section, we fix a category C equipped with a stable proper factorisation system.
3.1. Paths. If (P, ≤) is a poset, then a subset C ⊆ P is a chain if it is linearly ordered. (P, ≤) is a forest if, for all x ∈ P , the set ↓x := {y ∈ P | y ≤ x} is a finite chain. The height of a forest is the supremum of the cardinalities of its chains. The covering relation ≺ associated with a partial order ≤ is defined by u ≺ v if and only if u < v and there is no w such that u < w < v. It is convenient to allow the empty forest. The roots of a forest are the minimal elements. A tree is a forest with at most one root 2 . Morphisms of forests are maps which preserve roots and the covering relation. Equivalently, a monotone map ϕ : U → V between forests is a forest morphism if, for all u ∈ U , the restriction of ϕ yields a bijection between ↓u and ↓ϕ(u). The category of forests is denoted by F, and the full subcategory of trees by T. We equip these categories with the factorisation system (surjective morphisms, injective morphisms).
Remark 3.1. The factorisation system (surjective morphisms, injective morphisms) in F is obviously proper. Further, this factorisation system is stable and pullbacks of quotients along embeddings are computed in the category of sets and functions. To see this, consider forest morphisms f : F H and g : G H. Let and equip E with the componentwise order. As any injective forest morphism is an orderembedding, for all (x, y), (x , y ) ∈ E we have (x, y) ≤ (x , y ) if and only if x ≤ x . Just observe that x ≤ x entails g(y) = f (x) ≤ f (x ) = g(y ). Thus, E is a forest and the height of an element (x, y) ∈ E coincides with the height of x in F , and thus also with the height of y in G. The following diagram is then readily seen to be a pullback square in F, where π F and π G are the obvious projections. This factorisation system restricts to a stable proper factorisation system in the category T of trees.
Definition 3.2. An object X of C is called a path provided the poset S X is a finite chain. Paths will be denoted by P, Q, R, . . .. Examples 3.4. We define a forest-ordered σ-structure (A, ≤) to be a σ-structure A with a forest order ≤ on A. A morphism of forest-ordered σ-structures f : (A, ≤) → (B, ≤ ) is a σ-homomorphism f : A → B that is also a forest morphism. This determines a category R(σ). We equip R(σ) with the factorisation system given by (surjective morphisms, embeddings), where an embedding is a morphism which is an embedding qua σ-homomorphism.
In [AS21], it is shown that the categories of coalgebras for the various comonads studied there are given, up to isomorphism, by subcategories of R(σ) (or minor variants thereof): • For the Ehrenfeucht-Fraïssé comonad, this is the full subcategory R E (σ) determined by those objects satisfying the condition (E): adjacent elements of the Gaifman graph of A are comparable in the forest order. For each k > 0, R E k (σ) is the full subcategory of R E (σ) of those forest orders of height ≤ k. The objects (A, ≤) of R E k (σ) are forest covers of A witnessing that its tree-depth is ≤ k [NOdM06].
• For the pebbling comonad, for each k > 0 this is the category R P k (σ) whose objects have the form (A, ≤, p), where (A, ≤) is a forest-ordered σ-structure, and p : A → {1, . . . , k} is a pebbling function. In addition to condition (E), these structures have to satisfy the condition (P): if a is adjacent to b in the Gaifman graph of A, and a < b in the forest order, then for all x such that a < x ≤ b, p(a) = p(x). It is shown in [AS21] that these structures are equivalent to the more familiar form of tree decomposition used to define tree-width [Klo94]. Morphisms have to preserve the pebbling function.
• For the modal comonad, the category R M k (σ) has as objects the non-empty tree-ordered σ-structures of height ≤ k satisfying the condition (M): for x, y ∈ A, x ≺ y if and only if for some unique binary relation R α in σ ("transition relation"), R A α (x, y). The paths in each of these categories are those structures in which the order is a finite chain. These are our key motivating examples for paths. Note that in the (multi-)modal case, ignoring propositional variables, these correspond to synchronization trees consisting of a single branch, i.e. traces.
The following fact is an immediate consequence of Lemma 2.7: Lemma 3.5. Let f : X → Y be any morphism in C. The following statements hold: (a) If Y is a path and f is an embedding, then X is a path. (b) If X is path and f is a quotient, then Y is a path.
A path embedding is an embedding P X whose domain is a path. Given any object X of C, we let P X be the sub-poset of S X consisting of the path embeddings. By Lemma 3.5(b), for any arrow f : X → Y , the monotone map ∃ f : S X → S Y restricts to a monotone map By the uniqueness up to isomorphism of factorisations, this assignment is functorial.
3.2. Path categories. We now define the notion of path category. Suppose for a moment that C admits all coproducts of small families of paths. An object X of C is said to be connected if, for all non-empty small families of paths {P i | i ∈ I} in C, any morphism X → i∈I P i factors through some coproduct injection P j → i∈I P i .
Remark 3.6. In category theory, an object a of a locally small category A is usually said to be connected if the functor hom A (a, −), from A into the category of sets and functions, preserves all coproducts that exist in A. The definition that we have given above differs in two aspects: firstly we only consider (non-empty) coproducts of paths, and secondly we do not require that a morphism X → i∈I P i factor through a unique coproduct injection. Note that, unlike with the traditional notion, with our definition the initial object is connected.
Definition 3.7. A path category is a category C, equipped with a stable proper factorisation system, that satisfies the following conditions: (i) C has all coproducts of small families of paths.
(ii) Every path in C is connected.
(iii) For any paths P, Q, R, if a composite P → Q → R is a quotient, then so is P → Q.
Remark 3.8. Item (iii) in the definition of path category is equivalent to the following condition: For any paths P, Q, R and morphisms if any two of f , g, and g • f are quotients, then so is the third. Thus, we shall refer to (iii) as the 2-out-of-3 condition.
To see that the two conditions are equivalent, consider the diagram in equation (3.1) and suppose that item (iii) above holds. If f, g are quotients, then so is g • f by Lemma 2.5(a), and if g • f is a quotient then g is a quotient by Lemma 2.5(d) and f is a quotient by item (iii). Conversely, an application of Lemma 2.5(d) show that item (iii) holds if, whenever any two of f , g, and g • f are quotients, then so is the third.
Note that any path category has an initial object 0, obtained as the coproduct of the empty family.
Examples 3.9. F and T are path categories. Coproducts of forests are given by disjoint union. For trees, coproducts are given by smash sum, with the bottom elements identified. Finite chains are connected in both F and T. Finally, since forest morphisms preserve height, we see that F and T satisfy the 2-out-of-3 condition. A similar reasoning shows that R(σ) and its subcategories mentioned in Example 3.4 are all path categories. Note that coproducts in R(σ) are given by disjoint unions. In particular, R(σ) has an initial object because we allow empty σ-structures.
Theorem 3.10. Let C be a path category. The assignment X → P X induces a functor P : C → T into the category of trees.
To prove this theorem, we start by showing that each poset P X is a tree.
Lemma 3.11. Let C be a path category. For any object X of C, P X is a non-empty tree.
Proof. By Lemmas 2.7(a) and 3.5(a), the sub-poset of P X consisting of those elements that are below a given P ∈ P X is isomorphic to S P . Since the latter is a finite chain, P X is a forest. Now, let 0 0 m X be the (quotient, embedding) factorisation of the unique morphism from the initial object to X. We claim that m : 0 X is the unique root of P X. Note that 0 is a path: just observe that any embedding S 0 admits the unique morphism 0 → S as a right inverse, and thus is a retraction. It follows that S ∼ = 0, i.e., S 0 is the one-element poset. In particular, 0 is a path. Thus, 0 is a path by Lemma 3.5(b). We show that m : 0 X is the least element of P X. If m : P X is any path embedding, we have a commutative square as follows.
Hence there exists a diagonal filler d : 0 → P , and so m ≤ m in P X.
We next show that the functor P sends morphisms in a path category to tree morphisms, thus completing the proof of Theorem 3.10.
Proposition 3.12. Let C be a path category. For any arrow f in C, P f is a tree morphism.
Proof. It is enough to show that, for any path embedding m : P X, the induced map We start by establishing surjectivity, i.e. ↓ P f (m) ⊆ P f (↓m). Let (e, j) be the (quotient, embedding) factorisation of f • m. If n : Q Y is a path embedding such that n ≤ P f (m) in P Y , there exists an embedding k : Q ∃ f P such that the left-hand diagram below commutes. Consider the pullback of k along e, as displayed in the right-hand diagram below.
Then R is a path by Lemmas 2.5(c) and 3.5(a), and the composite i : R P X is a path embedding which is below m in the poset P P . Further, the top horizontal arrow in the pullback square is a quotient and so, by the uniqueness up to isomorphism of factorisations, the (quotient, embedding) factorisation of f For injectivity, let m 1 : P 1 X and m 2 : P 2 X be path embeddings in ↓m. Since P is a path, m 1 and m 2 are comparable in the order of P X. Assume without loss of generality that m 1 ≤ m 2 , i.e., there exists an embedding k : P 1 P 2 such that m 1 = m 2 • k. If P f (m 1 ) = P f (m 2 ), there exists an isomorphism k : ∃ f P 1 → ∃ f P 2 making the left-hand diagram below commute.
In particular, the diagram on the right-hand side above commutes, where the top horizontal arrow is the composition of P 1 ∃ f P 1 with the isomorphism k : ∃ f P 1 → ∃ f P 2 . By the 2-out-of-3 condition, k is an isomorphism, and so m 1 = m 2 in P X.
Remark 3.13. Direct inspection shows that Theorem 3.10 holds, more generally, for any category C (equipped with a stable proper factorisation system) that satisfies condition (iii) in Definition 3.7 and admits an initial object.
We conclude this section with the following useful observation: Lemma 3.14. The following statements hold for any object X of a path category C: (a) Any subset U ⊆ P X admits a supremum U in S X. (b) For any path embedding m ∈ P X and non-empty set S ⊆ S X, if m = S then m ∈ S.
Proof. For item (a), consider a set of path embeddings Let S := i∈I P i be the coproduct in C of the paths P i and consider the (quotient, embedding) factorisation of the unique morphism δ : S → X whose component at P i is m i : Each path embedding m i ∈ U factors through m, thus m is an upper bound for U. We claim that m is the least upper bound, i.e., m = U in S X. Suppose that all path embeddings in U factor through some embedding m : T X. By the universal property of S, we get a morphism ϕ : S → T . By uniqueness of δ we obtain m • ϕ = δ, and so the following square commutes.
S T T X ϕ e m m Therefore, there exists a diagonal filler T → T . In particular, the commutativity of the lower triangle entails that m ≤ m , as was to be proved. For item (b), let m : P X be a path embedding and let S ⊆ S X be a non-empty set such that m = S. Then n ≤ m for each n ∈ S. Since P is a path, ↓m is a finite chain in S X and so S must be a finite set whose largest element coincides with m. In particular, m ∈ S.
Remark 3.15. All results above concerning path categories remain valid if we drop item (ii) in Definition 3.7, stating that every path is connected. For this reason, this condition was not included in the original definition of path category in [AR21]. We do include it here as this allows us to give a conceptually simpler definition of arboreal category, cf. Definition 5.2.

Pathwise Embeddings, Open Maps, and Bisimulations
Throughout this section, we fix a category C equipped with a stable proper factorisation system.

4.1.
Pathwise embeddings and open maps. Following [AS21], let us say that a morphism f : X → Y in C is a pathwise embedding if, for all path embeddings m : P X, the composite f • m is a path embedding. Hence, P f (m) = f • m for all m ∈ P X. Following again [AS21], we introduce a notion of open map-inspired by [JNW93]-that, combined with the concept of pathwise embedding, will allow us to define an appropriate notion of bisimulation. A morphism f : X → Y in C is said to be open if it satisfies the following path-lifting property: Given any commutative square P Q X Y f with P, Q paths, there exists a diagonal filler Q → X (i.e., an arrow Q → X making the two triangles commute). Note that, if it exists, such a diagonal filler must be an embedding.
The previous definition of open map differs from the one given in [JNW93] because we require that, in the square above, the top horizontal morphism and the vertical ones be embeddings. However, the next lemma shows that the two definitions coincide for pathwise embeddings: Lemma 4.1. The following statements are equivalent for any pathwise embedding f : X → Y : (1) f is open.
(2) Given any commutative square Proof. For the non-trivial implication, suppose that (1) holds and consider a commutative square P Q where P and Q are paths. Let (e 1 , m 1 ) and (e 2 , m 2 ) be the (quotient, embedding) factorisations of g 1 and g 2 , respectively. Because e 1 has the left lifting property with respect to m 2 , the diagram on the left-hand side below admits a diagonal filler d : P → Q .
Note that P and Q are paths by Lemma 3.5(b). Further, f • m 1 is an embedding because f is a pathwise embedding, and so d is an embedding by Lemma 2.5(e). As f is open, the square on the right-hand side above admits a diagonal filler k : Q → X. The composite morphism k • e 2 : Q → X is a diagonal filler of diagram (4.1). Just observe that For a pathwise embedding f : X → Y , openness can be characterised in terms of the corresponding morphism of trees P f : P X → P Y : Proposition 4.2. The following statements are equivalent for any pathwise embedding Suppose f is open, and let m : P X be an arbitrary element of P X. The inclusion P f (↑m) ⊆ ↑ P f (m) follows at once from monotonicity of P f . For the converse inclusion, assume that n : Then, the composite f • m must factor through n, say f • m = n • s for some embedding s : P Q. Hence, we have a commutative square as displayed below.
Since f is open, there exists a diagonal filler m : Q X. The commutativity of the upper triangle entails that m ∈ ↑m, while the commutativity of the lower triangle implies that P f (m ) = n. Therefore, ↑ P f (m) ⊆ P f (↑m).
(2) ⇒ (1). Assume P f is a p-morphism and consider a commutative square as follows, where P and Q are paths. We have P f (m) ≤ n in P Y , and thus there exists a path embedding m : P X satisfying m ≤ m and P f (m ) = n. The inequality m ≤ m amounts to saying that m = m • l for some embedding l : P P , while the equality P f (m ) = n means that f • m = n • k for some isomorphism k : P → Q. We have a commutative diagram as displayed below.
and so k • l = s because n is a monomorphism. Now, by diagram chasing we see that This concludes the proof.
If such a bisimulation exists, we say that X and Y are bisimilar.
Examples 4.3. This definition directly generalizes that in [AS21], and the notions of bisimulation given there for the Ehrenfeucht-Fraïssé, pebbling and modal comonads are the special cases arising in the categories R E k (σ), R P k (σ) and R M k (σ) respectively, as described in Example 3.4.
Remark 4.4. Let C be a path category. If we regard trees as Kripke models where the accessibility relation is the tree order, then it follows from Theorem 3.10 and Proposition 4.2 that a span of pathwise embeddings Given a bisimulation X ← Z → Y , we would like to think of Z as providing a winning strategy for Duplicator in an appropriate game played "between X and Y ". To substantiate this idea, in Sections 5 and 6 we introduce arboreal categories-a refinement of the concept of path category-and show that, in these categories, bisimilarity is captured by back-and-forth systems which model the dynamic nature of games.

Arboreal Categories
By Theorem 3.10, any path category C admits a functor P : C → T into the category of trees. In general, the tree P X may retain little information about X. We are interested in the case where X is determined by P X. This leads us to the notion of path-generated object. 5.1. Path-generated objects. Let C be a path category. For any object X of C, we have a diagram with vertex X consisting of all path embeddings with codomain X: The morphisms between paths are those which make the obvious triangles commute. Choosing representatives in an appropriate way, this can be seen as a cocone over the small diagram P X. We say that X is path-generated provided this is a colimit cocone in C. Intuitively, an object is path-generated if it is the colimit of its paths.
Recall that a functor J : where J↓b is the comma category and π is the natural forgetful functor. If C p denotes the full subcategory of C defined by the paths, we have the following observation: Lemma 5.1. The following statements are equivalent for any path category C: (1) Every object of C is path-generated.
(2) The inclusion C p → C is dense.
Proof. Fix an arbitrary object X of C. It suffices to show that X is path-generated precisely when it is the colimit of the diagram where J : C p → C is the inclusion functor. Consider the canonical cocone C with vertex X on the diagram J • π, as depicted on the left-hand side below.
That is, if P = (J • π)(i) for some i ∈ J↓X then η P = i. Take the (quotient, embedding) factorisations of the morphisms in the cocone C, as displayed on the right-hand side above, and note that P and Q are paths by Lemma 3.5(b). Any arrow h : P → Q in the image of the diagram J • π induces an embedding h : P Q making the ensuing diagram commute. Just observe that the following square commutes, and so there is a diagonal filler h : P Q . Now, suppose that X is path-generated and consider a cocone D with vertex Y ∈ C over the diagram J • π. This restricts to a cocone D on the diagram of paths that embed into X and thus, since X is path-generated, induces a unique arrow f : X → Y that is a morphism between the cocones C and D , where C is the restriction of C to the diagram of paths that embed into X. It follows from the observations in the previous paragraph that f is a morphism between the cocones C and D. Just note that, if γ P is the component of D at P , where in the first step we used the naturality of D combined with the fact that e P is the image of the functor J • π. Hence, C is a colimit cocone.
Conversely, suppose that C is a colimit cocone and consider a cocone D with vertex Y ∈ C over the diagram of paths that embed into X. Using the notation introduced in the first paragraph, D can be extended to a cocone D over the diagram J • π by precomposing with the appropriate quotients e P . Naturality of D follows from naturality of D and the fact that e Q • h = h • e P . Thus, there is a unique arrow f : X → Y that is a morphism of cocones between C and D. This clearly induces a morphism from the canonical cocone of path embeddings into X to the cocone D , and uniqueness of this morphism follows from uniqueness of f . Therefore, X is path-generated.

Arboreal categories.
Definition 5.2. An arboreal category is a path category in which every object is pathgenerated.
Equivalently, by Lemma 5.1, an arboreal category is a path category C such that the inclusion C p → C is dense.
Examples 5.3. The category T of trees is arboreal; this is essentially the observation that every tree is the colimit of the diagram given by its branches and the embeddings between them. Similarly, F is arboreal.
Our key examples of the categories R E k (σ), R P k (σ) and R M k (σ) from Example 3.4 are also arboreal.
Note that, in view of Theorem 3.10, any arboreal category C admits a functor P : C → T into the category of trees. This crucial fact is what will allow us, given an arboreal cover (cf. Section 7), to process structures as tree-like objects.
We collect some useful properties of arboreal categories.
Lemma 5.4. Let C be an arboreal category. The following statements hold: (a) Between any two paths there is at most one embedding.
(b) For any object X of C and any m ∈ S X, m = {p ∈ P X | p ≤ m}.
(c) If f is a quotient in C, then P f is a surjection.
Proof. For item (a), since there is at most on tree morphism between any two finite chains, it suffices to show that P : C → T is faithful on embeddings between paths. That is, whenever f, g : P Q are embeddings between paths, P f = P g implies f = g. We show that, in fact, P is faithful on all pathwise embeddings in C. Suppose f, g : X → Y are pathwise embeddings. If P f = P g then, for all path embeddings m : P X, As X is path-generated, it follows that f = g.
For item (b), let m : S X be an arbitrary embedding. Clearly, we have For the converse direction, assume that n : T X is an upper bound for {p ∈ P X | p ≤ m}. This means that each path embedding P X that factors through m must factor through n. To start with, consider the diagram of all path embeddings into X that factor through m, as depicted on the left-hand side below.
Because S is path-generated, the s i 's form a colimit cocone and so m is the unique arrow S → X making the left-hand diagram commute. Now, since each p i factors through n, say p i = n • t i for some t i , and n is a monomorphism, the t i 's form a compatible cocone.
Using again the fact that the s i 's form a colimit cocone, we get a unique mediating arrow γ : S → T making the right-hand diagram above commute. By uniqueness of m we have n • γ = m, and so m ≤ n.
For item (c), suppose that f : X Y is a quotient in C. We first assume that Y = P is a path, and then settle the general case. To show that P f is a surjection, it suffices to prove that id P ∈ P f (P X), where id P : P → P is the identity. We have and so (using the fact that left adjoints preserve suprema) where the first step follows from the fact that ∃ f • f * is the identity of S P (cf. the proof of Lemma 2.7(b)). Hence, id P ∈ P f (P X) by Lemma 3.14(b). For the general case, let m : P Y be an arbitrary path embedding and consider the following pullback square in C.
By the argument above, there is a path embedding n : Q f * P such that P g(n) = id P . It follows that P f (f * m • n) = m. Just observe that the following square commutes, and g • n is a quotient because P g(n) = id P .
Since factorisations are unique up to isomorphism, we conclude that P f (f * m • n) = m.
Let X be an object of an arboreal category. If U is any subset of P X, and n : U X is its supremum in S X, then the downward closure of U is contained in P ( U) (where we identify P ( U) with its image under the order-embedding P n : P ( U) → P X). The next proposition shows that, in fact, P ( U) is equal to the downward closure of U. This will allow us to construct an object from a prescribed set of path embeddings, without adding any new paths in the process.
Proposition 5.5. Let C be an arboreal category, X an object of C, and U ⊆ P X a nonempty subset. A path embedding m ∈ P X is below U if, and only if, it is below some element of U.
Proof. Fix an arbitrary object X of C and a non-empty set of path embeddings U = {m i : P i X | i ∈ I}. Let m : P X be an arbitrary path embedding. If m is below some element of U, then clearly m ≤ U.
For the converse direction, suppose that m ≤ U. Recall from the proof of Lemma 3.14(a) that the supremum of U is obtained by taking the (quotient, embedding) factorisation i∈I P i e − → → S n X of the canonical morphism i∈I P i → X. With this notation, U = n.
Since m ≤ U, there exists an embedding m : P S such that m = n • m . Consider the pullback of m along e: T P i∈I P i S j r m e Applying Lemma 5.4(c) to the quotient r, we see that there exists a path embedding k : Q T such that r • k is a quotient. Because Q is connected, j • k : Q i∈I P i must factor through some coproduct injection ϕ i : P i → i∈I P i , i.e., j • k = ϕ i • p for some path embedding p : Q P . We then have a commutative diagram as follows.
As m • r • k = m i • p and the right-hand side of the equation is an embedding, r • k is an isomorphism. So m ≤ m i ∈ U, thus concluding the proof.
Remark 5.6. Let X be any object of an arboreal category C. Lemma 3.14(a), combined with Lemma 5.4(b), implies that the poset of embeddings S X admits all suprema, hence is a complete lattice. In fact, S X is a perfect lattice.
Recall that an element x of a complete lattice L is completely join-irreducible provided that, for any subset M ⊆ L, x = M entails x ∈ M . A lattice is perfect if it is complete, completely distributive, and each of its elements is a supremum of completely join-irreducible ones. It is well known, cf. [Ran52] or [DP02,Theorem 10.29], that a lattice is perfect precisely when it is isomorphic to the lattice D(P ) of downwards closed subsets of a poset P .
For an object X of an arboreal category, let F be the forest obtained by removing the root from the tree P X. Lemma 5.4(b) and Proposition 5.5 entail that the map S X → D(F ), m → {p ∈ F | p ≤ m} is a bijection, whose inverse sends a downwards closed subset of F to its supremum in S X. Both assignments are clearly monotone, and since any order isomorphism between lattices is a lattice isomorphism, the map above is an isomorphism of (complete) lattices. Thus, in an arboreal category, the lattice of embeddings of any object is isomorphic to the lattice of downwards closed subsets of some forest.

Back-and-Forth Systems and Games
Throughout this section, we work in a fixed arboreal category C. First, we introduce back-and-forth systems in C and show that they capture precisely the bisimilarity relation defined in Section 4 in terms of spans of open pathwise embeddings. Then, we show that back-and-forth systems can be equivalently seen as appropriate back-and-forth games. 6.1. Back-and-forth systems. Given objects X and Y of C, we consider spans of (equivalence classes of) path embeddings of the form X m P n Y . Such a span can be thought of as a partial isomorphism "of shape P " between X and Y . A back-and-forth system between X and Y is a collection of such spans containing an "initial element" and satisfying an appropriate extension property. Let X, Y be any two objects of C. Given m ∈ P X and n ∈ P Y , we write m, n to denote that dom(m) ∼ = dom(n). Observe that (i) any two embeddings in the same ∼-equivalence class have isomorphic domains, and (ii) given m, n , there exist path embeddings m ∼ m and n ∼ n such that dom(m ) = dom(n ). Hence, the pairs of the form m, n capture the partial isomorphisms X m P n Y "of shape P ".
Definition 6.1. A back-and-forth system between objects X, Y of C is a set satisfying the following conditions: where ⊥ X and ⊥ Y are the roots of P X and P Y , respectively.
(ii) If m, n ∈ B and m ∈ P X are such that m ≺ m , there exists n ∈ P Y satisfying n ≺ n and m , n ∈ B. (iii) If m, n ∈ B and n ∈ P Y are such that n ≺ n , there exists m ∈ P X satisfying m ≺ m and m , n ∈ B. A back-and-forth system B is strong if, for all m, n ∈ B and all m ∈ P X, n ∈ P Y , if m ≺ m and n ≺ n then m , n ∈ B.
Two objects X and Y of C are said to be (strong) back-and-forth equivalent if there exists a (strong) back-and-forth system between them.
Remark 6.2. The definition of (strong) back-and-forth system given above is a variant of the notion of (strong) path bisimulation from [JNW96]. The nomenclature adopted here is motivated by the analogy with back-and-forth systems of partial isomorphisms from model theory [Lib04]. Lemma 6.3. Any two objects of an arboreal category are back-and-forth equivalent if, and only if, they are strong back-and-forth equivalent.
Proof. Let X, Y be objects of an arboreal category. For the non-trivial direction, suppose that there exists a back-and-forth system between X and Y . To start with, note that for all m, n ∈ B the height of m in P X coincides with the height of n in P Y . To see this, assume without loss of generality that dom(m) = P = dom(n). Then the chain ↓m of elements of P X that are below m is isomorphic to S P , and similarly for ↓n.
Given m, n ∈ B, suppose that m and n have height k. For every j ∈ {1, . . . , k}, denote by m j and n j the unique path embeddings of height j below m and n, respectively. If m j , n j ∈ B for all j ∈ {1, . . . , k}, the pair m, n is said to be reachable. We claim that B := { m, n ∈ B | m, n is reachable} is a strong back-and-forth system between X and Y .
Item (i) in Definition 6.1 is satisfied because ⊥ X , ⊥ Y belongs to B and is trivially reachable. For item (ii), suppose that m, n ∈ B , and let m ∈ P X satisfy m ≺ m . Since B is a back-and-forth system, there is n ∈ P Y such that n ≺ n and m , n ∈ B. As m, n is reachable, so is m , n . Item (iii) follows by a similar reasoning. Finally, note that B is a strong back-and-forth system by construction.
The aim of this section is to clarify the relation between bisimilarity and back-and-forth equivalence in arboreal categories. While it turns out that any two bisimilar objects X and Y are back-and-forth equivalent, to construct a bisimulation from a back-and-forth system we will assume that the product X × Y exists. For convenience of notation, given any two objects a, b of a category A, let us write a π b to denote that the product a × b exists in A.
The following is our main result on bisimilarity: Theorem 6.4. Let X, Y be any two objects of an arboreal category such that X π Y . Then X and Y are bisimilar if, and only if, they are back-and-forth equivalent.
In particular, in any arboreal category with binary products, the bisimilarity relation coincides with back-and-forth equivalence. This is the case in all our key examples: Examples 6.5. The category T of trees has binary products. These are computed as "synchronous products" consisting of the pairs (x, y) of elements having the same height, with the componentwise order. Similarly, F has binary products, and so does the category R(σ) of forest-ordered σ-structures if the relations in the synchronous product are interpreted componentwise. As synchronous products do not increase the height of forests, we see that the category R E k (σ) from Example 3.4 has binary products. The category R P k (σ) has also finite products, but for these we need to restrict to those pairs (x, y) of elements with same height on which the pebbling functions coincide. Finally, binary products exist in R M k (σ) and can be described again as variants of synchronous products. Alternatively, as pointed out in [AS21], R M k (σ) can be identified with a coreflective subcategory of the category of all pointed Kripke structures. Since the latter is complete, so is R M k (σ). We start by establishing the easy direction of Theorem 6.4. Proposition 6.6. Any two bisimilar objects of an arboreal category are back-and-forth equivalent.
Proof. Suppose that X f ← − Z g − → Y is a span of open pathwise embeddings in an arboreal category C. We claim that is a back-and-forth system between X and Y (in fact, this is a strong back-and-forth system). We show that items (i), (ii) and (iii) in Definition 6.1 are satisfied.
For item (i), let ⊥ Z be the root of P Z. Then P f (⊥ Z ) = ⊥ X and P g(⊥ Z ) = ⊥ Y because tree morphisms preserve roots, and so ⊥ X , ⊥ Y ∈ B.
For item (ii), let P f (m), P g(m) ∈ B and m ∈ P X be such that P f (m) ≺ m . Let us denote P := dom(m) and P := dom(m ). As f • m ≤ m in P X, there exists k : P P such that f • m = m • k in C. Therefore, we have a commutative square as follows.
Since f is open, there is a diagonal filler n : P Z. Thus, m = P f (n) and m , P g(n) ∈ B. It remains to show that P g(m) ≺ P g(n). Note that m ≤ n and P f (m) ≺ P f (n) entail m ≺ n, and so P g(m) ≺ P g(n) because P g preserves the covering relation.
The proof of item (iii) is the same, mutatis mutandis, as for (ii).
Remark 6.7. Suppose for a moment that we define a back-and-forth system between X and Y to consist of spans of path embeddings X P Y , rather than equivalence classes of such path embeddings. Then Proposition 6.6 fails to hold. The reason is that, for a bisimulation need not be a set, in general. Even the notion of strong back-and-forth system would be problematic, as there may be a proper class of path embeddings with codomain P . Of course, in the usual applications the subcategory of paths has a small skeleton, which allows to circumvent this problem.
To establish the other direction of Theorem 6.4, we start by considering a (strong) back-and-forth system B = { m i , n i | i ∈ I} between X and Y , and attempt to construct an object Z and a span of open pathwise embeddings X ← Z → Y . Intuitively, Z is obtained by gluing together the paths P i := dom(m i ), for i ∈ I, by taking a colimit in C. If the product of X and Y exists in C, then this colimit can be equivalently described as the supremum of a set of path embeddings as we now explain.
Consider an arbitrary m i , n i ∈ B and assume without loss of generality that dom(m i ) = P i = dom(n i ) for some path P i . Then the product arrow m i , n i : P i → X × Y is an embedding. In fact, it suffices that m i be an embedding (or, symmetrically, that n i be an embedding), for then m i = π X • m i , n i entails that m i , n i is an embedding, where π X : X × Y → X is the projection. Therefore, we can identify each m i , n i ∈ B with a path embedding m i , n i ∈ P (X × Y ) and compute the supremum m : Z X × Y in S (X × Y ) of all these path embeddings. Note that the assignment does not depend on the choice of the representatives in the equivalence classes of m i and n i . We note in passing the following immediate fact: be a back-and-forth system between X and Y . If To show that the span X is a bisimulation, we exploit the fact that Z does not admit more path embeddings than those prescribed (cf. Proposition 5.5). The following proposition then completes the proof of Theorem 6.4: Proposition 6.9. Let X and Y be any two objects of an arboreal category such that X π Y . If X and Y are back-and-forth equivalent, then they are bisimilar.
Proof. Let C be an arboreal category, and let X, Y be any two back-and-forth equivalent objects of C admitting a product X × Y . By Lemma 6.3, there is a strong back-and-forth system B = { m i , n i | i ∈ I} between X and Y . Consider the set is a bisimulation between X and Y .
To see that this is a span of pathwise embeddings, consider an arbitrary path embedding n : P Z. In view of Proposition 5.5 and Lemma 6.8, m • n ∈ U. That is, m • n = m i , n i in P (X × Y ) for some m i , n i ∈ B. It follows that m • n = m i , n i • ϕ in C for some isomorphism ϕ, and so π X • m • n and π Y • m • n are embeddings because π X • m • n = m i • ϕ and π Y • m • n = n i • ϕ.
It remains to show that π X • m and π Y • m are open. We prove that π X • m is open; the proof for π Y • m follows by symmetry. Consider a commutative square in C as displayed below, where P and Q are paths.
Reasoning as above, we see that m • n = m i , n i in P (X × Y ) for some m i , n i ∈ B. Therefore, in P X, we have m i = π X • m • n ≤ m j . Applying item (ii) in Definition 6.1 (possibly finitely many times), it follows that there exists n j ∈ P Y such that n i ≤ n j and m j , n j ∈ B. Suppose without loss of generality that dom(m j ) = dom(n j ). Then m j , n j ∈ U and so m j , n j : Q X × Y factors through the supremum m : Z X × Y of U. That is, m j , n j = m • h in C for some morphism h : Q → Z. We claim that the following diagram commutes, thus establishing that π X • m is open.
For the commutativity of the lower triangle, just observe that Now, assume without loss of generality that dom(m i ) = R = dom(n i ) for some path R. As already observed above, m • n = m i , n i in P (X × Y ) implies that m • n = m i , n i • ϕ in C for some isomorphism ϕ : P → R. Thus, for the upper triangle, we have where in the first step we used the fact that m is a monomorphism. In turn, the inequalities m i ≤ m j and n i ≤ n j entail the existence of embeddings k 1 , k 2 : R Q such that m i = m j •k 1 and n i = n j •k 2 . By Lemma 5.4(a) we have k 1 •ϕ = k = k 2 •ϕ. It follows that m i •ϕ = m j •k and n i • ϕ = n j • k, and so n = h • k.
6.2. Back-and-forth games. Let C be an arboreal category and let X, Y be any two objects of C. We define a back-and-forth game G(X, Y ) played by Spoiler and Duplicator on X and Y as follows. Positions in the game are pairs of (equivalence classes of) path embeddings (m, n) ∈ P X × P Y . The winning relation W(X, Y ) ⊆ P X × P Y consists of the pairs (m, n) such that dom(m) ∼ = dom(n).
Let ⊥ X : P X and ⊥ Y : Q Y be the roots of P X and P Y , respectively. If P ∼ = Q, then Duplicator loses the game. Otherwise, the initial position is (⊥ X , ⊥ Y ). At the start of each round, the position is specified by a pair (m, n) ∈ P X × P Y , and the round proceeds as follows: Either Spoiler chooses some m m and Duplicator must respond with some n n, or Spoiler chooses some n n and Duplicator must respond with m m. Duplicator wins the round if they are able to respond and the new position is in W(X, Y ). Duplicator wins the game if they have a strategy which is winning after t rounds, for all t ≥ 0.
Examples 6.10. It is shown in [AS21] that the abstract game G(X, Y ) restricts, in the case of the arboreal categories R E k (σ), R P k (σ) and R M k (σ), to the usual k-round Ehrenfeucht-Fraïssé, k-pebble and k-round bisimulation games, respectively.
The following straightforward observation makes precise the translation between backand-forth systems and back-and-forth games.
Lemma 6.11. Two objects X, Y of an arboreal category C are back-and-forth equivalent if, and only if, Duplicator has a winning strategy in the game G(X, Y ).
Proof. Clearly, if B = { m i , n i | i ∈ I} is a back-and-forth system between X and Y , then the plays in the set {(m i , n i ) | i ∈ I} ⊆ P X × P Y yield a winning strategy for Duplicator in the game G(X, Y ).
Conversely, a winning strategy for Duplicator in the game G(X, Y ) determines a set W ⊆ W(X, Y ) of the plays following this strategy, and is a back-and-forth system. In fact, B is even strong because W is downwards closed in the (synchronous) product of trees P X × P Y .
The previous lemma, combined with Theorem 6.4, yields at once the following result: Theorem 6.12. Let X, Y be objects of an arboreal category such that X π Y . Then X and Y are bisimilar if, and only if, Duplicator has a winning strategy in the game G(X, Y ).
We record an easy but useful consequence 3 of the previous theorem: Corollary 6.13. In an arboreal category, suppose that X π Y , Y π Z and X π Z. If X and Y , and Y and Z, are bisimilar, then so are X and Z.
Proof. This is a consequence of Theorem 6.12. Just observe that, if Duplicator has a winning strategy for the games G(X, Y ) and G(Y, Z), then the composition of these strategies is a winning strategy for the game G(X, Z).
In more detail, let ⊥ X , ⊥ Y and ⊥ Z be the roots of P X, P Y and P Z, respectively. Then and so (⊥ X , ⊥ Z ) ∈ W(X, Z). After i rounds of the game, the position is given by a pair (m, p) ∈ P X × P Z. By inductive hypothesis, we can assume that there exists n ∈ P Y such that (m, n) ∈ W(X, Y ) and (n, p) ∈ W(Y, Z). Suppose that, in the following round, Spoiler chooses some m m. Following their winning strategies for the games G(X, Y ) and G(Y, Z), Duplicator can find n n and p p such that (m , n ) ∈ W(X, Y ) and (n , p ) ∈ W(Y, Z), and so (m , p ) ∈ W(X, Z). Therefore, Duplicator will respond with p . If Spoiler chooses some p p, the argument is the same, mutatis mutandis.
Remark 6.14. In view of Corollary 6.13, bisimilarity is an equivalence relation in any arboreal category admitting binary products.
There is also an existential positive version of the game G(X, Y ), denoted by ∃ + G(X, Y ), where Spoiler always plays in P X, and Duplicator always responds in P Y . The winning relation W(X, Y ) ⊆ P X × P Y consists of the pairs (m, n) such that there exists a morphism dom(m) → dom(n).
Proposition 6.15. Let C be an arboreal category and let X, Y be any two objects of C. If P : C → T is faithful, then Duplicator has a winning strategy in the game ∃ + G(X, Y ) if, and only if, there exists a morphism X → Y .
Proof. Suppose that there exists a morphism f : X → Y in C. As P f is a tree morphism, is a winning strategy for Duplicator in the game ∃ + G(X, Y ). Conversely, we show that a winning strategy for Duplicator in the game ∃ + G(X, Y ) determines a cocone with vertex Y over the diagram of paths that embed into X. Since X is path-generated, this cocone induces a morphism X → Y . We explain in detail how the cocone with vertex Y is constructed.
Fixing representatives, we can regard P X as a cocone in C over a small diagram D consisting of paths and path embeddings. For a generic path embedding m : P X in D, the cocone E = {e m : P → Y | m ∈ D} is defined as follows: (i) For the base case, suppose that m = ⊥ X : P X is the root of P X, and let (ii) Assume that e m has been defined whenever m ∈ D has height at most k in P X, and pick any m ∈ D of height k + 1. Then there exists m ∈ D such that m ≺ m . By inductive hypothesis, we have e m = n • h for some n ∈ P Y satisfying (m, n) ∈ W(X, Y ). Thus, there is n ∈ P Y such that n ≺ n and (m , n ) ∈ W(X, Y ). If h : dom(m ) → dom(n ) is any morphism in C, we let e m := n • h . The compatibility condition for the cocone E states that, for all m, m ∈ D with m ≤ m , e m extends e m ; an easy inductive argument shows that it suffices to settle the case where m ≺ m . If P : C → T is faithful, then the full subcategory C p of C defined by the paths is a preorder. Just observe that there is at most one tree morphism between any two finite chains. Therefore, any diagram in C p is commutative. Suppose that e m = n • h and e m = n • h are as in item (ii) above. Because m ≺ m , there exists an embedding dom(m) dom(m ). Moreover, n ≺ n entails the existence of an embedding dom(n) dom(n ) making the rightmost triangle below commute.
Since the leftmost rectangle is a diagram in C p , it must commute. We conclude that e m extends e m .
Examples 6.16. In the case of the arboreal categories R E k (σ), R P k (σ) and R M k (σ), it follows from their description in Example 3.4 that the functor P is faithful. In that case, the abstract existential positive game ∃ + G(X, Y ) restricts, respectively, to the asymmetric (forth only) versions of the k-round Ehrenfeucht-Fraïssé, k-pebble and k-round bisimulation games.
Remark 6.17. Direct inspection of the proof of Proposition 6.15 shows that the assumption that P : C → T is faithful can be replaced with the weaker condition that there is at most one arrow between any two paths of C.
Finally, we introduce a third type of game which sits in between G(X, Y ) and ∃ + G(X, Y ). The existential game ∃ G(X, Y ) has the same winning relation as the game G(X, Y ), but Spoiler always plays in P X and Duplicator always responds in P Y .
Proposition 6.18. Let C be an arboreal category and let X, Y be any two objects of C. Duplicator has a winning strategy in the game ∃ G(X, Y ) if, and only if, there exists a pathwise embedding X → Y .
Proof. If f : X → Y is a pathwise embedding, then the set in equation (6.1) is a winning strategy for Duplicator in the game ∃ G(X, Y ). Just observe that, since f is a pathwise embedding, for all m ∈ P X we have P f (m) = f • m and so dom(m) = dom(P f (m)).
For the other direction, suppose that Duplicator has a winning strategy in the game ∃ G(X, Y ). We proceed as in the proof of Proposition 6.15 and define a cocone over the diagram D of paths that embed in X. This time, all the morphisms e m will be embeddings, and so the induced morphism X → Y will be a pathwise embedding.
(i) For the base case, suppose that m = ⊥ X : P X is the root of P X, and let ⊥ Y : Q Y be the root of P Y . As (⊥ X , ⊥ Y ) ∈ W(X, Y ), we have P ∼ = Q. Upon identifying P and Q, we set e m := ⊥ Y .
(ii) Assume that e m has been defined whenever m ∈ D has height at most k in P X, and pick any m ∈ D of height k + 1. Then there exists m ∈ D such that m ≺ m . By inductive hypothesis, we have (m, e m ) ∈ W(X, Y ). Thus, there is n ∈ P Y such that e m ≺ n and (m , n ) ∈ W(X, Y ). Let e m := n . Upon composing with an appropriate isomorphism, we can assume that dom(m ) = dom(e m ). To verify the compatibility condition for the cocone E, it suffices to show that for all m, m ∈ D, if m ≺ m in P X then e m ≺ e m in P Y . In turn, this follows by the definition of E.
Examples 6.19. What does the existential game ∃ G(X, Y ) correspond to in concrete cases? For instance, in the case of the arboreal categories R E k (σ) and R P k (σ), the game ∃ G(X, Y ) restricts to one-way versions of the k-round Ehrenfeucht-Fraïssé and k-pebble games, respectively, in which the winning condition is that the ensuing relation is a partial isomorphism. For pebble games, this variant of the game was considered e.g. in [Ros95,Proposition 3], where it is shown to capture the existential fragment of k-variable logic. Similarly, for the k-round Ehrenfeucht-Fraïssé games, it captures the existential fragment of first-order logic with quantifier-rank at most k.
We conclude this section with an application of the games introduced above. In Section 7, we shall see that the following lemma is an abstraction of the (trivial) observation that any two σ-structures that are equivalent in a logic L are also equivalent in the existential (positive) fragment of L, cf. Theorem 7.15. Let us say that two objects X, Y in a category are homomorphically equivalent if there exist morphisms X → Y and Y → X (these need not satisfy any further property).
Lemma 6.20. Let X, Y be bisimilar objects of an arboreal category. Then there exist pathwise embeddings X → Y and Y → X. In particular, X and Y are homomorphically equivalent.
Proof. This follows directly from Lemma 6.11 and Propositions 6.6 and 6.18. Just observe that, if Duplicator has a winning strategy in the game G(X, Y ), then they have a winning strategy in the existential game ∃ G(X, Y ).

Arboreal Covers
We now return to the underlying motivation for the axiomatic development in this paper. Arboreal categories have a rich intrinsic process structure, which allows "dynamic" notions such as bisimulation and back-and-forth games, and resource notions such as the height of a tree, to be defined. A key idea is to relate these process notions to extensional, or "static" structures. In particular, much of finite model theory and descriptive complexity can be seen in this way.
In the general setting, we have an arboreal category C, and another category E, which we think of as the extensional category.
Definition 7.1. An arboreal cover of E by C is given by a comonadic adjunction As for any adjunction, this induces a comonad on E. The comonad is (G, ε, δ), where G := LR, ε is the counit of the adjunction, and δ a : LRa → LRLRa is given by δ a := L(η Ra ), with η the unit of the adjunction. The comonadicity condition states that the Eilenberg-Moore category of coalgebras for this comonad is isomorphic to C. The idea is then that we can use the arboreal category C, with its rich process structure and all the associated notions, to study the extensional category E via the adjunction. Both the co-Kleisli category of the comonad, and the full Eilenberg-Moore category, are useful in this regard.
We now bring resources into the picture.
Proposition 7.6. Let {C k } be a resource-indexed arboreal category. Then C k is an arboreal category for each k.
Proof. If C is equipped with the stable proper factorisation system (Q, M), consider the classes of morphisms Q := Q ∩ C k and M := M ∩ C k . Then (Q , M ) is a proper factorisation system in C k . Just observe that, whenever W → Y is a morphism in C k and W X Y is its (quotient, embedding) factorisation in C, then X ∈ C k by Lemma 7.5. Using again Lemma 7.5, along with the fact that embeddings are stable under pullbacks, it follows at once that (Q , M ) is stable (and, in fact, pullbacks of Q -morphisms along M -morphisms are computed in C).
We claim that, with respect to this factorisation system, the paths in C k are precisely the objects of C k p . It follows by Lemma 7.5 that, for all objects X of C k , the poset of embeddings of X in C k is isomorphic to the poset of embeddings of X in C. Thus, an object of C k is path in C k if, and only if, it is a path in C. In particular, the objects of C k p are paths in C k . Conversely, suppose that P is a path in C k . Applying Lemma 7.4 to the identity arrow P → P we see that P ∈ C k p . Next, we show that C k satisfies the conditions in the definition of path category. The category C k satisfies the 2-out-of-3 condition because C does. Moreover, C k has all coproducts of small families of paths, and they are computed in C. To see this, consider a set of paths {P i ∈ C k p | i ∈ I} and their coproduct i∈I P i in C. If I = ∅ then i∈I P i is initial in C and thus belongs to C k p , hence also to C k . Suppose that I = ∅. If m : P i∈I P i is any path embedding in C then, because P is connected, m must factor through some coproduct injection. In particular, there exist i ∈ I and an embedding P P i . Since P i ∈ C k p , we get P ∈ C k p . As i∈I P i is path-generated in C, it follows at once that i∈I P i ∈ C k . Hence, i∈I P i coincides with the coproduct of the family {P i ∈ C k p | i ∈ I} in C k . This shows that C k is a path category. Further, every object of C k is path-generated by construction, and paths in C k are connected because any path in C k is also a path in C and, as observed above, coproducts of paths in C k are computed in C. Therefore, C k is an arboreal category.
Definition 7.7. Let {C k } be a resource-indexed arboreal category. We define a resourceindexed arboreal cover of E by C to be an indexed family of comonadic adjunctions Examples 7.8.
Our key examples arise by taking the extensional category E to be Struct(σ).
For each k > 0, there are evident forgetful functors L E k : R E k (σ) → Struct(σ), L P k : R P k (σ) → Struct(σ) which forget the forest order, and in the case of R P k (σ), also the pebbling function. These functors are both comonadic over Struct(σ). The right adjoints build a forest over a structure A by forming sequences of elements over the universe A, suitably labelled and with the σ-relations interpreted so as to satisfy the conditions (E) and (P) respectively. In the modal logic case, the extensional category E is the category Struct (σ) of pointed σ-structures with morphisms the σ-homomorphisms preserving the distinguished point. There is a forgetful functor (A, a), where a is the unique root of (A, ≤). This functor is comonadic and its right adjoint sends a pointed σ-structure (A, a) to the tree-ordered structure obtained by unravelling the structure A, starting from a, to depth k, and with the σ-relations interpreted so as to satisfy the condition (M).
These constructions yield the comonads described concretely in [ADW17,AS21]. The sequences correspond to plays in the Ehrenfeucht-Fraïssé, pebbling and modal bisimulation games respectively.
Remark 7.9. In all our examples, the adjunctions L k R k in the definition of a resourceindexed arboreal cover satisfy an additional compatibility property. In fact, if k ≤ l and F k,l : C k → C l denotes the inclusion functor, then L k = L l • F k,l . Further, in our key examples the functors F k,l have right adjoints G k,l : C l → C k by (the dual of) Freyd's special adjoint functor theorem (cf. e.g. [ML98, §V.8]), and R k = G k,l • R l . However, as these properties are not necessary to develop the general theory of resource-indexed arboreal covers, we shall not assume them.
We now show how resource-indexed arboreal covers can be used to define important notions on the extensional category. For a resource-indexed arboreal cover of E by C, with adjunctions L k R k and comonads G k , we define four resource-indexed relations on objects of E.
Definition 7.10. Consider a resource-indexed arboreal cover of E by C, and any two objects a, b of E. For all k > 0, we define: In view of Lemma 6.20, we have the following chain of inclusions between these relations: Remark 7.11. The relations C k and ∼ = C k can equivalently be defined in terms of the co-Kleisli category of G k . In fact, a C k b if, and only if, there are co-Kleisli morphisms G k a → b and G k b → a, and a ∼ = C k b precisely when a and b are isomorphic in the co-Kleisli category of G k . However, the relations C k and ↔ C k require working in the Eilenberg-Moore category. Note that C k , C k and ∼ = C k are always equivalence relations (for the second one, just observe that the composition of pathwise embeddings is a pathwise embedding). Further, ↔ C k is transitive, thus an equivalence relation, whenever E has binary products. Just observe that, since right adjoints preserve limits, the product of R k a and R k b in C k exists and can be identified with R k (a × b). Hence, transitivity of ↔ C k follows from Corollary 6.13. Remark 7.12. Under the assumptions of Definition 7.10, we can define a coarsening of the relation C k , namely the preorder → C k defined by a → C k b if, and only if, there is a morphism R k a → R k b in C k (equivalently, a co-Kleisli morphism G k a → b). The equivalence relation C k then coincides with the symmetrisation of → C k . A similar reasoning applies to C k .
The equivalence relations C k and C k can be characterised using the (forth only) games ∃ + G and ∃ G, respectively.
Proposition 7.13. Consider a resource-indexed arboreal cover of E by C. The following statements are equivalent for all objects a, b of E: (1) a C k b.
(2) Duplicator has a winning strategy in the games ∃ G(R k a, R k b) and ∃ G(R k b, R k a). Moreover, whenever P : C k → T is faithful, the following statements are equivalent: (3) a C k b. (4) Duplicator has a winning strategy in the games ∃ + G(R k a, R k b) and ∃ + G(R k b, R k a).
Proof. In view of Proposition 7.6, the categories C k are arboreal. Therefore, the equivalences in the statement follow by Propositions 6.18 and 6.15, respectively.
Similarly, the relation ↔ C k can be characterised in terms of the back-and-forth game G, or equivalently in terms of back-and-forth systems.
Proposition 7.14. Consider a resource-indexed arboreal cover of E by C, and assume that E admits binary products. The following statements are equivalent for all objects a, b of E: (2) R k a and R k b are back-and-forth equivalent.
(3) Duplicator has a winning strategy in the game G(R k a, R k b).
Proof. This follows directly from Theorems 6.4 and 6.12, and Proposition 7.6.
What do these notions mean in Example 7.8? For each of our three types of model comparison game, there are corresponding fragments L k of first-order logic without equality 5 [Lib04, BDRV02]: • For Ehrenfeucht-Fraïssé games, L k is the fragment of quantifier-rank at most k.
• For pebble games, L k is the k-variable fragment.
• For bisimulation games, L k is the modal fragment with modal depth at most k. In each case, we write ∃L k for the existential fragment of L k , ∃ + L k for the existential positive fragment of L k , and L k (#) for the extension of L k with counting quantifiers [Lib04]. For each logic L, there is the usual equivalence on σ-structures: A ≡ L B if and only if, for all ϕ in L, A |= ϕ ⇐⇒ B |= ϕ.
We now have the following result from [AS21] (for the existential fragment ∃L k , this follows by a reasoning similar to the one in op. cit.): Theorem 7.15. The following statements hold for all σ-structures A and B: Note that this is really a family of four theorems, one for each type of game arising from a resource-indexed arboreal cover C as in Example 7.8. Thus in each case, we capture the salient logical equivalences in syntax-free, categorical form.
We return to the general setting. Given a resource-indexed arboreal cover of E by C, we know by comonadicity that for each k, C k is isomorphic to the Eilenberg-Moore category of coalgebras for the comonad G k . For each object a of E, we can ask if it carries a G k -coalgebra structure; that is, whether there is a morphism α : a → G k a satisfying the G k -coalgebra conditions. Moreover, we can ask for the least k such that this is the case. We call this the coalgebra number of a.
The intuition behind this, as explained in [ADW17,AS21], is that the resource parameter is bounding access to the structure, meaning that the lower the value of k, the more difficult it is to have a morphism in E with codomain G k a. So the least k for which this is possible is a significant invariant of the structure. This intuition is born out by the following result from [ADW17, AS21].
Theorem 7.16. The following statements hold: (a) For the Ehrenfeucht-Fraïssé comonad, the coalgebra number of A corresponds precisely to the tree-depth of A. (b) For the pebbling comonad, the coalgebra number of A corresponds precisely to the tree-width of A. (c) For the modal comonad, the coalgebra number of A corresponds precisely to the modal unfolding depth of A.
What underlies these results is the comonadicity of the arboreal covers, which means that the coalgebras are witnesses for the various forms of tree decompositions of structures in E corresponding to these combinatorial invariants. 7.1. Arboreal adjunctions. Consider the Ehrenfeucht-Fraïssé resource-indexed arboreal cover {R E k (σ)} of Struct(σ). In view of Theorem 7.15, the equivalence relation ↔ R E k on Struct(σ) captures precisely equivalence in first-order logic without equality and with quantifier rank at most k. In this section, following [AS21], we show how to capture first-order logic with equality and quantifier rank at most k, denoted by FO k . Let σ I := σ ∪ {I} be the vocabulary obtained by adding a new binary relation symbol I to σ. There is an associated Ehrenfeucht-Fraïssé resource-indexed arboreal cover of Struct(σ I ): Any σ-structure can be expanded to a σ I -structure by interpreting I as the identity relation. This yields a full and faithful functor J : Struct(σ) → Struct(σ I ). The functor J has a left adjoint H : Struct(σ I ) → Struct(σ) which sends a σ I -structure A to the quotient of the σ-reduct of A with respect to the equivalence relation generated by I A (see [DJR21, Lemma 25]). We can then compose the adjunction H J with the resource-indexed arboreal cover above.
The ensuing adjunction HL I k R I k J between Struct(σ) and R E k (σ I ) is not comonadic. For this reason, we need to relax the definition of resource-indexed arboreal cover by removing the comonadicity assumption: Definition 7.17. Let {C k } be a resource-indexed arboreal category. A resource-indexed arboreal adjunction between E and C is an indexed family of adjunctions with corresponding comonads G k on E.
Definition 7.10 (see also Remark 7.12), which associates with each resource-indexed arboreal cover four relations on the extensional category, extends to any resource-indexed arboreal adjunction in the obvious manner. We have the following easy yet useful observations: Lemma 7.18. The following statements hold for any resource-indexed arboreal adjunction between E and C, with adjunctions L k R k and comonads G k , and all objects a, b of E: (a) a C k G k a, for all k > 0. (b) If there exists a morphism a → b, then a → C k b for all k > 0. Proof. For item (a), reasoning in the co-Kleisli category (cf. Remark 7.11), we must exhibit two co-Kleisli morphisms G k a → G k G k a and G k G k a → G k a. The comultiplication of the comonad G k yields an arrow δ a : G k a → G k G k a, while the image under G k of the counit ε a : G k a → a yields an arrow G k G k a → G k a.
For item (b), if there is an arrow a → b in E then we can simply take its image under R k to obtain an arrow R k a → R k b. By definition (see Remark 7.12), we have a → C k b. For the Ehrenfeucht-Fraïssé resource-indexed arboreal adjunction between Struct(σ) and R E k (σ I ), see equation (7.1), we obtain equivalence relations on Struct(σ) that we shall denote by I k , I k , ↔ I k and ∼ = I k . The relation ↔ I k captures precisely equivalence of σ-structures in first-order logic with equality and quantifier rank at most k, see [AS21, Theorem 10.5]. That is, for all σ-structures A, B, A ↔ I k B ⇐⇒ A ≡ FO k B. Remark 7.19. The paths in the category R E k (σ I ) are those finite σ I -structures carrying a linear order (note that linear orders automatically satisfy condition (E) in Example 3.4). In [AS21], the bisimilarity relation ↔ I k is defined with respect to a smaller collection of paths, namely those linearly ordered finite σ I -structures in which the relation I is interpreted as the identity. Nonetheless, these two choices of paths give rise to the same notion of bisimilarity; for more details, see [JR22].