# Arboreal Categories and Homomorphism Preservation Theorems

Samson Abramsky  Department of Computer Science, University College London,
66–72 Gower Street, London, WC1E 6EA, United Kingdom<EMAIL_ADDRESS>and
Luca Reggio  Department of Computer Science, University College London, 66–72
Gower Street, London, WC1E 6EA, United Kingdom<EMAIL_ADDRESS>
###### Abstract.

The classical homomorphism preservation theorem, due to Łoś, Lyndon and
Tarski, states that a first-order sentence $\varphi$ is preserved under
homomorphisms between structures if, and only if, it is equivalent to an
existential positive sentence $\psi$. Given a notion of (syntactic) complexity
of sentences, an “equi-resource” homomorphism preservation theorem improves on
the classical result by ensuring that $\psi$ can be chosen so that its
complexity does not exceed that of $\varphi$.

We describe an axiomatic approach to equi-resource homomorphism preservation
theorems based on the notion of arboreal category. This framework is then
employed to establish novel homomorphism preservation results, and improve on
known ones, for various logic fragments, including first-order, guarded and
modal logics.

Research supported by the EPSRC grant EP/V040944/1, and by the European
Union’s Horizon 2020 research and innovation programme under the Marie
Skłodowska-Curie grant agreement No 837724.

##  1\. Introduction

Homomorphism preservation theorems relate the syntactic shape of a sentence
with the semantic property of being preserved under homomorphisms between
structures. Recall that a first-order sentence $\varphi$ in a vocabulary
$\tau$ is said to be _preserved under homomorphisms_ if, whenever there is a
homomorphism of $\tau$-structures $A\to B$ and ${A\vDash\varphi}$, then also
$B\vDash\varphi$. Further, an _existential positive sentence_ is a first-order
sentence that uses only the connectives $\vee,\wedge$ and the quantifier
$\exists$. The following classical result, known as the _homomorphism
preservation theorem_ , is due to Łoś, Lyndon and Tarski [31, 32, 39] and
applies to arbitrary (first-order) vocabularies.

######  Theorem 1.1.

A first-order sentence is preserved under homomorphisms if, and only if, it is
equivalent to an existential positive sentence.

The homomorphism preservation theorem is a fairly straightforward consequence
of the compactness theorem, see e.g. [40, Lemma 3.1.2]. However, applying the
compactness theorem means that we lose control over the syntactic shape of an
existential positive sentence $\psi$ that is equivalent to a sentence
$\varphi$ preserved under homomorphisms. In particular, it is an ineffective
approach if we want to determine to which extent the passage from $\varphi$ to
$\psi$ increases the “complexity” of the former sentence.

One way to measure the complexity of a formula $\varphi$ is in terms of its
_quantifier rank_ , i.e. the maximum number of nested quantifiers appearing in
$\varphi$. Rossman’s _equirank homomorphism preservation theorem_ [38], which
applies to relational vocabularies (i.e. vocabularies that contain no constant
or function symbols), shows that it is possible to find a $\psi$ whose
quantifier rank is less than or equal to the quantifier rank of $\varphi$:

######  Theorem 1.2.

A first-order sentence of quantifier rank at most $k$ is preserved under
homomorphisms if, and only if, it is equivalent to an existential positive
sentence of quantifier rank at most $k$.

This is a considerable improvement on the classical homomorphism preservation
theorem and was proved by Rossman on the way to his celebrated _finite
homomorphism preservation theorem_ , stating that Theorem 1.1 admits a
relativisation to finite structures.111The finite homomorphism preservation
theorem is a major result in finite model theory, as well as a surprising one
given that most preservation theorems fail when restricted to finite
structures. Note that the finite homomorphism preservation theorem and the
classical one are incomparable results. In the proof of the equirank
homomorphism preservation theorem, the application of the compactness theorem
is replaced with a model construction which is similar, in spirit, to the
construction of a saturated elementary extension of a given structure.

The main contribution of this paper consists in laying out a categorical
framework in which “equi-resource” homomorphism preservation theorems can be
proved in an axiomatic fashion. In [3, 8], _game comonads_ were introduced to
capture in a structural way a number of logic fragments and corresponding
combinatorial and game-theoretic notions, both at the level of finite and
infinite structures. For a recent survey article, see [2]. The template of
game comonads was axiomatised in [6], see also the extended version [7], by
means of the notion of _arboreal category_. Our proof strategy consists in
establishing abstract homomorphism preservation theorems at the level of
arboreal categories and then instantiating these results for specific choices
of game comonads.

We thus obtain novel equi-resource homomorphism preservation theorems for
modal and guarded logics (Theorems 4.9 and 4.11, respectively), along with
relativisations to appropriate subclasses of structures—e.g. the class of
finite structures (Theorems 4.23 and 4.24, respectively). Further, we derive a
relativisation result (Theorem 5.12) which refines Rossman’s equirank
homomorphism preservation theorem.

This paper is organised as follows. In Section 2 we provide a brief
introduction to game comonads, and in Section 3 we recall the necessary
definitions and facts concerning arboreal categories. Homomorphism
preservation theorems are recast into categorical statements and proved at the
level of arboreal categories in Sections 4 and 5. Finally, Section 6 contains
the proof of our main technical result, namely Theorem 5.9.

Throughout this article, we shall assume the reader is familiar with the basic
notions of category theory; standard references include e.g. [10, 33].

##  2\. Logic Fragments and Game Comonads

We shall mainly deal with two types of vocabularies:

  * •

_Relational vocabularies_ , i.e. first-order vocabularies that contain no
function or constant symbols.

  * •

_Multi-modal vocabularies_ , i.e. relational vocabularies in which every
relation symbol has arity at most $2$.

Multi-modal vocabularies will be referred to simply as _modal vocabularies_.
If $\sigma$ is a modal vocabulary, we can assign to each unary relation symbol
$P\in\sigma$ a propositional variable $p$, and to each binary relation symbol
$R\in\sigma$ modalities $\Diamond_{R}$ and $\Box_{R}$. We refer to
$\sigma$-structures as _Kripke structures_. For any Kripke structure $A$, the
interpretation of $P$ in $A$, denoted by $P^{A}$, corresponds to the valuation
of the propositional variable $p$, and the binary relation $R^{A}$ to the
accessibility relation for the modalities $\Diamond_{R}$ and $\Box_{R}$.

For our running examples and intended applications, we will be interested in
the following resource-bounded fragments of first-order logic (always
including the equality symbol) and modal logic, for a relational vocabulary
$\sigma$ and positive integer $k$:

  * •

$\mathrm{FO}_{k}$ and $\exists^{+}\mathrm{FO}_{k}$: these denote,
respectively, the set of sentences of quantifier rank $\leq k$ in the
vocabulary $\sigma$, and its existential positive fragment.

  * •

$\mathrm{ML}_{k}$ and $\exists^{+}\mathrm{ML}_{k}$: if $\sigma$ is a modal
vocabulary, $\mathrm{ML}_{k}$ is the set of modal formulas of modal depth
$\leq k$ in the vocabulary $\sigma$ (recall that the _modal depth_ is the
maximum number of nested modalities in a formula). Moreover,
$\exists^{+}\mathrm{ML}_{k}$ denotes the existential positive fragment of
$\mathrm{ML}_{k}$, i.e. the set of formulas in $\mathrm{ML}_{k}$ that use only
the connectives $\vee,\wedge$ and the diamond modalities.

  * •

$\mathrm{ML}_{k}(\\#)$: this is the extension of $\mathrm{ML}_{k}$ with
_graded modalities_. Recall that graded modalities have the form
$\Diamond_{R}^{n}$ and $\Box_{R}^{n}$, with $n\geq 0$, and
$A,a\models{\Diamond_{R}^{n}}\,\varphi$ if there are at least $n$
$R$-successors of $a$ satisfying $\varphi$ (and
$\Box_{R}^{n}\varphi=\neg\Diamond_{R}^{n}\neg\varphi$).

Further logics, namely _guarded logics_ , will be considered in Section 4.2.

Any logic fragment222We employ the nomenclature “logic fragment”, rather than
the more customary term “theory”, as we are mainly interested in the situation
where $\mathcal{L}$ is defined by constraining the syntactic shape of
sentences. $\mathcal{L}$, i.e. any set of first-order sentences in a
vocabulary $\tau$, induces an equivalence relation $\equiv^{\mathcal{L}}$ on
$\tau$-structures defined as follows: for all $\tau$-structures $A,B$,

$A\equiv^{\mathcal{L}}B\ \ \Longleftrightarrow\ \
\forall\varphi\in\mathcal{L}.\,(A\vDash\varphi\,\Leftrightarrow\,B\vDash\varphi).$

If $\mathcal{L}$ consists of all first-order sentences, $\equiv^{\mathcal{L}}$
coincides with elementary equivalence.

Syntax-free characterisations of the equivalence relations
$\equiv^{\mathcal{L}}$ play an important role in model theory. For example,
the Keisler-Shelah theorem states that two $\tau$-structures are elementarily
equivalent if, and only if, they have isomorphic ultrapowers. A different
approach is through _model comparison games_. These have a wide range of
applications in model theory, see e.g. [24, §3], and are central to finite
model theory where tools such as the compactness theorem and ultraproducts are
not available. Model comparison games lead to a perspective which may be
described as “model theory without compactness”.

Game comonads arise from the insight that model comparison games can be seen
as semantic constructions in their own right. Although we shall not employ
games as a tool, we recall two examples of games to motivate the framework of
game comonads.

Henceforth we shall work with a relational vocabulary $\sigma$. Let $A,B$ be
$\sigma$-structures. Both types of game are two-player games played between
Spoiler and Duplicator. Whereas Spoiler aims to show that $A$ and $B$ are
different, Duplicator aims to show that they are similar. Each game is played
in a number of rounds:

Ehrenfeucht-Fraïssé game:

In the $i$th round, Spoiler chooses an element in one of the structures and
Duplicator responds by choosing an element in the other structure. After $k$
rounds have been played, we have sequences $[a_{1},\ldots,a_{k}]$ and
$[b_{1},\ldots,b_{k}]$ of elements from $A$ and $B$ respectively. Duplicator
wins this play if the ensuing relation $r\coloneqq\\{(a_{i},b_{i})\mid 1\leq
i\leq k\\}$ is a partial isomorphism. Duplicator wins the $k$-round game if
they have a strategy which is winning after $i$ rounds, for all $1\leq i\leq
k$.

Bisimulation game:

Suppose $\sigma$ is a modal vocabulary. The game is played between pointed
Kripke structures $(A,a)$ and $(B,b)$, where $a\in A$ and $b\in B$. The
initial position is $(a_{0},b_{0})=(a,b)$. In the $i$th round, with current
position $(a_{i-1},b_{i-1})$, Spoiler chooses one of the two structures, say
$A$, a binary relation symbol $R$ in $\sigma$, and an element $a_{i}\in A$
such that $(a_{i-1},a_{i})\in R^{A}$. Duplicator responds by choosing an
element in the other structure, say $b_{i}\in B$, such that
$(b_{i-1},b_{i})\in R^{B}$. If Duplicator has no such response, they lose.
Duplicator wins the $k$-round game if, for all unary relation symbols $P$ in
$\sigma$, we have $P^{A}(a_{i})\Leftrightarrow P^{B}(b_{i})$ for all $0\leq
i\leq k$.

Assume the vocabulary $\sigma$ is finite. The classical Ehrenfeucht-Fraïssé
theorem [20, 21] states that Duplicator has a winning strategy in the
$k$-round Ehrenfeucht-Fraïssé game played between $A$ and $B$ if, and only if,
$A$ and $B$ satisfy the same first-order sentences of quantifier rank at most
$k$. Similarly, Duplicator has a winning strategy in the $k$-round
bisimulation game played between pointed Kripke structures $(A,a)$ and $(B,b)$
if, and only if, $(A,a)$ and $(B,b)$ satisfy the same modal formulas of modal
depth at most $k$ [23].

######  Remark 2.1.

In both Ehrenfeucht-Fraïssé and bisimulation games, the resource parameter is
the number of rounds. This need not be the case in general. For instance, the
resource parameter for pebble games [13, 25], which correspond to finite-
variable fragments of first-order logic, is the number of pebbles available to
the players.

Next, we introduce the comonads corresponding to Ehrenfeucht-Fraïssé and
bisimulation games, respectively. For each $\sigma$-structure $A$, denote by
$\mathbb{E}_{k}(A)$ the set of all non-empty sequences of length at most $k$
of elements from $A$. In other words, $\mathbb{E}_{k}(A)$ is the set of all
plays in $A$ in the $k$-round Ehrenfeucht-Fraïssé game. The interpretations of
the relation symbols can be lifted from $A$ to $\mathbb{E}_{k}(A)$ as follows.
Let $\varepsilon_{A}\colon\mathbb{E}_{k}(A)\to A$ be the function sending a
sequence to its last element. For each relation symbol $R\in\sigma$ of arity
$j$, we define $R^{\mathbb{E}_{k}(A)}$ to be the set of all tuples
$(s_{1},\ldots,s_{j})\in\mathbb{E}_{k}(A)^{j}$ such that:

  1. (i)

The sequences $s_{1},\ldots,s_{j}$ are pairwise comparable in the prefix
order.

  2. (ii)

$(\varepsilon_{A}(s_{1}),\ldots,\varepsilon_{A}(s_{j}))\in R^{A}$.

For every homomorphism $f\colon A\to B$, let

$\mathbb{E}_{k}(f)\colon\mathbb{E}_{k}(A)\to\mathbb{E}_{k}(B),\ \
[a_{1},\ldots,a_{l}]\mapsto[f(a_{1}),\ldots,f(a_{l})].$

This yields a comonad (in fact, a _family_ of comonads indexed by $k>0$) on
the category $\mathbf{Struct}(\sigma)$ of $\sigma$-structures and their
homomorphisms, known as _Ehrenfeucht-Fraïssé comonad_ [8]. The underlying
functor of this comonad is
$\mathbb{E}_{k}\colon\mathbf{Struct}(\sigma)\to\mathbf{Struct}(\sigma)$, the
counit is $\varepsilon$, and the comultiplication at $A$ is the homomorphism

$\mathbb{E}_{k}(A)\to\mathbb{E}_{k}\mathbb{E}_{k}(A),\ \
[a_{1},\ldots,a_{l}]\mapsto[[a_{1}],[a_{1},a_{2}],\ldots,[a_{1},\ldots,a_{l}]].$

A similar construction applies to $k$-round bisimulation games. Suppose
$\sigma$ is a modal vocabulary and let $(A,a)$ be a pointed Kripke structure.
We define a Kripke structure $\mathbb{M}_{k}(A,a)$ whose carrier is the set of
all paths $p$ of length at most $k$ starting from $a$:

$a\xrightarrow{R_{1}}a_{1}\xrightarrow{R_{2}}a_{2}\to\cdots\xrightarrow{R_{n}}a_{n}$

where $R_{1},\dots,R_{n}$ are binary relation symbols in $\sigma$. If
$P\in\sigma$ is unary then $P^{\mathbb{M}_{k}(A,a)}$ is the set of paths $p$
whose last element $a_{n}$ belongs to $P^{A}$. For a binary relation symbol
$R$ in $\sigma$, $R^{\mathbb{M}_{k}(A,a)}$ is the set of pairs of paths
$(p,p^{\prime})$ such that $p^{\prime}$ is obtained by extending $p$ by one
step along $R$. The distinguished element of the Kripke structure
$\mathbb{M}_{k}(A,a)$ is the trivial path $\langle a\rangle$ of length $0$,
and the function $\varepsilon_{(A,a)}\colon(\mathbb{M}_{k}(A,a),\langle
a\rangle)\to(A,a)$ sending a path to its last element is a morphism of pointed
Kripke structures. By similar reasoning to the one above, the assignment
$(A,a)\mapsto(\mathbb{M}_{k}(A,a),\langle a\rangle)$ can be upgraded to a
comonad on the category $\mathbf{Struct}_{\bullet}(\sigma)$ of pointed Kripke
structures and their homomorphisms, the _modal comonad_ [8].

In addition to the examples mentioned above, the framework of game comonads
covers a number of model comparison games, cf. e.g. [3, 4, 5, 16, 26, 35]. In
each case, they yield structural (syntax-free) characterisations of
equivalence in the corresponding logic fragments. This will be illustrated
from an axiomatic perspective in Section 3.4.

##  3\. Arboreal Categories

In this section, we recall from [7] the basic definitions and facts concerning
arboreal categories. All categories under consideration are assumed to be
locally small and _well-powered_ , i.e. every object has a _small_ set of
subobjects (as opposed to a proper class).

###  3.1. Proper factorisation systems

Given arrows $e$ and $m$ in a category $\operatorname{\mathscr{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

${{\cdot}}$${{\cdot}}$${{\cdot}}$${{\cdot}}$$\scriptstyle{e}$$\scriptstyle{m}$
${{\cdot}}$${{\cdot}}$${{\cdot}}$${{\cdot}}$$\scriptstyle{e}$$\scriptstyle{d}$$\scriptstyle{m}$

there is an arrow $d$ such that the right-hand diagram above commutes. For any
class $\mathscr{H}$ of morphisms in $\operatorname{\mathscr{C}}$, let
${}^{\pitchfork}\mathscr{H}$ (respectively $\mathscr{H}^{\pitchfork}$) be the
class of morphisms having the left (respectively right) lifting property with
respect to every morphism in $\mathscr{H}$.

######  Definition 3.1.

A pair of classes of morphisms $(\mathscr{Q},\mathscr{M})$ in a category
$\operatorname{\mathscr{C}}$ is a _weak factorisation system_ provided it
satisfies the following conditions:

  1. (i)

Every morphism $f$ in $\operatorname{\mathscr{C}}$ can be written as $f=m\circ
e$ with $e\in\mathscr{Q}$ and $m\in\mathscr{M}$.

  2. (ii)

$\mathscr{Q}={}^{\pitchfork}\mathscr{M}$ and
$\mathscr{M}=\mathscr{Q}^{\pitchfork}$.

A _proper factorisation system_ is a weak factorisation system
$(\mathscr{Q},\mathscr{M})$ such that each arrow in $\mathscr{Q}$ is epic and
each arrow in $\mathscr{M}$ is monic. We refer to $\mathscr{M}$-morphisms as
_embeddings_ and denote them by $\rightarrowtail$. $\mathscr{Q}$-morphisms
will be referred to as _quotients_ and denoted by $\twoheadrightarrow$.

Next, we state some well known properties of proper factorisation systems (cf.
e.g. [22] or [37]) which will be used throughout the paper without further
reference.

######  Lemma 3.2.

Let $(\mathscr{Q},\mathscr{M})$ be a proper factorisation system in
$\operatorname{\mathscr{C}}$. The following hold:

  1. (a)

$\mathscr{Q}$ and $\mathscr{M}$ are closed under compositions.

  2. (b)

$\mathscr{Q}$ contains all retractions, $\mathscr{M}$ contains all sections,
and $\mathscr{Q}\cap\mathscr{M}=\\{\text{isomorphisms}\\}$.

  3. (c)

The pullback of an $\mathscr{M}$-morphism along any morphism, if it exists, is
in $\mathscr{M}$.

  4. (d)

$g\circ f\in\mathscr{Q}$ implies $g\in\mathscr{Q}$.

  5. (e)

$g\circ f\in\mathscr{M}$ implies $f\in\mathscr{M}$.

Assume $\operatorname{\mathscr{C}}$ is a category admitting a proper
factorisation system $(\mathscr{Q},\mathscr{M})$. In the same way that one
usually defines the poset of subobjects of a given object
$X\in\operatorname{\mathscr{C}}$, we can define the poset
$\operatorname{\mathbb{S}}{X}$ of $\mathscr{M}$-subobjects of $X$. Given
embeddings $m\colon S\rightarrowtail X$ and $n\colon T\rightarrowtail X$, let
us say that $m\trianglelefteq n$ provided there is a morphism $i\colon S\to T$
such that $m=n\circ i$ (if it exists, $i$ is necessarily an embedding).

${S}$${X}$${T}$$\scriptstyle{m}$$\scriptstyle{i}$$\scriptstyle{n}$

This yields a preorder on the class of all embeddings with codomain $X$. The
symmetrisation $\sim$ of $\trianglelefteq$ is given by $m\sim n$ if, and only
if, there exists an isomorphism $i\colon S\to T$ such that $m=n\circ i$. Let
$\operatorname{\mathbb{S}}{X}$ be the class of $\sim$-equivalence classes of
embeddings with codomain $X$, equipped with the natural partial order $\leq$
induced by $\trianglelefteq$. We shall systematically represent a
$\sim$-equivalence class by any of its representatives. As
$\operatorname{\mathscr{C}}$ is well-powered and every embedding is a
monomorphism, $\operatorname{\mathbb{S}}{X}$ is a set.

For any morphism $f\colon X\to Y$ and embedding $m\colon S\rightarrowtail X$,
consider the (quotient, embedding) factorisation of $f\circ m$:

${S}$${\exists_{f}S}$${Y.}$$\scriptstyle{\exists_{f}m}$

This yields a monotone map
$\exists_{f}\colon\operatorname{\mathbb{S}}{X}\to\operatorname{\mathbb{S}}{Y}$
sending $m$ to $\exists_{f}m$. Note that the map $\exists_{f}$ is well-defined
because factorisations are unique up to isomorphism. If $f$ is an embedding
(or, more generally, $f\circ m$ is an embedding), $\exists_{f}m$ can be
identified with $f\circ m$. For the following observation, cf. e.g. [7, Lemma
2.7(a)].

######  Lemma 3.3.

Let $\operatorname{\mathscr{C}}$ be a category equipped with a proper
factorisation system and let $f\colon X\rightarrowtail Y$ be an embedding in
$\operatorname{\mathscr{C}}$. Then
$\exists_{f}\colon\operatorname{\mathbb{S}}{X}\to\operatorname{\mathbb{S}}{Y}$
is an order-embedding.

###  3.2. Arboreal categories

Let $\operatorname{\mathscr{C}}$ be a category endowed with a proper
factorisation system $(\mathscr{Q},\mathscr{M})$.

######  Definition 3.4.

An object $X$ of $\operatorname{\mathscr{C}}$ is called a _path_ provided the
poset $\operatorname{\mathbb{S}}{X}$ is a finite chain. Paths will be denoted
by $P,Q$ and variations thereof.

The collection of paths is closed under embeddings and quotients. That is,
given an arrow $f\colon X\to Y$, if $f$ is an embedding and $Y$ is a path then
$X$ is a path, and if $f$ is a quotient and $X$ is a path then $Y$ is a path
[7, Lemma 3.5].

A _path embedding_ is an embedding $P\rightarrowtail X$ whose domain is a
path. We let $\operatorname{\mathbb{P}}{X}$ denote the sub-poset of
$\operatorname{\mathbb{S}}{X}$ consisting of the path embeddings. Because
paths are closed under quotients, for any arrow $f\colon X\to Y$ the monotone
map
$\exists_{f}\colon\operatorname{\mathbb{S}}{X}\to\operatorname{\mathbb{S}}{Y}$
restricts to a monotone map

$\operatorname{\mathbb{P}}{f}\colon\operatorname{\mathbb{P}}{X}\to\operatorname{\mathbb{P}}{Y},\
\ (m\colon P\rightarrowtail
X)\mapsto(\exists_{f}m\colon\exists_{f}P\rightarrowtail Y).$ (1)

For any object $X$ of $\operatorname{\mathscr{C}}$, we have a diagram with
vertex $X$ consisting of all path embeddings with codomain $X$. The morphisms
between paths are those making the obvious triangles commute:

${X}$${P}$${Q}$

Choosing representatives in an appropriate way, this yields a cocone over the
small diagram $\operatorname{\mathbb{P}}{X}$. We say that $X$ is _path-
generated_ provided this is a colimit cocone in $\operatorname{\mathscr{C}}$.

Suppose for a moment that coproducts of sets of paths exist in
$\operatorname{\mathscr{C}}$. An object $X$ of $\operatorname{\mathscr{C}}$ is
_connected_ if, for all non-empty sets of paths $\\{P_{i}\mid i\in I\\}$ in
$\operatorname{\mathscr{C}}$, any morphism

$X\to\coprod_{i\in I}{P_{i}}$

factors through some coproduct injection $P_{j}\to\coprod_{i\in I}{P_{i}}$.

In order to state the definition of arboreal category, let us say that a
proper factorisation system is _stable_ if, for any quotient $e$ and embedding
$m$ with common codomain, the pullback of $e$ along $m$ exists and is a
quotient.

######  Definition 3.5.

An _arboreal category_ is a category $\operatorname{\mathscr{C}}$, equipped
with a stable proper factorisation system, that satisfies the following
conditions:

  1. (i)

$\operatorname{\mathscr{C}}$ has all coproducts of sets of paths.

  2. (ii)

For any paths $P,Q,Q^{\prime}$ in $\operatorname{\mathscr{C}}$, if a composite
$P\to Q\to Q^{\prime}$ is a quotient then so is $P\to Q$.

  3. (iii)

Every object of $\operatorname{\mathscr{C}}$ is path-generated.

  4. (iv)

Every path in $\operatorname{\mathscr{C}}$ is connected.

######  Remark 3.6.

Item (ii) in the previous definition is equivalent to the following _2-out-
of-3 condition_ : For any paths $P,Q,Q^{\prime}$ and morphisms

${P}$${Q}$${Q^{\prime},}$$\scriptstyle{f}$$\scriptstyle{g}$

if any two of $f$, $g$, and $g\circ f$ are quotients, then so is the third.
See [7, Remark 3.8]. Moreover, item (iii) is equivalent to saying that the
inclusion functor
$\operatorname{\mathscr{C}}_{p}\hookrightarrow\operatorname{\mathscr{C}}$ is
dense, where $\operatorname{\mathscr{C}}_{p}$ is the full subcategory of
$\operatorname{\mathscr{C}}$ defined by the paths [7, Lemma 5.1].

Finally, note that any arboreal category admits an initial object, obtained as
the coproduct of the empty set, and any initial object is a path because its
poset of $\mathscr{M}$-subobjects has a single element—namely, the equivalence
class of the identity.

If $(P,{\leq})$ is a poset, then $C\subseteq P$ is a _chain_ if it is linearly
ordered. $(P,\leq)$ is a _forest_ if, for all $x\in P$, the set
${\downarrow}x\coloneqq\\{y\in P\mid y\leq x\\}$ is a finite chain. The
_height_ of a forest is the supremum of the cardinalities of its chains. The
_covering relation_ $\prec$ associated with a partial order $\leq$ is defined
by $u\prec v$ if and only if $u<v$ and there is no $w$ such that $u<w<v$. The
_roots_ of a forest are the minimal elements, and a _tree_ is a forest with at
most one root. Morphisms of forests are maps that preserve roots and the
covering relation. The category of forests is denoted by
$\operatorname{\mathscr{F}}$, and the full subcategory of trees by
$\operatorname{\mathscr{T}}$.

######  Example 3.7.

Let $\sigma$ be a relational vocabulary. A _forest-ordered $\sigma$-structure_
$(A,{\leq})$ is a $\sigma$-structure $A$ equipped with a forest order $\leq$.
A morphism of forest-ordered $\sigma$-structures
$f\colon(A,{\leq})\to(B,{\leq^{\prime}})$ is a $\sigma$-homomorphism $f\colon
A\to B$ that is also a forest morphism. This determines a category
$\mathscr{R}(\sigma)$. We equip $\mathscr{R}(\sigma)$ with the factorisation
system given by (surjective morphisms, embeddings), where an embedding is a
morphism which is an embedding qua $\sigma$-homomorphism. Let
$\mathscr{R}^{E}(\sigma)$ be the full subcategory of $\mathscr{R}(\sigma)$
determined by those objects $(A,{\leq})$ satisfying the following condition:

  1. (E)

If $a,b\in A$ are distinct elements that appear in a tuple of related elements
$(a_{1},\ldots,a_{l})\in R^{A}$ for some $R\in\sigma$, then either $a<b$ or
$b<a$.333I.e., if $a$ and $b$ are adjacent in the _Gaifman graph_ of $A$, then
they are comparable in the forest order.

For each $k>0$, let $\mathscr{R}^{E}_{k}(\sigma)$ be the full subcategory of
$\mathscr{R}^{E}(\sigma)$ of forest-ordered structures of height $\leq k$. In
[9, Theorem 9.1], it is shown that $\mathscr{R}^{E}_{k}(\sigma)$ is isomorphic
to the category of coalgebras for the Ehrenfeucht-Fraïssé comonad
$\mathbb{E}_{k}$ on $\mathbf{Struct}(\sigma)$. The objects $(A,{\leq})$ of
$\mathscr{R}^{E}_{k}(\sigma)$ are forest covers of $A$ witnessing that its
_tree-depth_ is at most $k$ [34].

The category $\mathscr{R}^{E}(\sigma)$ is arboreal when equipped with the
restriction of the factorisation system on $\mathscr{R}(\sigma)$. The paths in
$\mathscr{R}^{E}(\sigma)$ are those objects in which the order is a finite
chain. Similarly, $\mathscr{R}^{E}_{k}(\sigma)$ is an arboreal category for
all $k>0$, when equipped with the restriction of the factorisation system on
$\mathscr{R}(\sigma)$. See [7, Examples 5.3].

######  Example 3.8.

Assume that $\sigma$ is a modal vocabulary. Let $\mathscr{R}^{M}(\sigma)$ be
the full subcategory of $\mathscr{R}(\sigma)$ consisting of the tree-ordered
$\sigma$-structures $(A,{\leq})$ satisfying:

  1. (M)

For $a,b\in A$, $a\prec b$ if and only if $(a,b)\in R^{A}$ for some unique
binary relation $R$.

For each $k>0$, the full subcategory $\mathscr{R}^{M}_{k}(\sigma)$ of
$\mathscr{R}^{M}(\sigma)$ consisting of the tree-ordered structures of height
at most $k$ is isomorphic to the category of coalgebras for the modal comonad
$\mathbb{M}_{k}$ on $\mathbf{Struct}_{\bullet}(\sigma)$ [9, Theorem 9.5]. When
equipped with the restriction of the factorisation system on
$\mathscr{R}(\sigma)$, the category $\mathscr{R}^{M}(\sigma)$ is arboreal and
its paths are those objects in which the order is a finite chain. Likewise for
$\mathscr{R}^{M}_{k}(\sigma)$.

It follows from the definition of path that, for any object $X$ of an arboreal
category, the poset $\operatorname{\mathbb{P}}{X}$ is a tree; in fact, a non-
empty tree. Crucially, this assignment extends to a functor into the category
of trees (for a proof, see [7, Theorem 3.10]):

######  Theorem 3.9.

Let $\operatorname{\mathscr{C}}$ be an arboreal category. The assignment
$f\mapsto\operatorname{\mathbb{P}}{f}$ in equation (1) induces a functor
$\operatorname{\mathbb{P}}\colon\operatorname{\mathscr{C}}\to\operatorname{\mathscr{T}}$
into the category of trees.

Finally, recall from [7, §5] the following properties of paths and posets of
embeddings.

######  Lemma 3.10.

The following statements hold in any arboreal category
$\operatorname{\mathscr{C}}$:

  1. (a)

Between any two paths there is at most one embedding.

  2. (b)

For all objects $X$ of $\operatorname{\mathscr{C}}$, the poset
$\operatorname{\mathbb{S}}{X}$ of its $\mathscr{M}$-subobjects is a complete
lattice.444In fact, $\operatorname{\mathbb{S}}{X}$ is a _perfect_ lattice, cf.
[36] or [17].

  3. (c)

Let $X$ be an object of $\operatorname{\mathscr{C}}$ and let
$\mathcal{U}\subseteq\operatorname{\mathbb{P}}{X}$ be a non-empty subset. A
path embedding $m\in\operatorname{\mathbb{P}}{X}$ is below
$\bigvee{\mathcal{U}}\in\operatorname{\mathbb{S}}{X}$ if, and only if, it is
below some element of $\mathcal{U}$.

If it exists, the unique embedding between paths $P,Q$ in an arboreal category
is denoted by

$!_{P,Q}\colon P\rightarrowtail Q.$

If no confusion arises, we simply write $!\colon P\rightarrowtail Q$.

###  3.3. Bisimilarity and back-and-forth systems

Throughout this section, we fix an arbitrary arboreal category
$\operatorname{\mathscr{C}}$. A morphism $f\colon X\to Y$ in
$\operatorname{\mathscr{C}}$ is said to be _open_ if it satisfies the
following path-lifting property: Given any commutative square

${P}$${Q}$${X}$${Y}$$\scriptstyle{f}$

with $P,Q$ paths, there is an arrow $Q\to X$ making the two triangles commute.
(If such an arrow exists, it is automatically an embedding.) Further, $f$ is a
_pathwise embedding_ if, for all path embeddings $m\colon P\rightarrowtail X$,
the composite $f\circ m\colon P\to Y$ is a path embedding.

Combining these notions, we can define a bisimilarity relation between objects
of $\operatorname{\mathscr{C}}$:

######  Definition 3.11.

Two objects $X,Y$ of $\operatorname{\mathscr{C}}$ are said to be _bisimilar_
if there exist an object $Z$ of $\operatorname{\mathscr{C}}$ and a span of
open pathwise embeddings $X\leftarrow Z\rightarrow Y$.

######  Remark 3.12.

The definition of open morphism given above is a refinement of the one
introduced in [28] (cf. [7, §4.1] for a discussion of the relation between
these notions), which is a special case of the concept of open geometric
morphism between toposes [27].

As we shall see next, if $\operatorname{\mathscr{C}}$ has binary products the
bisimilarity relation can be characterised in terms of back-and-forth systems.
Let $X,Y$ be objects of $\operatorname{\mathscr{C}}$. Given
$m\in\operatorname{\mathbb{P}}{X}$ and $n\in\operatorname{\mathbb{P}}{Y}$, we
write $\llbracket m,n\rrbracket$ to indicate that
$\operatorname{dom}(m)\cong\operatorname{dom}(n)$. Intuitively, the pair
$\llbracket m,n\rrbracket$ encodes a partial isomorphisms between $X$ and $Y$
“of shape $P$”, with $P$ a path.

######  Definition 3.13.

A _back-and-forth system_ between objects $X$ and $Y$ of
$\operatorname{\mathscr{C}}$ is a set

$\mathcal{B}=\\{\llbracket m_{i},n_{i}\rrbracket\mid
m_{i}\in\operatorname{\mathbb{P}}{X},\,n_{i}\in\operatorname{\mathbb{P}}{Y},\,i\in
I\\}$

satisfying the following conditions:

  1. (i)

$\llbracket\bot_{X},\bot_{Y}\rrbracket\in\mathcal{B}$, where
$\bot_{X},\bot_{Y}$ are the roots of $\operatorname{\mathbb{P}}{X}$ and
$\operatorname{\mathbb{P}}{Y}$, respectively.

  2. (ii)

If $\llbracket m,n\rrbracket\in\mathcal{B}$ and
$m^{\prime}\in\operatorname{\mathbb{P}}{X}$ are such that $m\prec m^{\prime}$,
there exists $n^{\prime}\in\operatorname{\mathbb{P}}{Y}$ satisfying $n\prec
n^{\prime}$ and $\llbracket m^{\prime},n^{\prime}\rrbracket\in\mathcal{B}$.

  3. (iii)

If $\llbracket m,n\rrbracket\in\mathcal{B}$ and
$n^{\prime}\in\operatorname{\mathbb{P}}{Y}$ are such that $n\prec n^{\prime}$,
there exists $m^{\prime}\in\operatorname{\mathbb{P}}{X}$ satisfying $m\prec
m^{\prime}$ and $\llbracket m^{\prime},n^{\prime}\rrbracket\in\mathcal{B}$.

Two objects $X$ and $Y$ of $\operatorname{\mathscr{C}}$ are said to be _back-
and-forth equivalent_ if there exists a back-and-forth system between them.

For a proof of the following result, see [7, Theorem 6.4].

######  Theorem 3.14.

Let $X,Y$ be objects of an arboreal category admitting a product. Then $X$ and
$Y$ are bisimilar if, and only if, they are back-and-forth equivalent.

The existence of a back-and-forth system between $X$ and $Y$ can be
equivalently described in terms of the existence of a Duplicator winning
strategy in a two-player game played between $\operatorname{\mathbb{P}}{X}$
and $\operatorname{\mathbb{P}}{Y}$ [7, §6.2]. Since winning strategies can be
composed to yield again a winning strategy, in any arboreal category with
binary products the bisimilarity relation is transitive, hence an equivalence
relation.

###  3.4. Resource-indexed arboreal adjunctions

Let $\operatorname{\mathscr{C}}$ be an arboreal category, with full
subcategory of paths $\operatorname{\mathscr{C}}_{p}$. We say that
$\operatorname{\mathscr{C}}$ is _resource-indexed_ if for all positive
integers $k$ there is a full subcategory $\operatorname{\mathscr{C}}_{p}^{k}$
of $\operatorname{\mathscr{C}}_{p}$ closed under embeddings555That is, for any
embedding $P\rightarrowtail Q$ in $\operatorname{\mathscr{C}}$ with $P,Q$
paths, if $Q\in\operatorname{\mathscr{C}}_{p}^{k}$ then also
$P\in\operatorname{\mathscr{C}}_{p}^{k}$. We shall further assume that each
category $\operatorname{\mathscr{C}}_{p}^{k}$ contains the initial object of
$\operatorname{\mathscr{C}}$. with

$\operatorname{\mathscr{C}}_{p}^{1}\hookrightarrow\operatorname{\mathscr{C}}_{p}^{2}\hookrightarrow\operatorname{\mathscr{C}}_{p}^{3}\hookrightarrow\cdots$

This induces a corresponding tower of full subcategories
$\operatorname{\mathscr{C}}_{k}$ of $\operatorname{\mathscr{C}}$, with the
objects of $\operatorname{\mathscr{C}}_{k}$ those whose cocone of path
embeddings with domain in $\operatorname{\mathscr{C}}_{p}^{k}$ is a colimit
cocone in $\operatorname{\mathscr{C}}$. It turns out that each category
$\operatorname{\mathscr{C}}_{k}$ is arboreal. Furthermore, the paths in
$\operatorname{\mathscr{C}}_{k}$ are precisely the objects of
$\operatorname{\mathscr{C}}_{p}^{k}$, i.e.
$(\operatorname{\mathscr{C}}_{k})_{p}=\operatorname{\mathscr{C}}_{p}^{k}$. Cf.
[7, Proposition 7.6] and its proof.

######  Example 3.15.

Consider the arboreal category $\mathscr{R}^{E}(\sigma)$ from Example 3.7.
This can be regarded as a resource-indexed arboreal category by taking as
$\operatorname{\mathscr{C}}_{p}^{k}$ the full subcategory of
$\mathscr{R}^{E}(\sigma)$ consisting of the objects in which the order is a
finite chain of cardinality $\leq k$. The generated subcategory
$\operatorname{\mathscr{C}}_{k}$ then coincides with
$\mathscr{R}^{E}_{k}(\sigma)$.

A similar reasoning shows that the arboreal category $\mathscr{R}^{M}(\sigma)$
from Example 3.8 can also be regarded as a resource-indexed arboreal category.

######  Definition 3.16.

Let $\\{\operatorname{\mathscr{C}}_{k}\\}$ be a resource-indexed arboreal
category and let $\operatorname{\mathscr{E}}$ be a category. A _resource-
indexed arboreal adjunction_ between $\operatorname{\mathscr{E}}$ and
$\operatorname{\mathscr{C}}$ is an indexed family of adjunctions

${\operatorname{\mathscr{C}}_{k}}$${\operatorname{\mathscr{E}}.}$$\scriptstyle{L_{k}}$$\scriptstyle{R_{k}}$$\bot$

A _resource-indexed arboreal cover_ of $\operatorname{\mathscr{E}}$ by
$\operatorname{\mathscr{C}}$ is a resource-indexed arboreal adjunction between
$\operatorname{\mathscr{E}}$ and $\operatorname{\mathscr{C}}$ such that all
adjunctions $L_{k}\dashv R_{k}$ are comonadic, i.e. for all $k>0$ the
comparison functor from $\operatorname{\mathscr{C}}_{k}$ to the category of
Eilenberg-Moore coalgebras for the comonad $G_{k}\coloneqq L_{k}R_{k}$ is an
isomorphism.

######  Example 3.17.

Let $\sigma$ be a relational vocabulary and let
$\operatorname{\mathscr{E}}=\mathbf{Struct}(\sigma)$. Consider the resource-
indexed arboreal category $\mathscr{R}^{E}(\sigma)$ in Example 3.15. For each
$k>0$, there is a forgetful functor

$L^{E}_{k}\colon\mathscr{R}^{E}_{k}(\sigma)\to\mathbf{Struct}(\sigma)$

which forgets the forest order. This functor is comonadic. The right adjoint
$R^{E}_{k}$ sends a $\sigma$-structure $A$ to $\mathbb{E}_{k}(A)$ equipped
with the prefix order, and the comonad induced by this adjunction coincides
with the $k$-round Ehrenfeucht-Fraïssé comonad $\mathbb{E}_{k}$. This gives
rise to a resource-indexed arboreal cover of $\mathbf{Struct}(\sigma)$ by
$\mathscr{R}^{E}(\sigma)$.

Similarly, if $\sigma$ is a modal vocabulary, there is a resource-indexed
arboreal cover of $\mathbf{Struct}_{\bullet}(\sigma)$ by
$\mathscr{R}^{M}(\sigma)$ such that each adjunction $L^{M}_{k}\dashv
R^{M}_{k}$ induces the $k$-round modal comonad $\mathbb{M}_{k}$.

######  Example 3.18.

To deal with the equality symbol in the logic, it is useful to consider
resource-indexed arboreal adjunctions constructed as follows. Let

$\sigma^{I}\coloneqq\sigma\cup\\{I\\}$

be the vocabulary obtained by adding a fresh binary relation symbol $I$ to
$\sigma$. Any $\sigma$-structure can be expanded to a $\sigma^{I}$-structure
by interpreting $I$ as the identity relation. This yields a fully faithful
functor $J\colon\mathbf{Struct}(\sigma)\to\mathbf{Struct}(\sigma^{I})$. The
functor $J$ has a left adjoint
$H\colon\mathbf{Struct}(\sigma^{I})\to\mathbf{Struct}(\sigma)$ which sends a
$\sigma^{I}$-structure $A$ to the quotient of the $\sigma$-reduct of $A$ by
the equivalence relation generated by $I^{A}$ [18, Lemma 25]. We can then
compose the adjunction $H\dashv J$ with e.g. the Ehrenfeucht-Fraïssé resource-
indexed arboreal cover of $\mathbf{Struct}(\sigma^{I})$ by
$\mathscr{R}^{E}(\sigma^{I})$ from Example 3.17.

${{\mathscr{R}^{E}_{k}(\sigma^{I})}}$${{\mathbf{Struct}(\sigma^{I})}}$${{\mathbf{Struct}(\sigma)}}$$\scriptstyle{L^{E}_{k}}$$\scriptstyle{R^{E}_{k}}$$\scriptstyle{H}$$\scriptstyle{J}$$\bot$$\bot$

The composite adjunctions $HL^{E}_{k}\dashv R^{E}_{k}J$, which are not
comonadic, yield the _Ehrenfeucht-Fraïssé resource-indexed arboreal
adjunction_ between $\mathbf{Struct}(\sigma)$ and
$\mathscr{R}^{E}(\sigma^{I})$.

Crucially, a resource-indexed arboreal adjunction between
$\operatorname{\mathscr{E}}$ and $\operatorname{\mathscr{C}}$ can be used to
define several resource-indexed relations between objects of
$\operatorname{\mathscr{E}}$:

######  Definition 3.19.

Consider a resource-indexed arboreal adjunction between
$\operatorname{\mathscr{E}}$ and $\operatorname{\mathscr{C}}$, with
adjunctions $L_{k}\dashv R_{k}$, and any two objects $a,b$ of
$\operatorname{\mathscr{E}}$. For all $k>0$, we define:

  * •

$a\rightarrow_{k}^{\operatorname{\mathscr{C}}}b$ if there exists a morphism
$R_{k}a\to R_{k}b$ in $\operatorname{\mathscr{C}}_{k}$.

  * •

$a\leftrightarrow_{k}^{\operatorname{\mathscr{C}}}b$ if $R_{k}a$ and $R_{k}b$
are bisimilar in $\operatorname{\mathscr{C}}_{k}$.

  * •

$a\cong_{k}^{\operatorname{\mathscr{C}}}b$ if $R_{k}a$ and $R_{k}b$ are
isomorphic in $\operatorname{\mathscr{C}}_{k}$.

Further, we write $\rightleftarrows_{k}^{\operatorname{\mathscr{C}}}$ for the
symmetrisation of the preorder $\rightarrow_{k}^{\operatorname{\mathscr{C}}}$.
There are inclusions

${\cong_{k}^{\operatorname{\mathscr{C}}}}\ \subseteq\
{\leftrightarrow_{k}^{\operatorname{\mathscr{C}}}}\ \subseteq\
{\rightleftarrows_{k}^{\operatorname{\mathscr{C}}}}.$

The first inclusion is trivial, the second follows from [7, Lemma 6.20]. For a
proof of the following easy observation, see [7, Lemma 7.18].

######  Lemma 3.20.

Consider a resource-indexed arboreal adjunction between
$\operatorname{\mathscr{E}}$ and $\operatorname{\mathscr{C}}$, with
adjunctions $L_{k}\dashv R_{k}$. The following hold for all
$a,b\in\operatorname{\mathscr{E}}$ and all $k>0$:

  1. (a)

If there exists a morphism $a\to b$ in $\operatorname{\mathscr{E}}$ then
$a\rightarrow_{k}^{\operatorname{\mathscr{C}}}b$.

  2. (b)

$a\rightleftarrows_{k}^{\operatorname{\mathscr{C}}}L_{k}R_{k}a$.

To conclude, we recall how the relations in Definition 3.19 capture, in our
running examples, preservation of the logics introduced at the beginning of
Section 2. Given a set of sentences (or modal formulas) $\mathcal{L}$, let
$\Rrightarrow^{\mathcal{L}}$ be the preorder on (pointed) $\sigma$-structures
given by

$A\Rrightarrow^{\mathcal{L}}B\ \ \Longleftrightarrow\ \
\forall\varphi\in\mathcal{L}.\,(A\vDash\varphi\,\Rightarrow\,B\vDash\varphi).$

The equivalence relation $\equiv^{\mathcal{L}}$ is the symmetrisation of
$\Rrightarrow^{\mathcal{L}}$.

######  Example 3.21.

Let $\sigma$ be a finite relational vocabulary. Consider the Ehrenfeucht-
Fraïssé resource-indexed arboreal adjunction between $\mathbf{Struct}(\sigma)$
and $\mathscr{R}^{E}(\sigma^{I})$ in Example 3.18, and write
$\rightarrow_{k}^{E}$ and $\leftrightarrow_{k}^{E}$ for the relations on
$\mathbf{Struct}(\sigma)$ induced according to Definition 3.19. For all
$\sigma$-structures $A,B$ and all $k>0$, we have

$A\rightarrow_{k}^{E}B\ \Longleftrightarrow\
A\Rrightarrow^{\exists^{+}\mathrm{FO}_{k}}B$

and

$A\leftrightarrow_{k}^{E}B\ \Longleftrightarrow\ A\equiv^{\mathrm{FO}_{k}}B.$

Cf. [9, Theorems 3.2 and 5.1] and [9, Theorem 10.5], respectively. We also
mention that $\cong_{k}^{E}$ coincides with equivalence in the extension of
$\mathrm{FO}_{k}$ with _counting quantifiers_ [9, Theorem 5.3(2)], although we
shall not need this fact.

######  Example 3.22.

Suppose $\sigma$ is a finite modal vocabulary and consider the relations
$\rightarrow_{k}^{M}$ and $\cong_{k}^{M}$ on
$\mathbf{Struct}_{\bullet}(\sigma)$ induced by the modal resource-indexed
arboreal cover of $\mathbf{Struct}_{\bullet}(\sigma)$ by
$\mathscr{R}^{M}_{k}(\sigma)$ in Example 3.17. For all pointed Kripke
structures $(A,a),(B,b)$ and all $k>0$, we have

$(A,a)\rightarrow_{k}^{M}(B,b)\ \Longleftrightarrow\
(A,a)\Rrightarrow^{\exists^{+}\mathrm{ML}_{k}}(B,b),$

see [8, Theorem 9]. Furthermore,

$(A,a)\cong_{k}^{M}(B,b)\ \Longrightarrow\
(A,a)\equiv^{\mathrm{ML}_{k}(\\#)}(B,b),$

cf. [8, Proposition 15] and [19, Proposition 3.6]. We mention in passing that
the relation $\leftrightarrow_{k}^{M}$ coincides with equivalence in
$\mathrm{ML}_{k}$ [9, Theorem 10.13].

##  4\. Homomorphism Preservation Theorems

In this section, we recast the statement of a generic equi-resource
homomorphism preservation theorem into a property (HP)—and its strengthening
(HP#)—that a resource-indexed arboreal adjunction may or may not satisfy. We
then identify a class of “tame” resource-indexed arboreal adjunctions, namely
those satisfying the _bisimilar companion property_ , for which (HP) always
holds. In the absence of the bisimilar companion property, one may try to
“force” it; this leads to the notion of _extendability_ , inspired by the work
of Rossman [38]. Finally, we provide simple sufficient conditions under which
properties (HP) and (HP#) admit a relativisation to a full subcategory.

###  4.1. (HP) and (HP#)

Given a first-order sentence $\varphi$ in a relational vocabulary $\sigma$,
its “model class” $\operatorname{\mathbf{Mod}}(\varphi)$ is the full
subcategory of $\mathbf{Struct}(\sigma)$ defined by the $\sigma$-structures
$A$ such that $A\vDash\varphi$. To motivate the formulation of properties (HP)
and (HP#), we recall a well-known characterisation of model classes of
sentences in $\mathrm{FO}_{k}$, i.e. first-order sentences of quantifier rank
at most $k$, and in its existential positive fragment
$\exists^{+}\mathrm{FO}_{k}$. Since a sentence can only contain finitely many
relation symbols, for the purpose of investigating homomorphism preservation
theorems we can safely assume that $\sigma$ is finite.

For a full subcategory $\operatorname{\mathscr{D}}$ of a category
$\operatorname{\mathscr{A}}$, and a relation $\nabla$ on the class of objects
of $\operatorname{\mathscr{A}}$, we say that $\operatorname{\mathscr{D}}$ is
_upwards closed (in $\operatorname{\mathscr{A}}$) with respect to $\nabla$_ if

$\forall a,b\in\operatorname{\mathscr{D}},\ \text{ if }\
a\in\operatorname{\mathscr{D}}\ \text{ and }\ a\nabla b\ \text{ then }\
b\in\operatorname{\mathscr{D}}.$

If $\nabla$ is an equivalence relation and the latter condition is satisfied,
we say that $\operatorname{\mathscr{D}}$ is _saturated under $\nabla$_. The
following lemma follows from the fact that, for all $k\geq 0$, there are
finitely many sentences in $\mathrm{FO}_{k}$ up to logical equivalence. Cf.
e.g. [30, Lemma 3.13].

######  Lemma 4.1.

The following hold for all $k\geq 0$ and all full subcategories
$\operatorname{\mathscr{D}}$ of $\mathbf{Struct}(\sigma)$:

  1. (a)

$\operatorname{\mathscr{D}}=\operatorname{\mathbf{Mod}}(\varphi)$ for some
$\varphi\in\mathrm{FO}_{k}$ if, and only if, $\operatorname{\mathscr{D}}$ is
saturated under $\equiv^{\mathrm{FO}_{k}}$.

  2. (b)

$\operatorname{\mathscr{D}}=\operatorname{\mathbf{Mod}}(\psi)$ for some
$\psi\in\exists^{+}\mathrm{FO}_{k}$ if, and only if,
$\operatorname{\mathscr{D}}$ is upwards closed with respect to
$\Rrightarrow^{\exists^{+}\mathrm{FO}_{k}}$.

######  Remark 4.2.

The previous lemma remains true if $\mathrm{FO}_{k}$ is replaced with any
fragment of first-order logic that is closed under Boolean connectives and
contains, up to logical equivalence, finitely many sentences.

Now, fix a resource-indexed arboreal adjunction between
$\operatorname{\mathscr{E}}$ and $\operatorname{\mathscr{C}}$, with
adjunctions

${\operatorname{\mathscr{C}}_{k}}$${\operatorname{\mathscr{E}}.}$$\scriptstyle{L_{k}}$$\scriptstyle{R_{k}}$$\bot$

Let us say that a full subcategory $\operatorname{\mathscr{D}}$ of
$\operatorname{\mathscr{E}}$ is _closed (in $\operatorname{\mathscr{E}}$)
under morphisms_ if, whenever there is an arrow $a\to b$ in
$\operatorname{\mathscr{E}}$ with $a\in\operatorname{\mathscr{D}}$, also
$b\in\operatorname{\mathscr{D}}$. Note that, when
$\operatorname{\mathscr{E}}=\mathbf{Struct}(\sigma)$ and
$\operatorname{\mathscr{D}}=\operatorname{\mathbf{Mod}}(\varphi)$ is the model
class of some sentence $\varphi$, the category $\operatorname{\mathscr{D}}$ is
closed under morphisms precisely when $\varphi$ is preserved under
homomorphisms.

Consider the following statement, where
$\rightarrow^{\operatorname{\mathscr{C}}}_{k}$ and
$\leftrightarrow_{k}^{\operatorname{\mathscr{C}}}$ are the relations on the
objects of $\operatorname{\mathscr{E}}$ induced by the resource-indexed
arboreal adjunction as in Definition 3.19:

  1. (HP)

For any full subcategory $\operatorname{\mathscr{D}}$ of
$\operatorname{\mathscr{E}}$ saturated under
$\leftrightarrow_{k}^{\operatorname{\mathscr{C}}}$,
$\operatorname{\mathscr{D}}$ is closed under morphisms precisely when it is
upwards closed with respect to $\rightarrow^{\operatorname{\mathscr{C}}}_{k}$.

Replacing the relation $\leftrightarrow_{k}^{\operatorname{\mathscr{C}}}$ with
$\cong_{k}^{\operatorname{\mathscr{C}}}$, we obtain a strengthening of (HP),
namely:

  1. (HP#)

For any full subcategory $\operatorname{\mathscr{D}}$ of
$\operatorname{\mathscr{E}}$ saturated under
$\cong_{k}^{\operatorname{\mathscr{C}}}$, $\operatorname{\mathscr{D}}$ is
closed under morphisms precisely when it is upwards closed with respect to
$\rightarrow^{\operatorname{\mathscr{C}}}_{k}$.

Just recall that
${\cong_{k}^{\operatorname{\mathscr{C}}}}\subseteq{\leftrightarrow_{k}^{\operatorname{\mathscr{C}}}}$,
and so any full subcategory $\operatorname{\mathscr{D}}$ saturated under
$\leftrightarrow_{k}^{\operatorname{\mathscr{C}}}$ is also saturated under
$\cong_{k}^{\operatorname{\mathscr{C}}}$. Thus, (HP#) entails (HP).

######  Remark 4.3.

By Lemma 3.20(a), any full subcategory of $\operatorname{\mathscr{E}}$ that is
upwards closed with respect to $\rightarrow^{\operatorname{\mathscr{C}}}_{k}$
is closed under morphisms. Hence, the right-to-left implications in (HP) and
(HP#) are always satisfied.

In view of Example 3.21 and Lemma 4.1, for the Ehrenfeucht-Fraïssé resource-
indexed arboreal adjunction between $\mathbf{Struct}(\sigma)$ and
$\mathscr{R}^{E}(\sigma^{I})$, property (HP) coincides with Rossman’s equirank
homomorphism preservation theorem (Theorem 1.2).

In Section 5 we will prove that (HP) holds for any resource-indexed arboreal
adjunction satisfying appropriate properties (see Corollary 5.10), which are
satisfied in particular by the Ehrenfeucht-Fraïssé resource-indexed arboreal
adjunction.

###  4.2. Tame: bisimilar companion property and idempotency

For all $k>0$, write $G_{k}\coloneqq L_{k}R_{k}$ for the comonad on
$\operatorname{\mathscr{E}}$ induced by the adjunction ${L_{k}\dashv
R_{k}\colon\operatorname{\mathscr{E}}\to\operatorname{\mathscr{C}}_{k}}$.

######  Definition 4.4.

A resource-indexed arboreal adjunction between $\operatorname{\mathscr{E}}$
and $\operatorname{\mathscr{C}}$, with induced comonads $G_{k}$, has the
_bisimilar companion property_ if
$a\leftrightarrow_{k}^{\operatorname{\mathscr{C}}}G_{k}a$ for all
$a\,{\in}\,\operatorname{\mathscr{E}}$ and $k>0$.

######  Proposition 4.5.

(HP) holds for any resource-indexed arboreal adjunction between
$\operatorname{\mathscr{E}}$ and $\operatorname{\mathscr{C}}$ satisfying the
bisimilar companion property.

###### Proof.

For the left-to-right implication in (HP), let $\operatorname{\mathscr{D}}$ be
a full subcategory of $\operatorname{\mathscr{E}}$ closed under morphisms and
saturated under $\leftrightarrow_{k}^{\operatorname{\mathscr{C}}}$. Suppose
that $a\rightarrow^{\operatorname{\mathscr{C}}}_{k}b$ for objects $a,b$ of
$\operatorname{\mathscr{E}}$. By definition, this means that there is an arrow
$R_{k}a\to R_{k}b$ and so, as $L_{k}$ is left adjoint to $R_{k}$, there is an
arrow $G_{k}a\to b$. Using the bisimilar companion property, we get

$a\,\leftrightarrow_{k}^{\operatorname{\mathscr{C}}}\,G_{k}a\,\to\,b.$

Therefore, if $a\in\operatorname{\mathscr{D}}$ then also
$b\in\operatorname{\mathscr{D}}$. That is, $\operatorname{\mathscr{D}}$ is
upwards closed with respect to $\rightarrow^{\operatorname{\mathscr{C}}}_{k}$.

The converse direction follows from Remark 4.3. ∎

In order to establish a similar result for property (HP#), recall that a
comonad $G$ is _idempotent_ if its comultiplication $G\Rightarrow GG$ is a
natural isomorphism.

######  Definition 4.6.

A resource-indexed arboreal adjunction between $\operatorname{\mathscr{E}}$
and $\operatorname{\mathscr{C}}$ is _idempotent_ if so are the induced
comonads $G_{k}$, for all $k>0$.

######  Proposition 4.7.

(HP#) holds for any idempotent resource-indexed arboreal adjunction between
$\operatorname{\mathscr{E}}$ and $\operatorname{\mathscr{C}}$.

###### Proof.

Recall that $G_{k}$ is idempotent if, and only if, $\eta R_{k}$ is a natural
isomorphism, where $\eta$ is the unit of the adjunction $L_{k}\dashv R_{k}$.
In particular, for any $a\in\operatorname{\mathscr{E}}$, the component of
$\eta R_{k}$ at $a$ yields an isomorphism $R_{k}a\cong R_{k}G_{k}a$ in
$\operatorname{\mathscr{C}}$. Hence,
$a\cong_{k}^{\operatorname{\mathscr{C}}}G_{k}a$ for all
$a\in\operatorname{\mathscr{E}}$. Reasoning as in the proof of Proposition
4.5, it is easy to see that (HP#) holds. ∎

######  Remark 4.8.

Consider an idempotent resource-indexed arboreal adjunction between
$\operatorname{\mathscr{E}}$ and $\operatorname{\mathscr{C}}$ with induced
comonads $G_{k}$ on $\operatorname{\mathscr{E}}$. The previous proof shows
that, for all $a\in\operatorname{\mathscr{E}}$ and $k>0$, we have
$a\cong_{k}^{\operatorname{\mathscr{C}}}G_{k}a$. A fortiori,
$a\leftrightarrow_{k}^{\operatorname{\mathscr{C}}}G_{k}a$. Therefore, any
idempotent resource-indexed arboreal adjunction satisfies the bisimilar
companion property.

Next, we show how Propositions 4.5 and 4.7 can be exploited to obtain equi-
resource homomorphism preservation theorems for (graded) modal logic and
guarded first-order logics. Relativisations of these results to subclasses of
structures, e.g. to the class of all finite structures, are discussed in
Section 4.4.

### Graded modal logic

Let $\sigma$ be a finite modal vocabulary. As observed in [9, §9.3], the modal
comonads $\mathbb{M}_{k}$ on $\mathbf{Struct}_{\bullet}(\sigma)$ are
idempotent, hence so is the modal resource-indexed arboreal cover of
$\mathbf{Struct}_{\bullet}(\sigma)$ by $\mathscr{R}^{M}_{k}(\sigma)$. This
corresponds to the fact that a tree-ordered Kripke structure is isomorphic to
its tree unravelling. Thus, Proposition 4.7 entails the following _equidepth
homomorphism preservation theorem_ for graded modal formulas (i.e., modal
formulas that possibly contain graded modalities):

######  Theorem 4.9.

The following statements are equivalent for any graded modal formula $\varphi$
of modal depth at most $k$ in a modal vocabulary:

  1. (1)

$\varphi$ is preserved under homomorphisms between pointed Kripke structures.

  2. (2)

$\varphi$ is logically equivalent to an existential positive modal formula of
modal depth at most $k$.

###### Proof.

Fix a graded modal formula $\varphi\in\mathrm{ML}_{k}(\\#)$. Since a single
modal formula contains only finitely many modalities and propositional
variables, we can assume without loss of generality that $\varphi$ is a
formula in a finite modal vocabulary. By Example 3.22 we have

${\rightarrow_{k}^{M}}={\Rrightarrow^{\exists^{+}\mathrm{ML}_{k}}}\ \text{ and
}\ {\cong_{k}^{M}}\subseteq{\equiv^{\mathrm{ML}_{k}(\\#)}}.$

In particular, the latter inclusion entails that the full subcategory
$\operatorname{\mathbf{Mod}}(\varphi)$ of $\mathbf{Struct}_{\bullet}(\sigma)$
is saturated under $\cong_{k}^{M}$. As the modal resource-indexed arboreal
cover is idempotent, Proposition 4.7 implies that
$\operatorname{\mathbf{Mod}}(\varphi)$ is closed under morphisms if, and only
if, it is upwards closed with respect to $\to_{k}^{M}$. Note that
$\operatorname{\mathbf{Mod}}(\varphi)$ is closed under morphisms precisely
when $\varphi$ is preserved under homomorphisms between pointed Kripke
structures. On the other hand, the equality
${\rightarrow_{k}^{M}}={\Rrightarrow^{\exists^{+}\mathrm{ML}_{k}}}$ implies
that $\operatorname{\mathbf{Mod}}(\varphi)$ is upwards closed with respect to
$\to_{k}^{M}$ if, and only if,
$\operatorname{\mathbf{Mod}}(\varphi)=\operatorname{\mathbf{Mod}}(\psi)$ for
some $\psi\in\exists^{+}\mathrm{ML}_{k}$ (this is akin to Lemma 4.1(b) and
hinges on the fact that $\exists^{+}\mathrm{ML}_{k}$ contains finitely many
formulas up to logical equivalence). Thus the statement follows. ∎

######  Remark 4.10.

Forgetting about both graded modalities and modal depth, Theorem 4.9 implies
that a modal formula is preserved under homomorphisms if, and only if, it is
equivalent to an existential positive modal formula. This improves the well
known result that a modal formula is preserved under simulations precisely
when it is equivalent to an existential positive modal formula (see e.g. [15,
Theorem 2.78]).

### Guarded fragments of first-order logic

The study of guarded fragments of first-order logic was initiated by Andréka,
van Benthem and Németi in [12] to analyse, and extend to the first-order
setting, the good algorithmic and model-theoretic properties of modal logic.
_Guarded formulas_ (over a relational vocabulary $\sigma$) are defined by
structural induction, starting from atomic formulas and applying Boolean
connectives and the following restricted forms of quantification: if
$\varphi(\overline{x},\overline{y})$ is a guarded formula, then so are

$\exists\overline{x}.\,G(\overline{x},\overline{y})\wedge\varphi(\overline{x},\overline{y})\
\text{ and }\
\forall\overline{x}.\,G(\overline{x},\overline{y})\to\varphi(\overline{x},\overline{y})$

where $G$ is a so-called _guard_. The (syntactic) conditions imposed on guards
determine different guarded fragments of first-order logic. We shall consider
the following two:

  * •

_Atom guarded:_ $G(\overline{x},\overline{y})$ is an atomic formula in which
all variables in $\overline{x},\overline{y}$ occur.

  * •

_Loosely guarded:_ $G(\overline{x},\overline{y})$ is a conjunction of atomic
formulas such that each pair of variables, one in $\overline{x}$ and the other
in $\overline{x},\overline{y}$, occurs in one of the conjuncts.

The atom guarded fragment of first-order logic was introduced in [12] under
the name of F2 (“Fragment $2$”), whereas the loosely guarded fragment was
defined by van Benthem in [14]. The atom guarded fragment can be regarded as
an extension of modal logic, in the sense that the standard translation of the
latter is contained in the former. In turn, the loosely guarded fragment
extends the atomic one and can express e.g. (the translation of) the _Until_
modality in temporal logic, cf. [14, p. 9].

For each notion of guarding $\mathfrak{g}$ (atomic or loose), denote by

$\mathfrak{g}\mathrm{FO}^{n}\ \text{ and }\
\exists^{+}\mathfrak{g}\mathrm{FO}^{n},$

respectively, the $n$-variable $\mathfrak{g}$-guarded fragment of first-order
logic and its existential positive fragment. In [4], _guarded comonads_
$\mathbb{G}_{n}^{\mathfrak{g}}$ on $\mathbf{Struct}(\sigma)$ are defined for
all $n>0$. The associated categories of Eilenberg-Moore coalgebras are
arboreal and induce the _$\mathfrak{g}$ -guarded resource-indexed arboreal
cover_ of $\mathbf{Struct}(\sigma)$ with resource parameter $n$. For an
explicit description of the resource-indexed arboreal category in question,
cf. [4, §IV].

Assume the vocabulary $\sigma$ is finite and let
$\rightarrow_{n}^{\mathfrak{g}}$ and $\leftrightarrow_{n}^{\mathfrak{g}}$ be
the resource-indexed relations on $\mathbf{Struct}(\sigma)$ induced by the
$\mathfrak{g}$-guarded resource-indexed arboreal cover. It follows from [4,
Theorems III.4 and V.2] that, for all $\sigma$-structures $A,B$ and all $n>0$,

$A\rightarrow_{n}^{\mathfrak{g}}B\ \Longleftrightarrow\
A\Rrightarrow^{\exists^{+}\mathfrak{g}\mathrm{FO}^{n}}B$

and

$A\leftrightarrow_{n}^{\mathfrak{g}}B\ \Longleftrightarrow\
A\equiv^{\mathfrak{g}\mathrm{FO}^{n}}B.$

To obtain an analogue of Lemma 4.1, we consider finite fragments of
$\mathfrak{g}\mathrm{FO}^{n}$ by stratifying in terms of _guarded-quantifier
rank_ (cf. Remark 4.2). Note that, as guarded quantifiers bound _tuples_ of
variables, rather than single variables, the guarded-quantifier rank of a
guarded formula is typically lower than its ordinary quantifier rank.
Nevertheless, for all $k\geq 0$, the fragment
$\mathfrak{g}\mathrm{FO}^{n}_{k}$ of $\mathfrak{g}\mathrm{FO}^{n}$ consisting
of those sentences with guarded-quantifier rank at most $k$ contains finitely
many sentences up to logical equivalence.

This stratification can be modelled in terms of comonads
$\mathbb{G}_{n,k}^{\mathfrak{g}}$ on $\mathbf{Struct}(\sigma)$, for all
$n,k>0$, as explained in [4, §VII]. Fixing $n$ and letting $k$ vary, we obtain
an _$n$ -variable $\mathfrak{g}$-guarded resource-indexed arboreal cover_ of
$\mathbf{Struct}(\sigma)$, with resource parameter $k$. The induced relations
$\rightarrow_{n,k}^{\mathfrak{g}}$ and $\leftrightarrow_{n,k}^{\mathfrak{g}}$
on $\mathbf{Struct}(\sigma)$ coincide, respectively, with preservation of
$\exists^{+}\mathfrak{g}\mathrm{FO}^{n}_{k}$ and equivalence in
$\mathfrak{g}\mathrm{FO}^{n}_{k}$. Thus, for any full subcategory
$\operatorname{\mathscr{D}}$ of $\mathbf{Struct}(\sigma)$:

  * •

$\operatorname{\mathscr{D}}=\operatorname{\mathbf{Mod}}(\varphi)$ for some
$\varphi\in\mathfrak{g}\mathrm{FO}^{n}_{k}$ if, and only if,
$\operatorname{\mathscr{D}}$ is saturated under
$\leftrightarrow_{n,k}^{\mathfrak{g}}$.

  * •

$\operatorname{\mathscr{D}}=\operatorname{\mathbf{Mod}}(\psi)$ for some
$\psi\in\exists^{+}\mathfrak{g}\mathrm{FO}^{n}_{k}$ if, and only if,
$\operatorname{\mathscr{D}}$ is upwards closed with respect to
$\rightarrow_{n,k}^{\mathfrak{g}}$.

As observed in [5, §6.1], the $\mathfrak{g}$-guarded resource-indexed arboreal
cover of $\mathbf{Struct}(\sigma)$ satisfies the bisimilar companion property,
and so does the $n$-variable $\mathfrak{g}$-guarded resource-indexed arboreal
cover for all $n>0$. Therefore, Proposition 4.5 implies the following
_equirank-variable homomorphism preservation theorem_ for guarded logics:

######  Theorem 4.11.

Let $\mathfrak{g}$ be a notion of guarding (either atom or loose). The
following statements are equivalent for any $\mathfrak{g}$-guarded sentence
$\varphi$ in $n$ variables of guarded-quantifier rank at most $k$ in a
relational vocabulary:

  1. (1)

$\varphi$ is preserved under homomorphisms.

  2. (2)

$\varphi$ is logically equivalent to an existential positive
$\mathfrak{g}$-guarded sentence in $n$ variables of guarded-quantifier rank at
most $k$.

###  4.3. Not-so-tame: extendability

A resource-indexed arboreal adjunction may fail to satisfy the bisimilar
companion property, in which case Proposition 4.5 does not apply. This is the
case e.g. for the Ehrenfeucht-Fraïssé resource-indexed arboreal adjunction:

######  Example 4.12.

The Ehrenfeucht-Fraïssé resource-indexed arboreal adjunction between
$\mathbf{Struct}(\sigma)$ and $\mathscr{R}^{E}(\sigma^{I})$ does not have the
bisimilar companion property. Suppose that $\sigma=\\{R\\}$ consists of a
single binary relation symbol and let $A$ be the $\sigma$-structure with
underlying set $\\{a,b\\}$ satisfying $R^{A}=\\{(a,b),(b,a)\\}$. In view of
Examples 3.18 and 3.21, it suffices to find $k>0$ and a first-order sentence
$\varphi$ of quantifier rank $\leq k$ such that

$A\vDash\varphi\ \text{ and }\ H\mathbb{E}_{k}JA\not\vDash\varphi.$

Let $\varphi$ be the sentence $\forall x\forall y\ (x\neq y\Rightarrow xRy)$
of quantifier rank $2$ stating that any two distinct elements are $R$-related.
Then $\varphi$ is satisfied by $A$ but not by $H\mathbb{E}_{k}JA$, because the
sequences $[a]$ and $[b]$ are not $R$-related in $H\mathbb{E}_{k}JA$. This
shows that the bisimilar companion property fails for all $k\geq 2$.

When the bisimilar companion property fails, i.e.
$a\not\leftrightarrow_{k}^{\operatorname{\mathscr{C}}}G_{k}a$ for some
$a\in\operatorname{\mathscr{E}}$ and $k>0$, we may attempt to force it by
finding appropriate extensions $a^{*}$ and $(G_{k}a)^{*}$ of $a$ and $G_{k}a$,
respectively, satisfying
$a^{*}\leftrightarrow_{k}^{\operatorname{\mathscr{C}}}(G_{k}a)^{*}$. This
motivates the notion of _$k$ -extendability_ (see Definition 4.17 below),
inspired by the work of Rossman [38] and its categorical interpretation in
[1].

To start with, we introduce the following notations. Given objects $a,b$ of a
category $\operatorname{\mathscr{A}}$, we write $a\to b$ to denote the
existence of an arrow from $a$ to $b$. Further, we write $a\rightleftarrows b$
to indicate that $a\to b$ and $b\to a$, i.e. $a$ and $b$ are _homomorphically
equivalent_. This applies in particular to coslice categories. Recall that,
for any $c\in\operatorname{\mathscr{A}}$, the _coslice category_
$c/{\operatorname{\mathscr{A}}}$ (also known as _under category_) has as
objects the arrows in $\operatorname{\mathscr{A}}$ with domain $c$. For any
two objects $m\colon c\to a$ and $n\colon c\to b$ of
$c/{\operatorname{\mathscr{A}}}$, an arrow $f\colon m\to n$ in
$c/{\operatorname{\mathscr{A}}}$ is a morphism $f\colon a\to b$ in
$\operatorname{\mathscr{A}}$ such that $f\circ m=n$. Hence, $m\rightleftarrows
n$ in $c/{\operatorname{\mathscr{A}}}$ precisely when there are arrows
$f\colon a\to b$ and $g\colon b\to a$ in $\operatorname{\mathscr{A}}$
satisfying $f\circ m=n$ and $g\circ n=m$. We shall represent this situation by
means of the following diagram:

${c}$${a}$${b}$$\scriptstyle{m}$$\scriptstyle{n}$$\scriptstyle{f}$$\scriptstyle{g}$

######  Remark 4.13.

Note that $m\rightleftarrows n$ in $c/{\operatorname{\mathscr{A}}}$ whenever
there is a section $f\colon a\to b$ in $\operatorname{\mathscr{A}}$ satisfying
$f\circ m=n$. Just observe that the left inverse $f^{-1}$ of $f$ satisfies

$f^{-1}\circ n=f^{-1}\circ f\circ m=m$

and so $n\to m$. Further, $f\circ m=n$ entails $m\to n$. Hence,
$m\rightleftarrows n$.

Now, let $a$ be an object of an arboreal category $\operatorname{\mathscr{C}}$
and let $m\colon P\rightarrowtail a$ be a path embedding. As
$\operatorname{\mathbb{S}}{a}$ is a complete lattice by Lemma 3.10(b), the
supremum $\bigvee{{\uparrow}m}$ in $\operatorname{\mathbb{S}}{a}$ of all path
embeddings above $m$ exists and we shall denote it by

$\mathfrak{i}_{m}\colon\mathscr{S}_{m}\rightarrowtail a.$

Clearly, $m\leq\mathfrak{i}_{m}$ in $\operatorname{\mathbb{S}}{a}$, and so
there is a path embedding

$m_{\star}\colon P\rightarrowtail\mathscr{S}_{m}$

satisfying $\mathfrak{i}_{m}\circ m_{\star}=m$. (Note that $\mathfrak{i}_{m}$
is well defined only up to isomorphism in the coslice category
${\operatorname{\mathscr{C}}}/a$, but as usual we work with representatives
for isomorphism classes.)

######  Remark 4.14.

To provide an intuition for the previous definition, let us say for the sake
of this remark that a path embedding $m\colon P\rightarrowtail a$ is “dense in
$a$” if all elements of $\operatorname{\mathbb{P}}{a}$ are comparable with
$m$. Then Lemma 4.15(a) below implies that
$\mathfrak{i}_{m}\colon\mathscr{S}_{m}\rightarrowtail a$ is the largest
$\mathscr{M}$-subobject of $a$ in which $m$ is dense.

######  Lemma 4.15.

The following statements hold for all path embeddings ${m\colon
P\rightarrowtail a}$:

  1. (a)

$\operatorname{\mathbb{P}}{\mathscr{S}_{m}}$ is isomorphic to the subtree of
$\operatorname{\mathbb{P}}{a}$ consisting of the elements that are comparable
with $m$.

  2. (b)

For all path embeddings $n\colon P\rightarrowtail b$ and arrows $f\colon a\to
b$ such that ${f\circ m=n}$, there is a unique
$g\colon\mathscr{S}_{m}\to\mathscr{S}_{n}$ making the following diagram
commute.

${\mathscr{S}_{m}}$${\mathscr{S}_{n}}$${a}$${b}$$\scriptstyle{\mathfrak{i}_{m}}$$\scriptstyle{g}$$\scriptstyle{\mathfrak{i}_{n}}$$\scriptstyle{f}$

  3. (c)

For all path embeddings $n\colon P\rightarrowtail b$, if $m\to n$ then
$m_{\star}\to n_{\star}$.

###### Proof.

(a) The map
$\mathfrak{i}_{m}\circ-\colon\operatorname{\mathbb{S}}{\mathscr{S}_{m}}\to\operatorname{\mathbb{S}}{a}$
is an order-embedding by Lemma 3.3, and so its restriction
$\operatorname{\mathbb{P}}{\mathscr{S}_{m}}\to\operatorname{\mathbb{P}}{a}$ is
an injective forest morphism. Hence,
$\operatorname{\mathbb{P}}{\mathscr{S}_{m}}$ is isomorphic to the subtree of
$\operatorname{\mathbb{P}}{a}$ consisting of those elements that factor
through $\mathfrak{i}_{m}$, i.e. that are below $\bigvee{{\uparrow}m}$. By
Lemma 3.10(c), an element of $\operatorname{\mathbb{P}}{a}$ is below
$\bigvee{{\uparrow}m}$ precisely when it is below some element of
${\uparrow}m$. In turn, the latter is equivalent to being comparable with $m$.

(b) Since $\mathscr{S}_{m}$ is path-generated, it is the colimit of the
canonical cocone $C$ of path embeddings over the small diagram
$\operatorname{\mathbb{P}}{\mathscr{S}_{m}}$ which, by item (a), can be
identified with the subdiagram of $\operatorname{\mathbb{P}}{a}$ consisting of
those elements comparable with $m$. As
$\operatorname{\mathbb{P}}{(f\circ\mathfrak{i}_{m})}$ is monotone, it sends
path embeddings comparable with $m$ to path embeddings comparable with $n$,
and so the cocone $\\{f\circ\mathfrak{i}_{m}\circ p\mid p\in C\\}$ factors
through $\mathfrak{i}_{n}\colon\mathscr{S}_{n}\rightarrowtail b$. Hence, there
is $g\colon\mathscr{S}_{m}\to\mathscr{S}_{n}$ such that $\mathfrak{i}_{n}\circ
g=f\circ\mathfrak{i}_{m}$. Finally, note that if
$g^{\prime}\colon\mathscr{S}_{m}\to\mathscr{S}_{n}$ satisfies
$\mathfrak{i}_{n}\circ g^{\prime}=f\circ\mathfrak{i}_{m}$ then we have
$\mathfrak{i}_{n}\circ g=\mathfrak{i}_{n}\circ g^{\prime}$, and so
$g=g^{\prime}$ because $\mathfrak{i}_{n}$ is monic.

(c) Suppose there exists $f\colon a\to b$ such that $f\circ m=n$. By the item
(b), there is $g\colon\mathscr{S}_{m}\to\mathscr{S}_{n}$ such that
$\mathfrak{i}_{n}\circ g=f\circ\mathfrak{i}_{m}$. Therefore,

$\mathfrak{i}_{n}\circ g\circ m_{\star}=f\circ\mathfrak{i}_{m}\circ
m_{\star}=f\circ m=n=\mathfrak{i}_{n}\circ n_{\star}$

and so $g\circ m_{\star}=n_{\star}$ because $\mathfrak{i}_{n}$ is a
monomorphism. ∎

######  Remark 4.16.

Lemma 4.15(c) entails that $m_{\star}\to n_{\star}$ whenever $m_{\star}\to n$.
Just observe that $(m_{\star})_{\star}$ can be identified with $m_{\star}$.

######  Definition 4.17.

Consider a resource-indexed arboreal adjunction between
$\operatorname{\mathscr{E}}$ and $\operatorname{\mathscr{C}}$, with
adjunctions $L_{k}\dashv R_{k}$. An object $a$ of $\operatorname{\mathscr{E}}$
is _$k$ -extendable_ if it satisfies the following property for all
$e\in\operatorname{\mathscr{E}}$: For all path embeddings $m\colon
P\rightarrowtail R_{k}a$ and $n\colon P\rightarrowtail R_{k}e$ such that
$m_{\star}\rightleftarrows n_{\star}$ in the coslice category
$P/{\operatorname{\mathscr{C}}_{k}}$ (see the leftmost diagram below),

${P}$${\mathscr{S}_{m}}$${\mathscr{S}_{n}}$$\scriptstyle{m_{\star}}$$\scriptstyle{n_{\star}}$${Q}$${\mathscr{S}_{m^{\prime}}}$${\mathscr{S}_{n^{\prime}}}$$\scriptstyle{m^{\prime}_{\star}}$$\scriptstyle{n^{\prime}_{\star}}$

if $n^{\prime}\colon Q\rightarrowtail R_{k}e$ is a path embedding satisfying
$n\leq n^{\prime}$ in $\operatorname{\mathbb{P}}{(R_{k}e)}$, there is a path
embedding $m^{\prime}\colon Q\rightarrowtail R_{k}a$ such that $m\leq
m^{\prime}$ in $\operatorname{\mathbb{P}}{(R_{k}a)}$ and
$m^{\prime}_{\star}\rightleftarrows n^{\prime}_{\star}$ in
$Q/{\operatorname{\mathscr{C}}_{k}}$ (as displayed in the rightmost diagram
above).

We shall see in Proposition 4.19 below that, under appropriate assumptions,
the $k$-extendability property allows us to upgrade the relation
$\rightleftarrows_{k}^{\operatorname{\mathscr{C}}}$ to the finer relation
$\leftrightarrow_{k}^{\operatorname{\mathscr{C}}}$. For the next lemma, recall
that a category is _locally finite_ if there are finitely many arrows between
any two of its objects.

######  Lemma 4.18.

Let $\operatorname{\mathscr{C}}$ be an arboreal category whose full
subcategory $\operatorname{\mathscr{C}}_{p}$ consisting of the paths is
locally finite. If $f\colon P\twoheadrightarrow Q$ and $g\colon
Q\twoheadrightarrow P$ are quotients between paths, then $f$ and $g$ are
inverse to each other.

###### Proof.

The set $M$ of quotients $P\twoheadrightarrow P$ is a finite monoid with
respect to composition, and it satisfies the right-cancellation law because
every quotient is an epimorphism. Hence $M$ is a group, and so $g\circ f\in M$
has an inverse. It follows that $g\circ f$ is an embedding. Because there is
at most one embedding between any two paths by Lemma 3.10(a), $g\circ
f=\mathrm{id}_{P}$. By symmetry, also $f\circ g=\mathrm{id}_{Q}$. ∎

######  Proposition 4.19.

Consider a resource-indexed arboreal adjunction between
$\operatorname{\mathscr{E}}$ and $\operatorname{\mathscr{C}}$ such that
$\operatorname{\mathscr{C}}_{p}^{k}$ is locally finite for all $k>0$. For all
$k$-extendable objects $a,b$ of $\operatorname{\mathscr{E}}$ admitting a
product, we have $a\rightleftarrows_{k}^{\operatorname{\mathscr{C}}}b$ if and
only if $a\leftrightarrow_{k}^{\operatorname{\mathscr{C}}}b$.

###### Proof.

Fix an arbitrary $k>0$ and recall that $\operatorname{\mathscr{C}}_{k}$ is an
arboreal category. The “if” part of the statement follows from the inclusion
${\leftrightarrow_{k}^{\operatorname{\mathscr{C}}}}\subseteq{\rightleftarrows_{k}^{\operatorname{\mathscr{C}}}}$.

For the “only if” part suppose that
$a\rightleftarrows_{k}^{\operatorname{\mathscr{C}}}b$, i.e. $R_{k}a$ and
$R_{k}b$ are homomorphically equivalent in $\operatorname{\mathscr{C}}_{k}$.
To improve readability, let $X\coloneqq R_{k}a$ and $Y\coloneqq R_{k}b$. We
must prove that $X$ and $Y$ are bisimilar. As $X$ and $Y$ admit a product in
$\operatorname{\mathscr{C}}_{k}$, namely the image under $R_{k}$ of the
product of $a$ and $b$ in $\operatorname{\mathscr{E}}$, by Theorem 3.14 it
suffices to show that $X$ and $Y$ are back-and-forth equivalent.

Fix arbitrary morphisms $f\colon X\to Y$ and $g\colon Y\to X$, and let $m$ and
$n$ denote generic elements of $\operatorname{\mathbb{P}}{X}$ and
$\operatorname{\mathbb{P}}{Y}$, respectively. We claim that

$\mathcal{B}\coloneqq\\{\llbracket m,n\rrbracket\mid\exists\
s\colon\mathscr{S}_{m}\to\mathscr{S}_{n},\,t\colon\mathscr{S}_{n}\to\mathscr{S}_{m}\
\text{s.t.}\ \operatorname{\mathbb{P}}{s}(m_{\star})=n_{\star}\ \text{and}\
\operatorname{\mathbb{P}}{t}(n_{\star})=m_{\star}\\}$

is a back-and-forth system between $X$ and $Y$, i.e. it satisfies items
(i)–(iii) in Definition 3.13. For item (i), let $\bot_{X},\bot_{Y}$ be the
roots of $\operatorname{\mathbb{P}}{X}$ and $\operatorname{\mathbb{P}}{Y}$,
respectively. Note that $\mathscr{S}_{\bot_{X}}$ and $\mathscr{S}_{\bot_{Y}}$
can be identified, respectively, with $X$ and $Y$. As
$\operatorname{\mathbb{P}}{f}$ and $\operatorname{\mathbb{P}}{g}$ are forest
morphisms, $\operatorname{\mathbb{P}}{f}(\bot_{X})=\bot_{Y}$ and
$\operatorname{\mathbb{P}}{g}(\bot_{Y})=\bot_{X}$. So,
$\llbracket\bot_{X},\bot_{Y}\rrbracket\in\mathcal{B}$.

For item (ii), suppose $\llbracket m,n\rrbracket\in\mathcal{B}$ and let
$m^{\prime}\in\operatorname{\mathbb{P}}{X}$ satisfy $m\prec m^{\prime}$. We
seek $n^{\prime}\in\operatorname{\mathbb{P}}{Y}$ such that $n\prec n^{\prime}$
and $\llbracket m^{\prime},n^{\prime}\rrbracket\in\mathcal{B}$. By assumption,
there are arrows $s\colon\mathscr{S}_{m}\to\mathscr{S}_{n}$ and
$t\colon\mathscr{S}_{n}\to\mathscr{S}_{m}$ such that
$\operatorname{\mathbb{P}}{s}(m_{\star})=n_{\star}$ and
$\operatorname{\mathbb{P}}{t}(n_{\star})=m_{\star}$. Writing
$P\coloneqq\operatorname{dom}(m)$ and
$P^{\prime}\coloneqq\operatorname{dom}(n)$, we have the following diagrams

${P}$${{\cdot}}$${P^{\prime}}$${\mathscr{S}_{m}}$${\mathscr{S}_{n}}$$\scriptstyle{e}$$\scriptstyle{m_{\star}}$$\scriptstyle{\operatorname{\mathbb{P}}{s}(m_{\star})}$$\scriptstyle{\varphi}$$\scriptstyle{n_{\star}}$$\scriptstyle{s}$${P^{\prime}}$${{\cdot}}$${P}$${\mathscr{S}_{n}}$${\mathscr{S}_{m}}$$\scriptstyle{e^{\prime}}$$\scriptstyle{n_{\star}}$$\scriptstyle{\operatorname{\mathbb{P}}{t}(n_{\star})}$$\scriptstyle{\psi}$$\scriptstyle{m_{\star}}$$\scriptstyle{t}$

where $\varphi$ and $\psi$ are isomorphisms. By Lemma 4.18, $\varphi\circ e$
and $\psi\circ e^{\prime}$ are inverse to each other, thus the left-hand
diagram below commutes.

${P}$${\mathscr{S}_{m}}$${\mathscr{S}_{n}}$$\scriptstyle{m_{\star}}$$\scriptstyle{n_{\star}\circ\varphi\circ
e}$$\scriptstyle{s}$$\scriptstyle{t}$${Q}$${\mathscr{S}_{m^{\prime}}}$${\mathscr{S}_{n^{\prime}}}$$\scriptstyle{m^{\prime}_{\star}}$$\scriptstyle{n^{\prime}_{\star}}$$\scriptstyle{s^{\prime}}$$\scriptstyle{t^{\prime}}$

Let $Q\coloneqq\operatorname{dom}(m^{\prime})$. Since $b$ is $k$-extendable,
there exist a path embedding $n^{\prime}\colon Q\rightarrowtail Y$ such that
$n\leq n^{\prime}$ in $\operatorname{\mathbb{P}}{Y}$, and arrows
$s^{\prime}\colon\mathscr{S}_{m^{\prime}}\to\mathscr{S}_{n^{\prime}}$ and
$t^{\prime}\colon\mathscr{S}_{n^{\prime}}\to\mathscr{S}_{m^{\prime}}$ making
the right-hand diagram above commute. It follows that $\llbracket
m^{\prime},n^{\prime}\rrbracket\in\mathcal{B}$; just observe that
$\operatorname{\mathbb{P}}{s^{\prime}}(m^{\prime}_{\star})=n^{\prime}_{\star}$
because the composite $s^{\prime}\circ m^{\prime}_{\star}$ is an embedding,
and similarly
$\operatorname{\mathbb{P}}{t^{\prime}}(n^{\prime}_{\star})=m^{\prime}_{\star}$.

It remains to show that $n\prec n^{\prime}$. For any element $x$ of a tree,
denote by $\operatorname{\mathrm{ht}}(x)$ its height. As $n\leq n^{\prime}$ in
$\operatorname{\mathbb{P}}{Y}$, it is enough to show that
$\operatorname{\mathrm{ht}}(n^{\prime})=\operatorname{\mathrm{ht}}(n)+1$.
Using the fact that forest morphisms preserve the height of points and
$\operatorname{\mathbb{P}}{s^{\prime}}(m^{\prime}_{\star})=n^{\prime}_{\star}$,
we get

$\operatorname{\mathrm{ht}}(n^{\prime})=\operatorname{\mathrm{ht}}(n^{\prime}_{\star})=\operatorname{\mathrm{ht}}(m^{\prime}_{\star})=\operatorname{\mathrm{ht}}(m^{\prime})=\operatorname{\mathrm{ht}}(m)+1.$

Item (iii) is proved in a similar way using the fact that $a$ is
$k$-extendable. ∎

######  Definition 4.20.

Consider a resource-indexed arboreal adjunction between
$\operatorname{\mathscr{E}}$ and $\operatorname{\mathscr{C}}$, and an object
$a\in\operatorname{\mathscr{E}}$. For all $k>0$, a _$k$ -extendable cover_ of
$a$ is a section $a\to a^{*}$ in $\operatorname{\mathscr{E}}$ such that
$a^{*}$ is $k$-extendable.

######  Proposition 4.21.

(HP) holds for any resource-indexed arboreal adjunction between
$\operatorname{\mathscr{E}}$ and $\operatorname{\mathscr{C}}$ satisfying the
following properties for all $k>0$:

  1. (i)

$\operatorname{\mathscr{C}}_{p}^{k}$ is locally finite.

  2. (ii)

$\operatorname{\mathscr{E}}$ has binary products and each of its objects
admits a $k$-extendable cover.

###### Proof.

Fix a full subcategory $\operatorname{\mathscr{D}}$ of
$\operatorname{\mathscr{E}}$ saturated under
$\leftrightarrow_{k}^{\operatorname{\mathscr{C}}}$. For the non-trivial
implication in (HP), assume $\operatorname{\mathscr{D}}$ is closed under
morphisms and let $a,b\in\operatorname{\mathscr{E}}$ satisfy
$a\rightarrow^{\operatorname{\mathscr{C}}}_{k}b$ and
$a\in\operatorname{\mathscr{D}}$.

If $G_{k}\coloneqq L_{k}R_{k}$, then
$a\rightarrow^{\operatorname{\mathscr{C}}}_{k}b$ implies $G_{k}a\to b$. Let
$s\colon a\to a^{*}$ and $t\colon G_{k}a\to(G_{k}a)^{*}$ be sections with
$a^{*}$ and $(G_{k}a)^{*}$ $k$-extendable objects. It follows from Lemma
3.20(a) that $a\rightleftarrows_{k}^{\operatorname{\mathscr{C}}}a^{*}$ and
$G_{k}a\rightleftarrows_{k}^{\operatorname{\mathscr{C}}}(G_{k}a)^{*}$. By
Lemma 3.20(b) we have
$a\rightleftarrows_{k}^{\operatorname{\mathscr{C}}}G_{k}a$ and so, by
transitivity,
$a^{*}\rightleftarrows_{k}^{\operatorname{\mathscr{C}}}(G_{k}a)^{*}$. An
application of Proposition 4.19 yields
$a^{*}\leftrightarrow_{k}^{\operatorname{\mathscr{C}}}(G_{k}a)^{*}$. We thus
have the following diagram, where $t^{-1}$ denotes the left inverse of $t$.

${a^{*}}$${{\leftrightarrow_{k}^{\operatorname{\mathscr{C}}}}}$${(G_{k}a)^{*}}$${a}$${{\rightleftarrows_{k}^{\operatorname{\mathscr{C}}}}}$${G_{k}a}$${b}$$\scriptstyle{s}$$\scriptstyle{t^{-1}}$

Since $a\in\operatorname{\mathscr{D}}$, and $\operatorname{\mathscr{D}}$ is
saturated under $\leftrightarrow_{k}^{\operatorname{\mathscr{C}}}$ and closed
under morphisms, all the objects in the diagram above sit in
$\operatorname{\mathscr{D}}$. In particular, $b\in\operatorname{\mathscr{D}}$
and thus (HP) holds. ∎

###  4.4. Relativising to full subcategories

Let $\operatorname{\mathscr{E}}^{\prime}$ be a full subcategory of
$\operatorname{\mathscr{E}}$. We say that (HP) holds _relative to
$\operatorname{\mathscr{E}}^{\prime}$_ if the following condition is
satisfied: For any full subcategory $\operatorname{\mathscr{D}}$ of
$\operatorname{\mathscr{E}}$ saturated under
$\leftrightarrow_{k}^{\operatorname{\mathscr{C}}}$,
$\operatorname{\mathscr{D}}\cap\operatorname{\mathscr{E}}^{\prime}$ is closed
under morphisms in $\operatorname{\mathscr{E}}^{\prime}$ precisely when it is
upwards closed in $\operatorname{\mathscr{E}}^{\prime}$ with respect to
$\rightarrow^{\operatorname{\mathscr{C}}}_{k}$. Likewise for (HP#).

For the next proposition, observe that in order for a comonad $G$ on
$\operatorname{\mathscr{E}}$ to restrict to a full subcategory
$\operatorname{\mathscr{E}}^{\prime}$ of $\operatorname{\mathscr{E}}$ it is
necessary and sufficient that $Ga\in\operatorname{\mathscr{E}}^{\prime}$ for
all $a\in\operatorname{\mathscr{E}}^{\prime}$.

######  Proposition 4.22.

Consider a resource-indexed arboreal adjunction between
$\operatorname{\mathscr{E}}$ and $\operatorname{\mathscr{C}}$, and let
$\operatorname{\mathscr{E}}^{\prime}$ be a full subcategory of
$\operatorname{\mathscr{E}}$ such that the induced comonads $G_{k}\coloneqq
L_{k}R_{k}$ restrict to $\operatorname{\mathscr{E}}^{\prime}$. If the
resource-indexed arboreal adjunction has the bisimilar companion property then
(HP) holds relative to $\operatorname{\mathscr{E}}^{\prime}$. If it is
idempotent then (HP#) holds relative to $\operatorname{\mathscr{E}}^{\prime}$.

###### Proof.

The same, mutatis mutandis, as for Propositions 4.5 and 4.7, respectively. ∎

Since the modal comonads $\mathbb{M}_{k}$ restrict to finite pointed Kripke
structures, the previous result yields a variant of Theorem 4.9 for finite
structures:

######  Theorem 4.23.

The following statements are equivalent for any graded modal formula $\varphi$
of modal depth at most $k$ in a modal vocabulary:

  1. (1)

$\varphi$ is preserved under homomorphisms between finite pointed Kripke
structures.

  2. (2)

$\varphi$ is logically equivalent over finite pointed Kripke structures to an
existential positive modal formula of modal depth at most $k$.

Similarly, since the guarded comonads $\mathbb{G}_{n,k}^{\mathfrak{g}}$
restrict to finite structures, we obtain the following variant of Theorem 4.11
for finite structures:

######  Theorem 4.24.

Let $\mathfrak{g}$ be a notion of guarding (either atom or loose). The
following statements are equivalent for any $\mathfrak{g}$-guarded sentence
$\varphi$ in $n$ variables of guarded-quantifier rank at most $k$ in a
relational vocabulary:

  1. (1)

$\varphi$ is preserved under homomorphisms between finite structures.

  2. (2)

$\varphi$ is logically equivalent over finite structures to an existential
positive $\mathfrak{g}$-guarded sentence in $n$ variables of guarded-
quantifier rank at most $k$.

In all our examples of resource-indexed arboreal adjunctions and covers, the
counits of the induced comonads $G_{k}\coloneqq L_{k}R_{k}$ are componentwise
surjective. The next easy observation, combined with Proposition 4.22, then
provides a useful criterion to relativise equi-resource homomorphism
preservation theorems to subclasses of structures. Recall that a _negative
formula_ is one obtained from negated atomic formulas and
$\vee,\wedge,\exists,\forall$.

######  Lemma 4.25.

Let $G$ be a comonad on $\mathbf{Struct}(\sigma)$ whose counit is
componentwise surjective and let $T$ be a set of negative sentences. Then $G$
restricts to $\operatorname{\mathbf{Mod}}(T)$.

###### Proof.

If $\psi\in T$, its negation is logically equivalent to a positive sentence
$\chi$. Positive sentences are preserved under surjective homomorphisms and
so, for all $A\in\mathbf{Struct}(\sigma)$, considering the component of the
counit $GA\twoheadrightarrow A$ we obtain

$GA\models\chi\ \Longrightarrow\ A\models\chi.$

I.e., $G$ restricts to $\operatorname{\mathbf{Mod}}(\psi)$. As
$\operatorname{\mathbf{Mod}}(T)=\bigcap_{\psi\in
T}{\operatorname{\mathbf{Mod}}(\psi)}$, the statement follows. ∎

The counits of the guarded comonads $\mathbb{G}_{n,k}^{\mathfrak{g}}$ are
componentwise surjective, thus the equirank-variable homomorphism preservation
theorem for guarded logics and its finite variant (Theorems 4.11 and 4.24,
respectively) admit a relativisation to any full subcategory of the form
$\operatorname{\mathbf{Mod}}(T)$ where $T$ is a set of negative
$\mathfrak{g}$-guarded sentences.

The counits of the modal comonads $\mathbb{M}_{k}$ are also componentwise
surjective. As positive modal formulas are preserved under surjective
homomorphisms between pointed Kripke structures, a slight variant of Lemma
4.25 shows that the comonads $\mathbb{M}_{k}$ restrict to any full subcategory
of the form $\operatorname{\mathbf{Mod}}(T)$, with $T$ a set of negative modal
formulas. Hence, the equidepth homomorphism preservation theorem for graded
modal logic and its finite version (Theorems 4.9 and 4.23, respectively) can
be relativised to any such subcategory.

Relativisations to subclasses of structures can be obtained even in the
absence of the bisimilar companion property; in that case, we need to ensure
that $k$-extendable covers can be constructed within the subclass. We defer
the statement of this result to Section 5.2 (see Corollary 5.11).

##  5\. An Axiomatic Approach

In this section, we identify sufficient conditions on a resource-indexed
arboreal adjunction between $\operatorname{\mathscr{E}}$ and
$\operatorname{\mathscr{C}}$ ensuring that property (HP) is satisfied (see
Corollary 5.10). We introduce first conditions (E1)–(E2) on
$\operatorname{\mathscr{E}}$ in Section 5.1 and then, in Section 5.2,
conditions (A1)–(A4) on the adjunctions. In Section 5.3, we derive a slight
generalisation of the equirank homomorphism preservation theorem by showing
that these conditions are satisfied by the Ehrenfeucht-Fraïssé resource-
indexed arboreal adjunction.

######  Remark 5.1.

Let us point out that we cannot derive from this axiomatic approach an
_equivariable_ homomorphism preservation theorem, whereby the number of
variables in a sentence is preserved, let alone an _equirank-variable_ one. In
fact, the corresponding ($k$-round) $n$-pebble comonads do not satisfy
property (A3) below. On the other hand, under the additional assumption that
$k\leq n+2$, where $k$ is the quantifier rank and $n$ is the number of
variables in a sentence, an equirank-variable homomorphism preservation
theorem was proved by Paine in [35]. Also, our approach does not readily apply
to _hybrid logic_ because the hybrid comonads $\mathbb{H}_{k}$ in [5] do not
satisfy the path restriction property (A4) (cf. Definition 5.8).

###  5.1. Axioms for the extensional category

We require that the category $\operatorname{\mathscr{E}}$ have the following
properties:

  1. (E1)

$\operatorname{\mathscr{E}}$ has all finite limits and small colimits.

  2. (E2)

$\operatorname{\mathscr{E}}$ is equipped with a proper factorisation system
such that:

     * •

Embeddings are stable under pushouts along embeddings.

     * •

Pushout squares of embeddings are also pullbacks.

     * •

Pushout squares of embeddings are stable under pullbacks along embeddings.

######  Remark 5.2.

Note that property (E2) only involves one half of the factorisation system,
namely the embeddings. In fact, it could be weakened to the requirement that
$\operatorname{\mathscr{E}}$ admit a class of monomorphisms $\mathscr{N}$
satisfying appropriate properties. When $\mathscr{N}$ is the class of all
monomorphisms, these are akin to the conditions for an _adhesive category_ ,
cf. [29].

######  Example 5.3.

If $\sigma$ is a relational vocabulary, $\mathbf{Struct}(\sigma)$ satisfies
(E1)–(E2). In fact, it is well known that $\mathbf{Struct}(\sigma)$ is
complete and cocomplete, hence it satisfies (E1). For (E2), consider the
proper factorisation system given by surjective homomorphisms and embeddings.
Up to isomorphism, embeddings can be identified with inclusions of induced
substructures. The pushout of a span of embeddings in
$\mathbf{Struct}(\sigma)$ can be identified with a union of structures, and so
embeddings are stable under pushouts along embeddings. The remaining two
conditions in (E2) hold because they are satisfied in
$\operatorname{\mathbf{Set}}$ by the class of monomorphism, and the forgetful
functor $\mathbf{Struct}(\sigma)\to\operatorname{\mathbf{Set}}$ preserves and
reflects pullback and pushout diagrams consisting of embeddings.

We note in passing that properties (E1)–(E2) are stable under taking coslices:

######  Lemma 5.4.

If a category $\operatorname{\mathscr{E}}$ satisfies (E1)–(E2), then so does
$e/{\operatorname{\mathscr{E}}}$ for all $e\in\operatorname{\mathscr{E}}$.

###### Proof.

Fix an arbitrary object $e\in\operatorname{\mathscr{E}}$. It is well known
that limits and colimits in $e/{\operatorname{\mathscr{E}}}$ are inherited
from $\operatorname{\mathscr{E}}$, so $e/{\operatorname{\mathscr{E}}}$
satisfies (E1) because $\operatorname{\mathscr{E}}$ does.

By assumption, $\operatorname{\mathscr{E}}$ admits a proper factorisation
system satisfying (E2). Let $\mathscr{Q}$ and $\mathscr{M}$ be the classes of
arrows in $e/{\operatorname{\mathscr{E}}}$ whose underlying morphisms in
$\operatorname{\mathscr{E}}$ are quotients and embeddings, respectively. It is
folklore that $(\mathscr{Q},\mathscr{M})$ is a weak factorisation system in
$e/{\operatorname{\mathscr{E}}}$. Moreover, this factorisation system is
proper because the codomain functor $\operatorname{cod}\colon
e/{\operatorname{\mathscr{E}}}\to\operatorname{\mathscr{E}}$ is faithful.
Recall that $\operatorname{cod}\colon
e/{\operatorname{\mathscr{E}}}\to\operatorname{\mathscr{E}}$ preserves
pushouts, so embeddings in $e/{\operatorname{\mathscr{E}}}$ are stable under
pushouts along embeddings because the corresponding property is satisfied in
$\operatorname{\mathscr{E}}$. The remaining two properties in (E2) follow by a
similar reasoning, using the fact that $\operatorname{cod}\colon
e/{\operatorname{\mathscr{E}}}\to\operatorname{\mathscr{E}}$ preserves and
reflects limits and pushouts. ∎

######  Example 5.5.

It follows from Example 5.3 and Lemma 5.4 that, for all relational
vocabularies $\sigma$, the category $\mathbf{Struct}_{\bullet}(\sigma)$ of
pointed $\sigma$-structures satisfies (E1)–(E2).

###  5.2. Axioms for the resource-indexed adjunctions

We now assume that the extensional category $\operatorname{\mathscr{E}}$
satisfies (E1)–(E2), and proceed to introduce conditions on the resource-
indexed arboreal adjunction between $\operatorname{\mathscr{E}}$ and
$\operatorname{\mathscr{C}}$. To start with, consider an arbitrary adjunction
$L\dashv R\colon\operatorname{\mathscr{E}}\to\operatorname{\mathscr{C}}$. As
with any adjunction, there are hom-set bijections

$\operatorname{\mathscr{E}}(Lc,e)\longrightarrow\operatorname{\mathscr{C}}(c,Ra),\enspace
f\mapsto f^{\flat}$

natural in $c\in\operatorname{\mathscr{C}}$ and
$e\in\operatorname{\mathscr{E}}$. Explicitly, $f^{\flat}$ is defined as the
composite

${c}$${RLc}$${Re}$$\scriptstyle{\eta_{c}}$$\scriptstyle{Rf}$

where $\eta$ is the unit of the adjunction $L\,{\dashv}\,R$. The inverse of
the function $f\mapsto f^{\flat}$ sends $g\in\operatorname{\mathscr{C}}(c,Re)$
to the morphism $g^{\\#}$ given by the composition

${Lc}$${LRe}$${e,}$$\scriptstyle{Lg}$$\scriptstyle{\varepsilon_{e}}$

where $\varepsilon$ is the counit of the adjunction. Naturality of these
bijections means that

$(f_{1}\circ f_{2})^{\flat}=Rf_{1}\circ f_{2}^{\flat}$

for all morphisms $f_{1}\colon e\to e^{\prime}$ and $f_{2}\colon Lc\to e$ in
$\operatorname{\mathscr{E}}$, and

$(g_{1}\circ g_{2})^{\\#}=g_{1}^{\\#}\circ Lg_{2}$

for all morphisms $g_{1}\colon c\to Re$ and $g_{2}\colon c^{\prime}\to c$ in
$\operatorname{\mathscr{C}}$.

Next, we introduce the path restriction property for resource-indexed arboreal
adjunctions. In a nutshell, this states that whenever
$a\in\operatorname{\mathscr{E}}$ embeds into the image under $L_{k}$ of a
path, $a$ itself can be equipped with a path structure. Furthermore, these
path structures can be chosen in a coherent fashion. We start with an
auxiliary definition:

######  Definition 5.6.

Consider a resource-indexed arboreal adjunction between
$\operatorname{\mathscr{E}}$ and $\operatorname{\mathscr{C}}$. A path
$P\in\operatorname{\mathscr{C}}_{p}^{k}$ is _smooth_ if there exist
$e\in\operatorname{\mathscr{E}}$ and an embedding $P\rightarrowtail R_{k}e$.

######  Remark 5.7.

The motivation for considering smooth paths arises from the fact that, when
considering a fresh binary relation symbol $I$ modelling equality in the logic
(cf. Example 3.18), the interpretation of $I$ in these paths is always an
equivalence relation.

######  Definition 5.8.

A resource-indexed arboreal adjunction between $\operatorname{\mathscr{E}}$
and $\operatorname{\mathscr{C}}$ has the _path restriction property_ if, for
all smooth paths $Q\in\operatorname{\mathscr{C}}_{p}^{k}$ and embeddings
${j\colon a\rightarrowtail L_{k}Q}$, there is a path
$Q_{a}\in\operatorname{\mathscr{C}}_{p}^{k}$ such that $L_{k}Q_{a}\cong a$ and
the following conditions are satisfied:

  1. (i)

For all path embeddings $!_{P,Q}\colon P\rightarrowtail Q$ in
$\operatorname{\mathscr{C}}_{k}$ and all commutative diagrams

${L_{k}P}$${a}$${L_{k}Q}$$\scriptstyle{L_{k}(!_{P,Q})}$$\scriptstyle{f}$$\scriptstyle{j}$

there is an arrow $\ell\colon P\to Q_{a}$ such that $L_{k}\ell=f$.

  2. (ii)

For all path embeddings $!_{P,Q}\colon P\rightarrowtail Q$ such that
$L_{k}(!_{P,Q})$ is an embedding, the pullback of $L_{k}(!_{P,Q})$ along $j$
is of the form $L_{k}\ell$ for some $\ell\colon Q_{b}\to Q_{a}$.

${b}$${L_{k}P}$${a}$${L_{k}Q}$${\lrcorner}$$\scriptstyle{L_{k}\ell}$$\scriptstyle{L_{k}(!_{P,Q})}$$\scriptstyle{j}$

Finally, recall that an object $a$ of a category $\operatorname{\mathscr{A}}$
is _finitely presentable_ if the associated hom-functor
$\operatorname{\mathscr{A}}(a,-)\colon\operatorname{\mathscr{A}}\to\operatorname{\mathbf{Set}}$
preserves directed colimits.

With regards to the resource-indexed arboreal adjunction, we assume the
following properties are satisfied for all $k>0$ and all paths
$P\in\operatorname{\mathscr{C}}_{p}^{k}$:

  1. (A1)

The category $\operatorname{\mathscr{C}}_{p}^{k}$ is locally finite and has
finitely many objects up to isomorphism.

  2. (A2)

$L_{k}P$ is finitely presentable in $\operatorname{\mathscr{E}}$.

  3. (A3)

For all arrows $m\colon P\to R_{k}a$ in $\operatorname{\mathscr{C}}_{k}$, if
$m$ is an embedding then so is $m^{\\#}\colon L_{k}P\to a$. The converse holds
whenever $P$ is smooth.

  4. (A4)

The path restriction property is satisfied.

######  Theorem 5.9.

Consider a resource-indexed arboreal adjunction between
$\operatorname{\mathscr{E}}$ and $\operatorname{\mathscr{C}}$ satisfying
(E1)–(E2) and (A1)–(A4). For all $a\in\operatorname{\mathscr{E}}$ and all
$k>0$, there exists a $k$-extendable cover of $a$.

The proof of the previous key fact is deferred to Section 6. Let us point out
the following immediate consequence:

######  Corollary 5.10.

(HP) holds for all resource-indexed arboreal adjunctions satisfying (E1)–(E2)
and (A1)–(A4).

###### Proof.

By Proposition 4.21 and Theorem 5.9. ∎

We can also deduce the following relativisation result. Let us say that a full
subcategory $\operatorname{\mathscr{D}}$ of a category
$\operatorname{\mathscr{A}}$ is _closed (in $\operatorname{\mathscr{A}}$)
under co-retracts_ provided that, whenever $A\in\operatorname{\mathscr{D}}$
and there is a section $A\to B$ in $\operatorname{\mathscr{A}}$, also
$B\in\operatorname{\mathscr{D}}$.

######  Corollary 5.11.

Let $\sigma$ be a relational vocabulary and consider a resource-indexed
arboreal adjunction between $\mathbf{Struct}(\sigma)$ and
$\operatorname{\mathscr{C}}$ satisfying (A1)–(A4). The following hold:

  1. (1)

If $\operatorname{\mathscr{D}}$ is a full subcategory of
$\mathbf{Struct}(\sigma)$ closed under co-retracts such that each induced
comonad $G_{k}\coloneqq L_{k}R_{k}$ restricts to $\operatorname{\mathscr{D}}$,
then (HP) holds relative to $\operatorname{\mathscr{D}}$.

  2. (2)

If the counits of the comonads $G_{k}$ are componentwise surjective and $T$ is
a set of negative sentences in the vocabulary $\sigma$, then (HP) holds
relative to $\operatorname{\mathbf{Mod}}(T)$.

###### Proof.

The proof of item 1 is the same, mutatis mutandis, as for Proposition 4.21,
using Theorem 5.9 and the fact that if $\operatorname{\mathscr{D}}$ is closed
under co-retracts then $k$-extendable covers can be constructed within
$\operatorname{\mathscr{D}}$.

Item 2 is an immediate consequence of item 1. Just observe that the comonads
$G_{k}$ restrict to $\operatorname{\mathbf{Mod}}(T)$ by Lemma 4.25, and
$\operatorname{\mathbf{Mod}}(T)$ is closed under co-retracts (cf. the proof of
the aforementioned lemma). ∎

###  5.3. The equirank homomorphism preservation theorem

As observed in Section 4.1, Rossman’s equirank homomorphism preservation
theorem is equivalent to property (HP) for the Ehrenfeucht-Fraïssé resource-
indexed arboreal adjunction between $\mathbf{Struct}(\sigma)$ and
$\mathscr{R}^{E}(\sigma^{I})$. In turn, by Corollary 5.10, to establish (HP)
it suffices to show that the latter resource-indexed arboreal adjunction
satisfies (E1)–(E2) and (A1)–(A4). By Example 5.3, the category
$\mathbf{Struct}(\sigma)$ satisfies (E1)–(E2) when equipped with the
(surjective homomorphisms, embeddings) factorisation system, so it remains to
show that (A1)–(A4) hold. Before doing so, note that Corollary 5.11 yields the
following slight generalisation of the equirank homomorphism preservation
theorem (just observe that the counits of the induced comonads on
$\mathbf{Struct}(\sigma)$ are componentwise surjective).

######  Theorem 5.12.

Let $\sigma$ be a relational vocabulary and let $\operatorname{\mathscr{D}}$
be a full subcategory of $\mathbf{Struct}(\sigma)$ closed under co-retracts
such that the comonads on $\mathbf{Struct}(\sigma)$ induced by the
Ehrenfeucht-Fraïssé resource-indexed arboreal adjunction restrict to
$\operatorname{\mathscr{D}}$. Then the equirank homomorphism preservation
theorem holds relative to $\operatorname{\mathscr{D}}$.

In particular, the equirank homomorphism preservation theorem holds relative
to $\operatorname{\mathbf{Mod}}(T)$ whenever $T$ is a set of negative
sentences in the vocabulary $\sigma$.

######  Remark 5.13.

A consequence of the first part of Theorem 5.12 is that the equirank
homomorphism preservation theorem admits a relativisation to any class of
structures that is _co-homomorphism closed_ , i.e. downwards closed with
respect to the homomorphism preorder on $\mathbf{Struct}(\sigma)$, a fact
already pointed out by Rossman in [38, §7.1.2].

We proceed to verify conditions (A1)–(A4) for the adjunctions $L_{k}\dashv
R_{k}$, where

$L_{k}\coloneqq HL^{E}_{k}\ \text{ and }\ R_{k}\coloneqq R^{E}_{k}J$

with the notation of Example 3.18. Note that, since a first-order sentence
contains only finitely many relation symbols, in order to deduce the equirank
homomorphism preservation theorem, as well as Theorem 5.12 above, we can
assume without loss of generality that the relational vocabulary $\sigma$ is
finite.

(A1) Recall from Example 3.7 that, for all $k>0$, the paths in
$\mathscr{R}^{E}_{k}(\sigma^{I})$ are those forest-ordered
$\sigma^{I}$-structures $(A,\leq)$ such that the order is a chain of
cardinality at most $k$. Thus, $A$ has cardinality at most $k$. It follows at
once that there are finitely many paths in $\mathscr{R}^{E}_{k}(\sigma^{I})$
up to isomorphism, and at most one arrow between any two paths.

(A2) For any path $P=(A,\leq)$ in $\mathscr{R}^{E}_{k}(\sigma^{I})$, $L_{k}P$
is the quotient of the $\sigma$-reduct of $A$ with respect to the equivalence
relation generated by $I^{A}$. As $A$ is finite, so is $L_{k}P$. The finitely
presentable objects in $\mathbf{Struct}(\sigma)$ are precisely the finite
$\sigma$-structures (see e.g. [11, §5.1]), hence $L_{k}P$ is finitely
presentable.

(A3) Consider an arrow $m\colon P\to R_{k}B$ in
$\mathscr{R}^{E}_{k}(\sigma^{I})$, with $P=(A,\leq)$ a path and $B$ a
$\sigma$-structure. Let $B^{\prime}\coloneqq J(B)$ be the
$\sigma^{I}$-structure obtained from $B$ by interpreting $I$ as the identity
relation. Then $R_{k}B$ is obtained by equipping $\mathbb{E}_{k}(B^{\prime})$
with the prefix order. Consider the $\sigma$-homomorphism

$L_{k}m=Hm\colon H(A)\to H\mathbb{E}_{k}(B^{\prime}).$

For convenience of notation, given an element $x\in A$ we write $[x]$ for the
corresponding element of $H(A)$, and likewise for elements of
$\mathbb{E}_{k}(B^{\prime})$. Then $m^{\\#}\colon L_{k}P\to B$ is the
composite of $Hm$ with the homomorphism $H\mathbb{E}_{k}(B^{\prime})\to B$
sending the equivalence class of an element of $\mathbb{E}_{k}(B^{\prime})$ to
the last element of any of its representatives. This map is well defined
because, for any pair of sequences in $I^{\mathbb{E}_{k}(B^{\prime})}$, their
last elements coincide.

Suppose $m$ is an embedding. If $m^{\\#}([x])=m^{\\#}([y])$ then $(m(x),m(y))$
belongs to the equivalence relation generated by
$I^{\mathbb{E}_{k}(B^{\prime})}$, and so $(x,y)$ belongs to the equivalence
relation generated by $I^{A}$. It follows that $[x]=[y]$ in $H(A)$, and so
$m^{\\#}$ is injective. The same argument, mutatis mutandis, shows that
$m^{\\#}$ reflects the interpretation of the relation symbols, hence is an
embedding.

Conversely, suppose that $m^{\\#}$ is an embedding and $P$ is smooth. Consider
an embedding $n\colon P\rightarrowtail R_{k}C$ with
$C\in\mathbf{Struct}(\sigma)$. Note that the restriction of
$I^{\mathbb{E}_{k}(C^{\prime})}$ to the image of $n$ is an equivalence
relation, hence $I^{A}$ is an equivalence relation. As any forest morphism
whose domain is linearly ordered is injective, $m$ is injective. So, it
remains to show that $m$ reflects the interpretation of the relation symbols.
For all $x,y\in A$, if

$(m(x),m(y))\in I^{\mathbb{E}_{k}(B^{\prime})}$

then $m^{\\#}([x])=m^{\\#}([y])$ and so $[x]=[y]$ because $m^{\\#}$ is
injective. That is, $(x,y)\in I^{A}$, showing that $m$ reflects the
interpretation of the relation $I$. Suppose now that $S$ is a relation symbol
different from $I$. For convenience of notation we shall assume that $S$ has
arity $2$; the general case is a straightforward adaptation. For all $x,y\in
A$, if

$(m(x),m(y))\in S^{\mathbb{E}_{k}(B^{\prime})}$

then $(m^{\\#}([x]),m^{\\#}([y]))\in S^{B}$ and so $([x],[y])\in S^{H(A)}$
because $m^{\\#}$ is an embedding. That is, there are
$x^{\prime},y^{\prime}\in A$ such that $(x,x^{\prime}),(y,y^{\prime})\in
I^{A}$ and $(x^{\prime},y^{\prime})\in S^{A}$. We claim that the following
property holds, from which it follows that $m$ is an embedding:

$(x,x^{\prime}),(y,y^{\prime})\in I^{A}\ \text{ and }\
(x^{\prime},y^{\prime})\in S^{A}\ \Longrightarrow\ (x,y)\in S^{A}.$ ($\ast$)

In turn, this is a consequence of the fact that $n$ is an embedding and, in
$\mathbb{E}_{k}(C^{\prime})$,

$(n(x),n(x^{\prime})),(n(y),n(y^{\prime}))\in I^{\mathbb{E}_{k}(C^{\prime})}\
\text{ and }\ (n(x^{\prime}),n(y^{\prime}))\in S^{\mathbb{E}_{k}(C^{\prime})}$

imply $(n(x),n(y))\in S^{\mathbb{E}_{k}(C^{\prime})}$.

(A4) Finally, we show that the path restriction property is satisfied. Let
$Q=(B,\leq)$ be a smooth path in $\mathscr{R}^{E}_{k}(\sigma^{I})$, and let
$j\colon A\rightarrowtail H(B)$ be an embedding in $\mathbf{Struct}(\sigma)$.
Without loss of generality, we can identify $A$ with a substructure of $H(B)$,
and $j$ with the inclusion map. As observed above, since $Q$ is smooth,
$I^{B}$ is an equivalence relation and property ($\ast$ ‣ 5.3) is satisfied
(with $B$ in place of $A$). If $q_{B}\colon B\twoheadrightarrow H(B)$ is the
canonical quotient map, let $Q_{A}$ denote the substructure of $B$ whose
underlying set is

$\\{x\in B\mid q_{B}(x)\in A\\}.$

Then $Q_{A}$ is a path in $\mathscr{R}^{E}_{k}(\sigma^{I})$ when equipped with
the restriction of the order on $B$ and, using ($\ast$ ‣ 5.3), we get
$H(Q_{A})\cong A$.

It follows from the definition of $Q_{A}$ that item (i) in Definition 5.8 is
satisfied. Just observe that any substructure of $Q_{A}$ that is downwards
closed in $Q$ is also downwards closed in $Q_{A}$. With regards to item (ii),
consider a path embedding $!_{P,Q}\colon P\rightarrowtail Q$ with $P=(C,\leq)$
and form the following pullback square in $\mathbf{Struct}(\sigma)$.

${D}$${H(C)}$${A}$${H(B)}$${\lrcorner}$$\scriptstyle{L_{k}(!_{P,Q})}$$\scriptstyle{j}$

Identifying $H(C)$ with a substructure of $H(B)$, we can assume $D$ is the
intersection of $A$ and $H(C)$. Because $C$ is a substructure of $B$, it
follows that $Q_{D}$ is a substructure of $Q_{A}$. Moreover, because $C$ is
downwards closed in $B$, $Q_{D}$ is downwards closed in $Q_{A}$. That is,
there is an inclusion $Q_{D}\rightarrowtail Q_{A}$ whose image under $L_{k}$
coincides with the pullback of $L_{k}(!_{P,Q})$ along $j$. Hence the path
restriction property holds.

##  6\. Proof of Theorem 5.9

For the remainder of this section, we fix an arbitrary resource-indexed
arboreal adjunction between $\operatorname{\mathscr{E}}$ and
$\operatorname{\mathscr{C}}$, with adjunctions $L_{k}\dashv
R_{k}\colon\operatorname{\mathscr{E}}\to\operatorname{\mathscr{C}}_{k}$,
satisfying (E1)–(E2) and (A1)–(A4).

###  6.1. Relative extendability

For all $k>0$, we denote by $\overline{\operatorname{\mathscr{C}}}_{k}$ the
full subcategory of $\operatorname{\mathscr{C}}_{k}$ whose objects are
colimits of finite diagrams of embeddings in
$\operatorname{\mathscr{C}}_{p}^{k}$. Further, we write
$L_{k}[\overline{\operatorname{\mathscr{C}}}_{k}]$ for the full subcategory of
$\operatorname{\mathscr{E}}$ defined by the objects of the form $L_{k}c$ for
$c\in\overline{\operatorname{\mathscr{C}}}_{k}$.

######  Remark 6.1.

It follows from (A1) that $\overline{\operatorname{\mathscr{C}}}_{k}$ is
equivalent to a finite category. Therefore
$L_{k}[\overline{\operatorname{\mathscr{C}}}_{k}]$ contains, up to
isomorphism, only finitely many objects.

As we shall see in the following lemma, every path embedding $P\rightarrowtail
R_{k}a$ is homomorphically equivalent to one of the form $P\rightarrowtail
R_{k}\widetilde{a}$ with $\widetilde{a}\in
L_{k}[\overline{\operatorname{\mathscr{C}}}_{k}]$. Consequently, in the
definition of $k$-extendable object (see Definition 4.17) we can assume
without loss of generality that $e\in
L_{k}[\overline{\operatorname{\mathscr{C}}}_{k}]$. This observation, combined
with Remark 6.1, will allow us to control the size of the diagrams featuring
in the proof of Theorem 5.9.

######  Lemma 6.2.

For all path embeddings $m\colon P\rightarrowtail R_{k}a$, there are
$\widetilde{a}\in L_{k}[\overline{\operatorname{\mathscr{C}}}_{k}]$ and a path
embedding $\widetilde{m}\colon P\rightarrowtail R_{k}\widetilde{a}$ such that
$m\rightleftarrows\widetilde{m}$ in $P/{\operatorname{\mathscr{C}}_{k}}$.

###### Proof.

Fix an arbitrary path embedding $m\colon P\rightarrowtail R_{k}a$. By (A1),
there is a finite set of paths
$\mathscr{P}=\\{P_{1},\ldots,P_{j}\\}\subseteq\operatorname{\mathscr{C}}_{p}^{k}$
such that each path in $\operatorname{\mathscr{C}}_{k}$ is isomorphic to
exactly one member of $\mathscr{P}$. We can assume without loss of generality
that $P\in\mathscr{P}$.

For each path embedding $p\in\operatorname{\mathbb{P}}{(R_{k}a)}$, denote by
$T_{p}$ the tree obtained by first considering the tree
${\uparrow}p\subseteq\operatorname{\mathbb{P}}{(R_{k}a)}$ and then replacing
each node $q$ (which is an isomorphism class of a path embedding) with the
unique path $P_{i}\in\mathscr{P}$ such that $P_{i}\cong\operatorname{dom}(q)$.
We assume that $T_{p}$ is _reduced_ , i.e. given any two nodes $x$ and $y$ of
$T_{p}$ that cover the same node, if the trees ${\uparrow}x$ and ${\uparrow}y$
are equal then $x=y$. (If $T_{p}$ is not reduced, we can remove branches in
the obvious manner to obtain a maximal reduced subtree $T^{\prime}_{p}$.) We
refer to $T_{p}$ as the _type_ of $p$; note that this is a finite tree. In
particular, if $\bot$ is the root of $\operatorname{\mathbb{P}}{(R_{k}a)}$, we
get a finite tree $T_{\bot}$.

Now, for each node $x$ of $T_{\bot}$, we shall define a path embedding $m_{x}$
into $R_{k}a$ whose domain belongs to $\mathscr{P}$. The definition of $m_{x}$
is by induction on the height of $x$. Suppose $x$ has height $0$, i.e. $x$ is
the root of $T_{\bot}$. Then $x=P_{i}$ for a unique $i\in\\{1,\ldots,j\\}$.
Define $m_{x}$ as the restriction of $m$ to $P_{i}$, i.e. the composition of
$m\colon P\rightarrowtail R_{k}a$ with the unique embedding
$P_{i}\rightarrowtail P$. Next, suppose $m_{z}$ has been defined for all nodes
$z$ of height at most $l$, and let $x$ be a node of height $l+1$ labeled by
some $P_{j}$. We distinguish two cases:

  * •

If there is a node $y\geq x$ such that $T_{m}$ coincides with the tree
${\uparrow}y\subseteq T_{\bot}$, then we let $m_{x}$ be the restriction of $m$
to $P_{j}$. Note that, in this case, the type of $m_{x}$ coincides with the
tree ${\uparrow}x\subseteq T_{\bot}$. Moreover, if $z$ is the predecessor of
$x$ then $m_{z}$ will also be an appropriate restriction of $m$, and thus
$m_{x}$ extends $m_{z}$.

  * •

Otherwise, we let $m_{x}\colon P_{j}\rightarrowtail R_{k}a$ be any path
embedding such that:

    1. (i)

The type of $m_{x}$ coincides with the tree ${\uparrow}x\subseteq T_{\bot}$.

    2. (ii)

$m_{x}$ extends $m_{z}$, where $z$ is the predecessor of $x$.

Note that such an embedding $m_{x}$ exists because $x\in{\uparrow}z\subseteq
T_{\bot}$ and, by inductive hypothesis, ${\uparrow}z$ coincides with the type
of $m_{z}$.

The set

$V\coloneqq\\{m_{x}\mid x\in T_{\bot}\\}$

is finite and contains $m$. We regard $V$ as a cocone over a finite diagram
$D$ of paths and embeddings between them. Let $\widetilde{a}\coloneqq
L_{k}(\operatornamewithlimits{colim}D)$ and note that $\widetilde{a}\in
L_{k}[\overline{\operatorname{\mathscr{C}}}_{k}]$. The functor $L_{k}$
preserves colimits because it is left adjoint, hence $\widetilde{a}$ is the
colimit in $\operatorname{\mathscr{E}}$ of the diagram $L_{k}D$. The cocone
$\\{n^{\\#}\mid n\in V\\}$ with vertex $a$ over $L_{k}D$ then factors through
a unique morphism $f\colon\widetilde{a}\to a$. By construction, $m\colon
P\rightarrowtail R_{k}a$ factors through $R_{k}f$, and so there is
$\widetilde{m}\colon P\rightarrowtail\widetilde{a}$ such that
$m=R_{k}f\circ\widetilde{m}$. Hence, $\widetilde{m}\to m$.

Next, with the aim of showing that $m\to\widetilde{m}$, we shall define a
morphism ${R_{k}a\to R_{k}\widetilde{a}}$. As $R_{k}a$ is path generated, it
suffices to define a cocone

$W=\\{\varphi_{p}\mid p\in\operatorname{\mathbb{P}}{(R_{k}a)}\\}$

with vertex $R_{k}\widetilde{a}$ over the diagram of path embeddings into
$R_{k}a$. Suppose $p\in\operatorname{\mathbb{P}}{(R_{k}a)}$. We define the
corresponding arrow $\varphi_{p}$ by induction on the height of $p$:

  1. (i)

If $p$ is the root of $\operatorname{\mathbb{P}}{(R_{k}a)}$, then it factors
through $R_{k}f\colon R_{k}\widetilde{a}\rightarrowtail R_{k}a$, and so it
yields an embedding $\varphi_{p}\colon\operatorname{dom}(p)\rightarrowtail
R_{k}\widetilde{a}$.

  2. (ii)

Suppose that $p$ has height $l+1$ and $\varphi_{q}$ has been defined whenever
$q$ has height at most $l$. We distinguish two cases: if $p$ factors through
$R_{k}f\colon R_{k}\widetilde{a}\rightarrowtail R_{k}a$, i.e. $p=R_{k}f\circ
s_{p}$ for some embedding $s_{p}$, then we set $\varphi_{p}\coloneqq s_{p}$.
This is the case, in particular, when $p\leq m$ in
$\operatorname{\mathbb{P}}{(R_{k}a)}$. Clearly, if $p$ extends $q$ then
$\varphi_{p}$ extends $\varphi_{q}$.

Otherwise, let $q$ be such that $p\succ q$. By inductive hypothesis, we can
suppose that $R_{k}f\circ\varphi_{q}$ coincides with an embedding $m_{x}\colon
P_{j}\rightarrowtail R_{k}a$ in $V$ (up to an isomorphism
$\operatorname{dom}(q)\cong P_{j}$) whose type coincides with the tree
${\uparrow}x\subseteq T_{\bot}$. As $q$ corresponds to a node $y$ covering $x$
labeled by some $P_{h}\cong\operatorname{dom}(p)$, by definition of $V$ there
is an embedding $m_{y}\colon P_{h}\rightarrowtail R_{k}a$ in $V$ such that
$m_{y}$ extends $m_{x}$, and the type $m_{y}$ coincides with ${\uparrow}y$.
Since $m_{y}$ factors through $R_{k}f$, precomposing with the isomorphism
$\operatorname{dom}(p)\cong P_{h}$ we get an embedding
$\varphi_{p}\colon\operatorname{dom}(p)\rightarrowtail R_{k}\widetilde{a}$.
Observe that $\varphi_{p}$ extends $\varphi_{q}$.

The compatibility condition for the cocone $W$ states that $\varphi_{p}$
extends $\varphi_{q}$ whenever $p$ extends $q$, which is ensured by the
definition above. Thus, $W$ induces a morphism $g\colon R_{k}a\to
R_{k}\widetilde{a}$ and, by construction, $g\circ m=\widetilde{m}$. Hence,
$m\to\widetilde{m}$. ∎

The construction of $k$-extendable covers is akin to that of
$\omega$-saturated elementary extensions in model theory, where one starts
with a first-order structure $M$ and constructs an elementary extension
$M_{1}$ of $M$ in which all types over (finite subsets of) $M$ are realised,
then an elementary extension $M_{2}$ of $M_{1}$ in which all types over
$M_{1}$ are realised, and so forth. The union of the induced elementary chain
of models yields the desired $\omega$-saturated elementary extension of $M$.

In the same spirit, we introduce a notion of $k$-extendability relative to a
homomorphism, which models the one-step construction just outlined.

######  Definition 6.3.

Let $h\colon a\to b$ be an arrow in $\operatorname{\mathscr{E}}$. We say that
$b$ is _$k$ -extendable relative to $h$_ if the following property is
satisfied for all $e\in L_{k}[\overline{\operatorname{\mathscr{C}}}_{k}]$: For
all path embeddings $m\colon P\rightarrowtail R_{k}a$ and $n\colon
P\rightarrowtail R_{k}e$ such that $m_{\star}\rightleftarrows n_{\star}$,

${P}$${\mathscr{S}_{m}}$${\mathscr{S}_{n}}$$\scriptstyle{m_{\star}}$$\scriptstyle{n_{\star}}$

if $n^{\prime}\colon Q\rightarrowtail R_{k}e$ is a path embedding such that
$n\leq n^{\prime}$ in $\operatorname{\mathbb{P}}{(R_{k}e)}$, there is a path
embedding $m^{\prime}\colon Q\rightarrowtail R_{k}b$ such that the leftmost
diagram below commutes and $m^{\prime}_{\star}\rightleftarrows
n^{\prime}_{\star}$.

${P}$${Q}$${R_{k}a}$${R_{k}b}$$\scriptstyle{!}$$\scriptstyle{m}$$\scriptstyle{m^{\prime}}$$\scriptstyle{R_{k}h}$${Q}$${\mathscr{S}_{m^{\prime}}}$${\mathscr{S}_{n^{\prime}}}$$\scriptstyle{m^{\prime}_{\star}}$$\scriptstyle{n^{\prime}_{\star}}$

Suppose that, given an object $a\in\operatorname{\mathscr{E}}$, we are able to
construct a section $s\colon a\to b$ such that $b$ is $k$-extendable relative
to $s$. Iterating this process countably many times, we obtain a
$k$-extendable cover $a\to a^{*}$, thus settling Theorem 5.9. The main hurdle
consists in establishing the following proposition; a proof is offered in
Section 6.2.

######  Proposition 6.4.

For all $a\in\operatorname{\mathscr{E}}$ and all $k>0$ there is a section
$s\colon a\to b$ such that $b$ is $k$-extendable relative to $s$.

We can finally prove Theorem 5.9:

###### Proof of Theorem 5.9.

Let $a\in\operatorname{\mathscr{E}}$. By applying Proposition 6.4 repeatedly,
we obtain a chain of sections

${a}$${b_{1}}$${b_{2}}$${b_{3}}$${\cdots}$$\scriptstyle{s_{1}}$$\scriptstyle{s_{2}}$$\scriptstyle{s_{3}}$$\scriptstyle{s_{4}}$

such that $b_{i}$ is $k$-extendable relative to $s_{i}$, for all $i\geq 1$.
Denote the previous diagram by $D$ and let $a^{*}$ be the colimit of $D$ in
$\operatorname{\mathscr{E}}$, which exists by (E1). Let $h_{i}\colon b_{i}\to
a^{*}$ be the colimit map with domain $b_{i}$, and $s\colon a\to a^{*}$ the
one with domain $a$. As all the arrows in $D$ are sections, so are the colimit
maps; in particular, $s$ is a section.

We claim that $a^{*}$ is $k$-extendable. Suppose $m\colon P\rightarrowtail
R_{k}(a^{*})$ and $n\colon P\rightarrowtail R_{k}e$ are path embeddings such
that $m_{\star}\rightleftarrows n_{\star}$. By Lemma 6.2, we can assume
without loss of generality that $e\in
L_{k}[\overline{\operatorname{\mathscr{C}}}_{k}]$.

By (A2), $L_{k}P$ is finitely presentable in $\operatorname{\mathscr{E}}$ and
so $m^{\\#}\colon L_{k}P\to a^{*}$ factors through one of the colimit maps.
Assume without loss of generality that $m^{\\#}$ factors through $h_{j}\colon
b_{j}\to a$ for some $j\,{\geq}\,1$, so there is an arrow $r\colon L_{k}P\to
b_{j}$ satisfying $m^{\\#}=h_{j}\circ r$. If $m_{j}\coloneqq r^{\flat}$, it
follows that $m=R_{k}h_{j}\circ m_{j}$. In particular, $m_{j}$ is an embedding
because so is $m$. Since $R_{k}h_{j}$ is a section, Remark 4.13 entails
$m_{j}\rightleftarrows m$, and so $(m_{j})_{\star}\rightleftarrows m_{\star}$
by Lemma 4.15(c). Because $m_{\star}\rightleftarrows n_{\star}$, also
$(m_{j})_{\star}\rightleftarrows n_{\star}$.

Now, let $n^{\prime}\colon Q\rightarrowtail R_{k}e$ be any path embedding such
that $n\leq n^{\prime}$ in $\operatorname{\mathbb{P}}{(R_{k}e)}$. Since
$b_{j+1}$ is $k$-extendable relative to $s_{j+1}$, there is a path embedding
$m^{\prime}\colon Q\rightarrowtail R_{k}b_{j+1}$ such that
$m^{\prime}_{\star}\rightleftarrows n^{\prime}_{\star}$ and the following
diagram commutes.

${P}$${Q}$${R_{k}b_{j}}$${R_{k}b_{j+1}}$$\scriptstyle{!}$$\scriptstyle{m_{j}}$$\scriptstyle{m^{\prime}}$$\scriptstyle{R_{k}s_{j+1}}$

It follows that

$m=R_{k}h_{j}\circ m_{j}=R_{k}h_{j+1}\circ R_{k}s_{j+1}\circ
m_{j}=R_{k}h_{j+1}\circ m^{\prime}\circ{!}$

and so $m^{\prime\prime}\coloneqq R_{k}h_{j+1}\circ m^{\prime}\colon
Q\rightarrowtail R_{k}(a^{*})$ satisfies $m\leq m^{\prime\prime}$ in
$\operatorname{\mathbb{P}}{(R_{k}(a^{*}))}$. Again by Remark 4.13 and Lemma
4.15(c) we get $m^{\prime\prime}_{\star}\rightleftarrows m^{\prime}_{\star}$,
and thus $m^{\prime\prime}_{\star}\rightleftarrows n^{\prime}_{\star}$. This
shows that $a^{*}$ is $k$-extendable. ∎

###  6.2. Proof of Proposition 6.4

Fix an object $a$ of $\operatorname{\mathscr{E}}$ and a positive integer $k$.
To improve readability, we drop the subscript from $L_{k}$ and $R_{k}$, and
simply write $L$ and $R$ (but continue to denote by
$\operatorname{\mathscr{C}}_{k}$ the arboreal category). We must find a
section $s\colon a\to b$ such that $b$ is $k$-extendable relative to $s$.
Consider all pairs of path embeddings

$(u\colon P\rightarrowtail Ra,v\colon P\rightarrowtail Re)$

in $\operatorname{\mathscr{C}}_{k}$ such that $e\in
L[\overline{\operatorname{\mathscr{C}}}_{k}]$ and $Lv_{\star}\to u^{\\#}$ in
$LP/{\operatorname{\mathscr{E}}}$.

######  Remark 6.5.

Note that $Lv_{\star}\to u^{\\#}$ entails that $Lv_{\star}$ is an embedding.
Just observe that $u^{\\#}$ is an embedding by the first part of (A3).

Each such pair $(u,v)$ induces a pushout square in
$\operatorname{\mathscr{E}}$ as follows.

${LP}$${L\mathscr{S}_{v}}$${a}$${a+_{LP}L\mathscr{S}_{v}}$$\scriptstyle{u^{\\#}}$$\scriptstyle{Lv_{\star}}$$\scriptstyle{\lambda_{(u,v)}}$$\scriptstyle{\iota_{(u,v)}}$${\ulcorner}$

This pushout square exists by (E1) and consists entirely of embeddings by
virtue of (E2).

######  Lemma 6.6.

$\iota_{(u,v)}$ is a section.

###### Proof.

Just observe that, since $Lv_{\star}\to u^{\\#}$, there is $g\colon
L\mathscr{S}_{v}\to a$ such that ${g\circ Lv_{\star}=u^{\\#}}$. By the
universal property of the pushout, there is an arrow $h\colon
a+_{LP}L\mathscr{S}_{v}\to a$ such that $h\circ\iota_{(u,v)}$ is the identity
of $a$. ∎

We let $D$ be the diagram in $\operatorname{\mathscr{E}}$ consisting of all
the morphisms

$\iota_{(u,v)}\colon a\to a+_{LP}L\mathscr{S}_{v}$

as above. Because $\operatorname{\mathscr{C}}_{k}$ is locally finite and $e$
varies among the objects of $L[\overline{\operatorname{\mathscr{C}}}_{k}]$,
choosing representatives for isomorphism classes in an appropriate way we can
assume by Remark 6.1 that $D$ is a small diagram.

By (E1), $D$ admits a colimit $b\coloneqq\operatornamewithlimits{colim}D$. In
other words, $b$ is obtained as a _wide pushout_ in
$\operatorname{\mathscr{E}}$. Denote by $s\colon a\to b$ the colimit map with
domain $a$, and by

$t_{(u,v)}\colon a+_{LP}L\mathscr{S}_{v}\to b$

the colimit map corresponding to the arrow $\iota_{(u,v)}$. As all arrows in
$D$ are sections by Lemma 6.6, so are the colimit maps. In particular,
$s\colon a\to b$ is a section.

We claim that $b$ is $k$-extendable relative to $s$, thus settling Proposition
6.4. Assume we are given path embeddings $m\colon P\rightarrowtail Ra$ and
$n\colon P\rightarrowtail Re$, with $e\in
L[\overline{\operatorname{\mathscr{C}}}_{k}]$, such that
$m_{\star}\rightleftarrows n_{\star}$ as displayed in the leftmost diagram
below.

${P}$${\mathscr{S}_{m}}$${\mathscr{S}_{n}}$$\scriptstyle{m_{\star}}$$\scriptstyle{n_{\star}}$$\scriptstyle{f}$$\scriptstyle{g}$
${LP}$${a}$${L\mathscr{S}_{n}}$$\scriptstyle{m^{\\#}}$$\scriptstyle{Ln_{\star}}$$\scriptstyle{\mathfrak{i}_{m}^{\\#}\circ
Lg}$

If $\mathfrak{i}_{m}\colon\mathscr{S}_{m}\rightarrowtail Ra$ is the canonical
embedding, we get a commutative triangle as on the right-hand side above. Just
observe that

$\mathfrak{i}_{m}^{\\#}\circ Lg\circ Ln_{\star}=\mathfrak{i}_{m}^{\\#}\circ
Lm_{\star}=(\mathfrak{i}_{m}\circ m_{\star})^{\\#}=m^{\\#}.$

Hence $Ln_{\star}\to m^{\\#}$. Let

$\iota_{(m,n)}\colon a\to a+_{LP}L\mathscr{S}_{n}$

be the corresponding arrow in the diagram $D$. To improve readability we shall
write, respectively, $\iota$, $\lambda$ and $t$ instead of $\iota_{(m,n)}$,
$\lambda_{(m,n)}$ and $t_{(m,n)}$.

Let $n^{\prime}\colon Q\rightarrowtail Re$ be a path embedding with $n\leq
n^{\prime}$ in $\operatorname{\mathbb{P}}{(Re)}$. We must exhibit a path
embedding $m^{\prime}\colon Q\rightarrowtail Rb$ such that the leftmost square
below commutes and $m^{\prime}_{\star}\rightleftarrows n^{\prime}_{\star}$.

${P}$${Q}$${Ra}$${Rb}$$\scriptstyle{!}$$\scriptstyle{m}$$\scriptstyle{m^{\prime}}$$\scriptstyle{Rs}$
${Q}$${\mathscr{S}_{m^{\prime}}}$${\mathscr{S}_{n^{\prime}}}$$\scriptstyle{m^{\prime}_{\star}}$$\scriptstyle{n^{\prime}_{\star}}$
(2)

Note that, because $n\leq n^{\prime}$, we get
$\mathscr{S}_{n^{\prime}}\leq\mathscr{S}_{n}$ in
$\operatorname{\mathbb{S}}{Re}$. Thus, $n^{\prime}_{\star}$ can be identified
with a path embedding into $\mathscr{S}_{n}$. Consider the arrow

$\xi\coloneqq(\lambda\circ Ln^{\prime}_{\star})^{\flat}\colon Q\to
R(a+_{LP}L\mathscr{S}_{n}).$

######  Lemma 6.7.

$\xi$ is an embedding.

###### Proof.

By the first part of (A3), $(n^{\prime})^{\\#}$ is an embedding. Then
$Ln^{\prime}$ is an embedding since $(n^{\prime})^{\\#}=\varepsilon_{e}\circ
Ln^{\prime}$, and so is $Ln^{\prime}_{\star}$. It follows that $\lambda\circ
Ln^{\prime}_{\star}$ is an embedding because it is a composition of
embeddings, and $\xi$ is an embedding by the second part of (A3). ∎

Lemma 6.7, combined with the fact that $Rt$ is a section (hence an embedding),
entails that the composite $m^{\prime}\coloneqq Rt\circ\xi\colon
Q\rightarrowtail Rb$ is an embedding. Moreover

$\displaystyle m^{\prime}\circ{!}$
$\displaystyle=((m^{\prime}\circ{!})^{\\#})^{\flat}=((m^{\prime})^{\\#}\circ
L{!})^{\flat}=(t\circ\lambda\circ Ln^{\prime}_{\star}\circ L{!})^{\flat}$
$\displaystyle=(t\circ\lambda\circ Ln_{\star})^{\flat}=(t\circ\iota\circ
m^{\\#})^{\flat}=(s\circ m^{\\#})^{\flat}=Rs\circ m,$

showing that the leftmost diagram in equation (2) commutes. Since $Rt$ is a
section, we have $\xi\rightleftarrows m^{\prime}$ by Remark 4.13, and so
$\xi_{\star}\rightleftarrows m^{\prime}_{\star}$ by Lemma 4.15(c). Therefore,
in order to show that $m^{\prime}_{\star}\rightleftarrows n^{\prime}_{\star}$
it suffices to prove that $\xi_{\star}\rightleftarrows n^{\prime}_{\star}$. We
have

$\lambda^{\flat}\circ n^{\prime}_{\star}=((\lambda^{\flat}\circ
n^{\prime}_{\star})^{\\#})^{\flat}=(\lambda\circ
Ln^{\prime}_{\star})^{\flat}=\xi$

and thus $n^{\prime}_{\star}\to\xi$. It follows from Remark 4.16 that
$n^{\prime}_{\star}\to\xi_{\star}$.

It remains to show that $\xi_{\star}\to n^{\prime}_{\star}$; the proof of this
fact will occupy us for the rest of this section. As
$\operatorname{\mathscr{C}}_{k}$ is an arboreal category, $\mathscr{S}_{\xi}$
is the colimit of its path embeddings. Thus, in order to define a morphism
$\mathscr{S}_{\xi}\to\mathscr{S}_{n^{\prime}}$ it suffices to define a
compatible cocone with vertex $\mathscr{S}_{n^{\prime}}$ over the diagram of
path embeddings into $\mathscr{S}_{\xi}$. By Lemma 4.15(a), the path
embeddings into $\mathscr{S}_{\xi}$ can be identified with the path embeddings
into $R(a+_{LP}L\mathscr{S}_{n})$ that are comparable with $\xi$. For each
such path embedding $q\colon Q^{\prime}\rightarrowtail
R(a+_{LP}L\mathscr{S}_{n})$, we shall define an arrow $\zeta_{q}\colon
Q^{\prime}\to Re$ and prove that these form a compatible cocone. We will then
deduce, using the induced mediating morphism $\mathscr{S}_{\xi}\to Re$, that
$\xi_{\star}\to n^{\prime}_{\star}$.

Fix an arbitrary path embedding $q\colon Q^{\prime}\rightarrowtail
R(a+_{LP}L\mathscr{S}_{n})$ above $\xi$ and consider the following diagram in
$\operatorname{\mathscr{E}}$, where the four vertical faces are pullbacks.

${\overline{LP}}$${\overline{L\mathscr{S}_{n}}}$${\overline{a}}$${LQ^{\prime}}$${LP}$${L\mathscr{S}_{n}}$${a}$${a+_{LP}L\mathscr{S}_{n}}$$\scriptstyle{\nu}$$\scriptstyle{\mu_{1}}$$\scriptstyle{\mu_{2}}$$\scriptstyle{\tau_{2}}$$\scriptstyle{\tau_{1}}$$\scriptstyle{\sigma_{1}}$$\scriptstyle{Ln_{\star}}$$\scriptstyle{m^{\\#}}$$\scriptstyle{\lambda}$$\scriptstyle{\iota}$$\scriptstyle{\sigma_{2}}$$\scriptstyle{q^{\\#}}$
(3)

Note that the previous diagram consists entirely of embeddings because
$q^{\\#}$ is an embedding by the first part of (A3), and the pullback in
$\operatorname{\mathscr{E}}$ of an embedding exists by (E1) and is again an
embedding.

Because $q$ is above $\xi$, there is an embedding $Q\rightarrowtail
Q^{\prime}$, and thus also an embedding $P\rightarrowtail Q^{\prime}$. By the
universal property of pullbacks, there are unique arrows

$\vartheta\colon LP\rightarrowtail\overline{a}\ \ \text{ and }\ \ \Delta\colon
LP\rightarrowtail\overline{LP}$

making the following diagrams commute.

${LP}$${\overline{a}}$${LQ^{\prime}}$${a}$${{a+_{LP}L\mathscr{S}_{n}}}$$\scriptstyle{L!}$$\scriptstyle{m^{\\#}}$$\scriptstyle{\vartheta}$${\lrcorner}$$\scriptstyle{\sigma_{1}}$$\scriptstyle{\sigma_{2}}$$\scriptstyle{q^{\\#}}$$\scriptstyle{\iota}$
${LP}$${\overline{LP}}$${\overline{a}}$${LP}$${a}$$\scriptstyle{\vartheta}$$\scriptstyle{\mathrm{id}_{LP}}$$\scriptstyle{\Delta}$${\lrcorner}$$\scriptstyle{\mu_{1}}$$\scriptstyle{\mu_{2}}$$\scriptstyle{\sigma_{2}}$$\scriptstyle{m^{\\#}}$

Note in particular that $\mu_{2}$ is a retraction whose right inverse is
$\Delta$. As $\mu_{2}$ is also an embedding, it must be an isomorphism with
(two-sided) inverse $\Delta$.

By (A4) (more precisely, by item (i) in Definition 5.8) there is an arrow
$w\colon P\to Q_{\overline{a}}$ between paths such that $Lw=\vartheta$. Hence,
we can consider $\sigma_{2}^{\flat}\colon Q_{\overline{a}}\to Ra$. Note that

$(\sigma_{2}^{\flat}\circ w)^{\\#}=\sigma_{2}\circ
Lw=\sigma_{2}\circ\vartheta=m^{\\#},$

and so $\sigma_{2}^{\flat}\circ w=m$. In particular, $w$ is an embedding. As
$Q_{\overline{a}}$ is a path,
$\mathfrak{i}_{w}\colon\mathscr{S}_{w}\rightarrowtail Q_{\overline{a}}$ can be
identified with the identity $Q_{\overline{a}}\to Q_{\overline{a}}$. By Lemma
4.15(b), there is a unique arrow $\psi_{q}\colon
Q_{\overline{a}}\to\mathscr{S}_{m}$ making the following diagram commute.

${Q_{\overline{a}}}$${\mathscr{S}_{m}}$${Ra}$$\scriptstyle{\psi_{q}}$$\scriptstyle{\sigma_{2}^{\flat}}$$\scriptstyle{\mathfrak{i}_{m}}$

######  Lemma 6.8.

The following diagram commutes.

${\overline{LP}}$${\overline{a}}$${L\mathscr{S}_{n}}$$\scriptstyle{\mu_{1}}$$\scriptstyle{Ln_{\star}\circ\mu_{2}}$$\scriptstyle{L(f\circ\psi_{q})}$

###### Proof.

Note that

$\mathfrak{i}_{m}\circ\psi_{q}\circ w=\sigma_{2}^{\flat}\circ
w=m=\mathfrak{i}_{m}\circ m_{\star}$

and so $\psi_{q}\circ w=m_{\star}$ since $\mathfrak{i}_{m}$ is a monomorphism.
Applying the functor $L$ to the outer commutative diagram on the left-hand
side below, we obtain the commutative diagram on the right-hand side.