width $<n$_ in the sense of (Robertson and Seymour, 1986; Feder and Vardi,
1998); cf. (Abramsky et al., 2017) or (Abramsky and Shah, 2021, Theorem 6.4).
The least width of a tree decomposition of $A$ is called the _tree-width_ of
$A$, a combinatorial parameter that plays an important role in finite model
theory. Thus, $\mathbb{P}_{n}$-coalgebra structures on $A$ witness the fact
that the tree-width of $A$ is $<n$:

###### Proposition 6.11.

For the pebbling comonads $\mathbb{P}_{n}$, the coalgebra number of a
structure $A\in\mathbf{Struct}(\sigma)$ coincides with the tree-depth of $A$
increased by $1$.888The definition of width of a tree decomposition
customarily involves subtracting $1$, so that trees have tree-width $1$; this
is why there is a difference of $1$ between coalgebra numbers and tree-width.

###  6.2. Homomorphism counting results _à la_ Lovász

A well-known consequence of the _Yoneda Lemma_ states that any two objects
$X,Y$ of an (essentially small) category $\operatorname{\mathscr{C}}$ are
isomorphic if, and only if, the corresponding hom-functors are _naturally
isomorphic_ ; in symbols,

$X\cong Y\ \Longleftrightarrow\ \hom(-,X)\cong\hom(-,Y).$

In 1967, Lovász showed that the naturality condition can be omitted when
$\operatorname{\mathscr{C}}$ is the category of finite $\sigma$-structures,
for any finite relational signature $\sigma$ (Lovász, 1967). That is, finite
$\sigma$-structures $A,B$ are isomorphic precisely when they admit the same
(finite) number of homomorphisms from any other finite $\sigma$-structure:

$A\cong B\ \Longleftrightarrow\ \text{for all finite $\sigma$-structures $C$,
}\hom(C,A)\cong\hom(C,B).$

###### Remark 6.12.

Two pointwise isomorphic functors (as in Lovász’ theorem) need not be
naturally isomorphic, as the next example from (Joyal, 1981) shows. For any
finite set $X$, let $K_{1}(X)$ and $K_{2}(X)$ be, respectively, the set of
permutations of $X$ and the set of linear orders on $X$. The assignments
$X\mapsto K_{1}(X)$ and $X\mapsto K_{2}(X)$ can be extended to endofunctors
$K_{1}$ and $K_{2}$, respectively, on the category of finite sets and
bijections between them. The functors $K_{1}$ and $K_{2}$ are pointwise
isomorphic because the number of permutations of a finite set $X$ is $|X|!$,
which is also the number of linear orders on $X$. However, they are not
naturally isomorphic; just note that there is no natural way of assigning a
linear order to the identity permutation.

Homomorphism counting results, akin to Lovász’ seminal result, have been
investigated also in finite model theory. There, one is interested in
equivalence relations between structures that can be captured in terms of
homomorphism counts from a restricted class of structures. Prime examples are
Dvořák’s and Grohe’s homomorphism counting results:

###### Theorem 6.13 ((Dvořák, 2010)).

Let $\operatorname{\mathscr{C}}$ be the category of finite undirected graphs
without loops and graph homomorphisms, and let
$\mathcal{K}\subseteq\operatorname{\mathscr{C}}$ consist of those graphs
having tree-width $<n$. For any $A,B\in\operatorname{\mathscr{C}}$ we have

$A\equiv_{\mathrm{FO}^{n}(\\#)}B\ \Longleftrightarrow\ \text{for all
$C\in\mathcal{K}$, }\hom(C,A)\cong\hom(C,B).$

###### Theorem 6.14 ((Grohe, 2020)).

Let $\operatorname{\mathscr{C}}$ be the category of finite undirected vertex-
coloured graphs and graph homomorphisms preserving the colours, and let
$\mathcal{K}\subseteq\operatorname{\mathscr{C}}$ consist of those graphs
having tree-depth $\leq k$. For any $A,B\in\operatorname{\mathscr{C}}$ we have

$A\equiv_{\mathrm{FO}_{k}(\\#)}B\ \Longleftrightarrow\ \text{for all
$C\in\mathcal{K}$, }\hom(C,A)\cong\hom(C,B).$

The three homomorphism counting results above find a natural common
generalisation in the setting of game comonads. Recall from Theorem 5.6 that
equivalence in the counting logics is captured by the isomorphism relation in
the Kleisli categories, or equivalently in the Eilenberg–Moore categories
(since the former fully embed into the latter). In turn, by Propositions 6.9
and 6.11, the structures having tree-width $<n$ or tree-depth $\leq k$ are
precisely those admitting, respectively, a coalgebra structure for
$\mathbb{P}_{n}$ or $\mathbb{E}_{k}$. This suggests the following notion:

###### Definition 6.15.

Let $\operatorname{\mathscr{C}}$ be a locally finite category (that is, there
are finitely many arrows between any two objects of
$\operatorname{\mathscr{C}}$). We say that $\operatorname{\mathscr{C}}$ is
_combinatorial_ if, for all $A,B\in\operatorname{\mathscr{C}}$,

$A\cong B\ \Longleftrightarrow\ \text{for all
$C\in\operatorname{\mathscr{C}}$, }\hom(C,A)\cong\hom(C,B).$

For example, Lovász’ theorem states that the category of finite
$\sigma$-structures is combinatorial. In fact, any locally finite category
with pushouts and a proper factorisation system is combinatorial; see (Dawar
et al., 2021) and also (Pultr, 1973; Isbell, 1991). (The assumption that all
pushouts exist is not necessary and can be weakened, see (Dawar et al., 2021,
Remark 13) and (Reggio, 2022, Theorem 4.3).) This leads to the following
result:

###### Theorem 6.16 ((Dawar et al., 2021)).

Let $\mathbb{G}$ be a comonad on $\mathbf{Struct}(\sigma)$. The full
subcategory of $\mathbf{EM}(\mathbb{G})$ consisting of the finite coalgebras
is combinatorial.999A coalgebra for $\mathbb{G}$ is _finite_ if its underlying
$\sigma$-structure is finite.

If we let $\mathbb{G}$ in Theorem 6.16 be the identity comonad, we obtain
exactly Lovász’ theorem. When $\mathbb{G}=\mathbb{E}_{k}^{I}$, in view of
Remark 5.2 and Theorem 5.6 we get that any two finite $\sigma$-structures $A$
and $B$ are $\mathrm{FO}_{k}(\\#)$-equivalent if, and only if, $J(A)$ and
$J(B)$ cannot be distinguished by the number of homomorphisms from any finite
$\sigma^{I}$-structure of tree-depth $\leq k$. One then shows that the functor
$H\colon\mathbf{Struct}(\sigma^{I})\to\mathbf{Struct}(\sigma)$, left adjoint
to $J$, does not increase the tree-depth of structures, and so $A$ and $B$ are
$\mathrm{FO}_{k}(\\#)$-equivalent if, and only if, they cannot be
distinguished by the number of homomorphisms from any finite
$\sigma$-structure of tree-depth $\leq k$.

A similar analysis can be carried out for the pebbling comonad
$\mathbb{P}_{n}^{I}$, and thus we obtain variants of Dvořák’s and Grohe’s
theorems for arbitrary structures.101010The case of the pebbling comonad is
less straightforward because, unlike for the Ehrenfeucht–Fraïssé comonad, co-
free coalgebras for the pebbling comonad are never finite. To overcome this
hurdle, one can either “stratify” the pebbling comonad into finitary levels or
apply a more direct topological argument; see (Dawar et al., 2021, §IV.B) and
(Reggio, 2022, §6.3), respectively. The aforementioned results, in their
original form, can be recovered simply by observing that the comonads restrict
to the appropriate categories of graphs; cf. (Dawar et al., 2021).

The analysis outlined above, and in particular the observation that the
functor $H$ preserves the relevant combinatorial parameters of structures, has
the following logical consequences concerning equality elimination:

###### Corollary 6.17 ((Dawar et al., 2021)).

Let $\mathcal{L}$ be either $\mathrm{FO}_{k}(\\#)$ or $\mathrm{FO}^{n}(\\#)$.
The following statements hold:

  1. (1)

If two finite $\sigma$-structures are not distinguished by any sentence of
$\mathcal{L}$ without equality, then they are not distinguished by any
sentence of $\mathcal{L}$.

  2. (2)

Let $\mathcal{L}_{\infty}$ be the closure of $\mathcal{L}$ under infinitary
conjunctions and disjunctions. Each sentence of $\mathcal{L}_{\infty}$ is
equivalent, over finite $\sigma$-structures, to one without equality.

Finally, let us mention that applying (the obvious variant for pointed
structures of) Theorem 6.16 to the modal comonad, one obtains at once a
homomorphism counting result for graded modal logic that characterises
$\mathrm{ML}_{k}(\\#)$-equivalence of finite pointed Kripke models in terms of
homomorphism counts from finite synchronization trees of height $\leq k$
(Dawar et al., 2021, Theorem 31).

##  7\. Paths, open maps, and more logical equivalences

In §5 we saw that the homomorphism preorder and the isomorphism relation in
the Kleisli categories for game comonads capture, respectively, preservation
of existential positive fragments $\exists^{+}\mathcal{L}$ and equivalence (of
finite structures) in fragments with counting quantifiers $\mathcal{L}(\\#)$.
Note that, since the Kleisli category $\mathbf{Kl}(\mathbb{G})$ of a comonad
$\mathbb{G}$ is a full subcategory of the Eilenberg–Moore category
$\mathbf{EM}(\mathbb{G})$, these results could equivalently be phrased in the
latter category.

In this section, we show how other relations between coalgebras for game
comonads, which are _not_ definable in the Kleisli category, allow us to
encode equivalence in the _full fragments_ $\mathcal{L}$ as well as
preservation of the _existential fragments_ $\exists\mathcal{L}$ and _positive
fragments_ ${}^{+}\mathcal{L}$. These results crucially rely on the notion of
_path_. We give a concrete definition of path using the characterisation of
Eilenberg–Moore categories of game comonads in §6; an axiomatic definition of
path will be given in §8.

###### Definition 7.1.

A coalgebra $(A,\alpha)$ for any of the comonads $\mathbb{E}_{k}$,
$\mathbb{P}_{n}$ or $\mathbb{M}_{k}$ is a _path_ if, when regarded as a
forest-ordered structure $(A,\leq)$, it is a finite linear order. Paths will
be denoted by $P,Q$ and variations thereof.

Before we continue, let us make the following point about the handling of the
equality symbol. Recall from §5.2 the comonads $\mathbb{G}^{I}$ and
$\mathbb{G}^{=}$, for a generic game comonad $\mathbb{G}$ on
$\mathbf{Struct}(\sigma)$. We have seen that there is a full embedding
$\mathbf{Kl}(\mathbb{G}^{=})\to\mathbf{Kl}(\mathbb{G}^{I})$ sending $A$ to
$J(A)$ (see Remark 5.2), and therefore the existence of an (iso)morphism $A\to
B$ in $\mathbf{Kl}(\mathbb{G}^{=})$ is equivalent to the existence of an
(iso)morphism $J(A)\to J(B)$ in $\mathbf{Kl}(\mathbb{G}^{I})$.

When considering the Eilenberg–Moore categories for the comonads
$\mathbb{G}^{I}$ and $\mathbb{G}^{=}$, the situation is quite different. There
is a canonical comparison functor

$\mathbf{EM}(\mathbb{G}^{I})\to\mathbf{EM}(\mathbb{G}^{=}),$

but it is _not_ fully faithful (this follows e.g. from the criterion dual to
the one in (Mesablishvili, 2006, Proposition 2.2)). Since the category
$\mathbf{EM}(\mathbb{G}^{I})$ typically admits a concrete and simple
description as outlined in §6.1, instead of working with (the Eilenberg–Moore
adjunction associated with) the comonad $\mathbb{G}^{=}$, we work with its
_resolution_

(2)
${\mathbf{Struct}(\sigma)}$$\top$${\mathbf{Struct}(\sigma^{I})}$$\top$${\mathbf{EM}(\mathbb{G}^{I})}$$\scriptstyle{J}$$\scriptstyle{F^{I}}$$\scriptstyle{H}$$\scriptstyle{L^{I}}$

where $L^{I}\dashv F^{I}$ is the Eilenberg–Moore adjunction associated with
$\mathbb{G}^{I}$. In order to improve readability, we will use the notation

(3) $\mathscr{F}^{I}\coloneqq F^{I}\circ
J\colon\mathbf{Struct}(\sigma)\to\mathbf{EM}(\mathbb{G}^{I}).$

###  7.1. Existential fragments and pathwise embeddings

Given a class of first-order formulas $\mathcal{L}$, we write

$\exists\mathcal{L}$

for the fragment of $\mathcal{L}$ consisting of _existential formulas_ , i.e.
those formulas that contain no universal quantifiers and in which negations
are only applied to atomic subformulas. In the case of modal logic, the
existential formulas are those in which the modalities $\Box_{\alpha}$ do not
appear and the negation symbol is only applied to propositional variables.
Since preserving the validity of negated atomic formulas is equivalent to
_reflecting_ the validity of atomic formulas, we should look at coalgebra
morphisms that not only preserve relations but also reflect them (at least in
appropriate cases). This leads us to the notion of pathwise embedding.

Recall that a homomorphism of $\sigma$-structures $h\colon A\to B$ is an
_embedding_ if it is injective and, for each relation symbol $R\in\sigma$ of
arity $n$ and each $(a_{1},\ldots,a_{n})\in A^{n}$,

$(h(a_{1}),\ldots,h(a_{n}))\in R^{B}\ \Longrightarrow\ (a_{1},\ldots,a_{n})\in
R^{A}.$

Now, let $\operatorname{\mathscr{A}}$ be any of the categories
$\mathbf{EM}(\mathbb{E}_{k})$, $\mathbf{EM}(\mathbb{P}_{n})$ or
$\mathbf{EM}(\mathbb{M}_{k})$.

###### Definition 7.2.

Let $f\colon X\to Y$ be an arrow in $\operatorname{\mathscr{A}}$.

  * •

$f$ is an _embedding_ , written $\rightarrowtail$, if its underlying
homomorphism of $\sigma$-structures is.

  * •

If $X$ is a path and $f$ is an embedding, then $f$ is called a _path
embedding_.

  * •

$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. That is, the restriction of $f$ to each branch of the forest is an
embedding.

###### Remark 7.3.

Every embedding in $\operatorname{\mathscr{A}}$ is a pathwise embedding; the
converse need not hold because pathwise embeddings may fail to be injective.

Akin to the homomorphism preorder, we can consider the preorder between
objects determined by the existence of a pathwise embedding between them. The
next result states that this preorder captures exactly preservation of the
existential fragments. Recall the functor $\mathscr{F}^{I}$ from eq. (3); with
this notation, we have

###### Theorem 7.4.

The following statements hold for each $k,n\in\mathbb{N}$ and (pointed)
structures $A,B$:

  1. (1)

$A\Rrightarrow_{\exists\mathrm{FO}_{k}}B$ if and only if there is a pathwise
embedding $\mathscr{F}^{I}(A)\to\mathscr{F}^{I}(B)$ in
$\mathbf{EM}(\mathbb{E}_{k}^{I})$.

  2. (2)

$A\Rrightarrow_{\exists L^{n}_{\infty,\omega}}B$ if and only if there is a
pathwise embedding ${\mathscr{F}^{I}(A)\to\mathscr{F}^{I}(B)}$ in
$\mathbf{EM}(\mathbb{P}_{n}^{I})$.

  3. (3)

$(A,a)\Rrightarrow_{\exists\mathrm{ML}_{k}}(B,b)$ if and only if there is a
pathwise embedding $F(A,a)\to F(B,b)$ in $\mathbf{EM}(\mathbb{M}_{k})$.

While Theorem 5.3 relied on the correspondence between Kleisli arrows and
Duplicator winning strategies in the existential positive variant of the
games, Theorem 7.4 relies on a correspondence between pathwise embeddings and
Duplicator winning strategies in the _existential_ variant of the games. In
these games, Spoiler is forced to play in $A$ and Duplicator responds in $B$,
and the winning condition is the same as in the back-and-forth game.

###  7.2. Full fragments and open maps

In order to capture equivalence of structures in the full fragments
$\mathcal{L}$, corresponding to equivalence in the back-and-forth games, we
consider those pathwise embeddings that satisfy the following path lifting
property (as before, $\operatorname{\mathscr{A}}$ denotes any of the
categories $\mathbf{EM}(\mathbb{E}_{k})$, $\mathbf{EM}(\mathbb{P}_{n})$ or
$\mathbf{EM}(\mathbb{M}_{k})$):

###### Definition 7.5.

A morphism $f\colon X\to Y$ in $\operatorname{\mathscr{A}}$ is _open_ if each
commutative square

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

where the horizontal morphisms and the left vertical one are path embeddings,
admits a _diagonal filler_ , i.e. an arrow $Q\to X$ making the two triangles
commute (such an arrow is necessarily an embedding).

We use the notation
$\mathrel{\vphantom{\rightarrow}\mathchoice{\ooalign{$\displaystyle\circ\mkern
1.0mu$\cr$\displaystyle\longrightarrow$\cr}}{\ooalign{$\textstyle\circ\mkern
1.0mu$\cr$\textstyle\longrightarrow$\cr}}{\ooalign{$\scriptstyle\circ\mkern
1.0mu$\cr$\scriptstyle\longrightarrow$\cr}}{\ooalign{$\scriptscriptstyle\circ\mkern
1.0mu$\cr$\scriptscriptstyle\longrightarrow$\cr}}}$ to indicate that a
morphism is an open pathwise embedding. Given objects $X,Y$ of
$\operatorname{\mathscr{A}}$, a _bisimulation_ between $X$ and $Y$ is a span
of open pathwise embeddings connecting the two objects:

$X\mathrel{\vphantom{\leftarrow}\mathchoice{\ooalign{$\displaystyle\circ$\cr$\displaystyle\longleftarrow\mkern
1.0mu$\cr}}{\ooalign{$\textstyle\circ$\cr$\textstyle\longleftarrow\mkern
1.0mu$\cr}}{\ooalign{$\scriptstyle\circ$\cr$\scriptstyle\longleftarrow\mkern
1.0mu$\cr}}{\ooalign{$\scriptscriptstyle\circ$\cr$\scriptscriptstyle\longleftarrow\mkern
1.0mu$\cr}}}W\mathrel{\vphantom{\rightarrow}\mathchoice{\ooalign{$\displaystyle\circ\mkern
1.0mu$\cr$\displaystyle\longrightarrow$\cr}}{\ooalign{$\textstyle\circ\mkern
1.0mu$\cr$\textstyle\longrightarrow$\cr}}{\ooalign{$\scriptstyle\circ\mkern
1.0mu$\cr$\scriptstyle\longrightarrow$\cr}}{\ooalign{$\scriptscriptstyle\circ\mkern
1.0mu$\cr$\scriptscriptstyle\longrightarrow$\cr}}}Y$

If such a bisimulation exists, we say that $X$ and $Y$ are _bisimilar_ and
write $X\mathrel{\raisebox{1.5pt}{$\underline{\leftrightarrow}$}}Y$.

###### Remark 7.6.

An arrow $f\colon X\to Y$ in $\operatorname{\mathscr{A}}$ is an open pathwise
embedding if, and only if, for all paths $P,Q$, each commutative square

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

admits a diagonal filler (Abramsky and Reggio, 2023, Lemma 4.1). Thus, the
open pathwise embeddings are precisely the arrows in
$\operatorname{\mathscr{A}}$ that satisfy the _right lifting property_ with
respect to all morphisms between paths (cf. §8.1).

To see how bisimulations yield winning strategies in back-and-forth games,
suppose there exists a bisimulation

$X\mathrel{\mathop{\mathrel{\vphantom{\leftarrow}\mathchoice{\ooalign{$\displaystyle\circ$\cr$\displaystyle\longleftarrow\mkern
1.0mu$\cr}}{\ooalign{$\textstyle\circ$\cr$\textstyle\longleftarrow\mkern
1.0mu$\cr}}{\ooalign{$\scriptstyle\circ$\cr$\scriptstyle\longleftarrow\mkern
1.0mu$\cr}}{\ooalign{$\scriptscriptstyle\circ$\cr$\scriptscriptstyle\longleftarrow\mkern
1.0mu$\cr}}}}^{f}}W\mathrel{\mathop{\mathrel{\vphantom{\rightarrow}\mathchoice{\ooalign{$\displaystyle\circ\mkern
1.0mu$\cr$\displaystyle\longrightarrow$\cr}}{\ooalign{$\textstyle\circ\mkern
1.0mu$\cr$\textstyle\longrightarrow$\cr}}{\ooalign{$\scriptstyle\circ\mkern
1.0mu$\cr$\scriptstyle\longrightarrow$\cr}}{\ooalign{$\scriptscriptstyle\circ\mkern
1.0mu$\cr$\scriptscriptstyle\longrightarrow$\cr}}}}^{g}}Y.$

We consider a back-and-forth game between $X$ and $Y$ whose positions are
pairs of path embeddings

$(P\rightarrowtail X,P\rightarrowtail Y)$

with the same domain. Assume that the current position is given by

$(f\circ m\colon P\rightarrowtail X,g\circ m\colon P\rightarrowtail Y)$

for some path embedding $m\colon P\rightarrowtail W$. In the next round,
Spoiler plays a path embedding ${j\colon Q\rightarrowtail X}$ extending
$f\circ m$, and Duplicator must respond with a path embedding $k\colon
Q\rightarrowtail Y$ extending $g\circ m$. Duplicator can use the fact that $f$
is an open pathwise embedding to obtain a diagonal filler $n$ as displayed
below.

${P}$${W}$${Q}$${X}$$\scriptstyle{m}$$\scriptstyle{f}$$\scriptstyle{j}$$\scriptstyle{n}$

Duplicator’s response will then be $g\circ n$, which is a path embedding since
$g$ is a pathwise embedding. Symmetrically, if Spoiler plays a path embedding
$j^{\prime}$ into $Y$, Duplicator can use the fact that $g$ is an open
pathwise embedding to “lift $j^{\prime}$ along $g$” and then compose this
lifting with $f$ to obtain a path embedding into $X$.

In fact, this back-and-forth game between objects of
$\operatorname{\mathscr{A}}$ can be defined axiomatically, and the existence
of a Duplicator winning strategy turns out to be equivalent to the existence
of a bisimulation between the objects, cf. §8. For each of the game comonads
$\mathbb{E}_{k}$, $\mathbb{P}_{n}$ and $\mathbb{M}_{k}$, the axiomatic game
played between co-free coalgebras coincides with the corresponding concrete
notion of model-comparison game. We thus obtain that equivalence in the full
fragments is captured by the bisimilarity relation:

###### Theorem 7.7.

The following statements hold for each $k,n\in\mathbb{N}$ and (pointed)
structures $A,B$:

  1. (1)

$A\equiv_{\mathrm{FO}_{k}}B$ if, and only if,
$\mathscr{F}^{I}(A)\mathrel{\raisebox{1.5pt}{$\underline{\leftrightarrow}$}}\mathscr{F}^{I}(B)$
in $\mathbf{EM}(\mathbb{E}_{k}^{I})$.

  2. (2)

$A\equiv_{L^{n}_{\infty,\omega}}B$ if, and only if,
$\mathscr{F}^{I}(A)\mathrel{\raisebox{1.5pt}{$\underline{\leftrightarrow}$}}\mathscr{F}^{I}(B)$
in $\mathbf{EM}(\mathbb{P}_{n}^{I})$.

  3. (3)

$(A,a)\equiv_{\mathrm{ML}_{k}}(B,b)$ if, and only if,
$F(A,a)\mathrel{\raisebox{1.5pt}{$\underline{\leftrightarrow}$}}F(B,b)$ in
$\mathbf{EM}(\mathbb{M}_{k})$.

For example, an open pathwise embedding in the category
$\mathbf{EM}(\mathbb{M}_{k})$ is the same thing as a _p-morphism_ , also
called _bounded morphism_ , a basic notion of modal logic (see e.g. (Blackburn
et al., 2002, Definition 2.10)). Thus, two synchronization trees are bisimilar
as objects of $\mathbf{EM}(\mathbb{M}_{k})$, in the sense defined above,
precisely when they are bisimilar in the usual sense of modal logic (see e.g.
(Blackburn et al., 2002, Definition 2.16)). Therefore, item 3 in Theorem 7.7
amounts to the well-known fact that two pointed Kripke models satisfy the same
modal formulas of modal depth at most $k$ if, and only if, their
$k$-unravellings are bisimilar.

Theorem 7.7 can be proved by first showing that the existence of a
bisimulation is equivalent to the existence of a Duplicator winning strategy
in the corresponding back-and-forth game played between $A$ and $B$, and then
applying the corresponding translation result between games and logic (see
Theorems 3.1, 3.2 and 3.4).

###  7.3. Positive fragments and positive bisimulations

If $\mathcal{L}$ is a class of first-order formulas, we denote by

${}^{+}\mathcal{L}$

the fragment of $\mathcal{L}$ consisting of _positive formulas_ , i.e.
formulas that do not contain the negation symbol. Akin to the way in which
equivalence in the full fragments is captured by bisimulations, equivalence in
the positive fragments is captured by a positive variant of bisimulations:

###### Definition 7.8.

Let $X,Y$ be objects of $\operatorname{\mathscr{A}}$. A _positive
bisimulation_ from $X$ to $Y$ is a triple $(f,\iota,g)$

${W_{1}}$${W_{2}}$${X}$${Y}$$\scriptstyle{\iota}$$\scriptstyle{f}$$\scriptstyle{g}$

where $f$ and $g$ are open pathwise embeddings and $\iota$ is a bijection. We
write $X\mathrel{\raisebox{1.5pt}{$\underline{\rightarrow}$}}Y$ to indicate
the existence of a positive bisimulation from $X$ to $Y$.

The fact that $\iota$ is a bijection means that we can think of $W_{1}$ and
$W_{2}$ as having the same underlying forest order, with $W_{2}$ obtained from
$W_{1}$ by adding relations (i.e., by enlarging the interpretations of the
relation symbols in $\sigma$). This reflects the directed nature of positive
bisimulations.

###### Theorem 7.9 ((Abramsky et al., 2024a)).

The following statements hold for each $k,n\in\mathbb{N}$ and (pointed)
structures $A,B$:

  1. (1)

$A\Rrightarrow_{{}^{+}\mathrm{FO}_{k}}B$ if, and only if,
$\mathscr{F}^{I}(A)\mathrel{\raisebox{1.5pt}{$\underline{\rightarrow}$}}\mathscr{F}^{I}(B)$
in $\mathbf{EM}(\mathbb{E}_{k}^{I})$.

  2. (2)

$A\Rrightarrow_{{}^{+}L^{n}_{\infty,\omega}}B$ if, and only if,
$\mathscr{F}^{I}(A)\mathrel{\raisebox{1.5pt}{$\underline{\rightarrow}$}}\mathscr{F}^{I}(B)$
in $\mathbf{EM}(\mathbb{P}_{n}^{I})$.

  3. (3)

$(A,a)\Rrightarrow_{{}^{+}\mathrm{ML}_{k}}(B,b)$ if, and only if,
$F(A,a)\mathrel{\raisebox{1.5pt}{$\underline{\rightarrow}$}}F(B,b)$ in
$\mathbf{EM}(\mathbb{M}_{k})$.

In the case of modal logic, our notion of positive bisimulation coincides with
that of “directed simulation” from (Kurtonina and de Rijke, 1997). In _op.
cit._ , the authors show that, for any two _image-finite_ pointed Kripke
models $(A,a)$ and $(B,b)$,

$(A,a)\Rrightarrow_{{}^{+}\mathrm{ML}}(B,b)\text{ if, and only if,
}(A,a)\mathrel{\raisebox{1.5pt}{$\underline{\rightarrow}$}}(B,b).$

Item 3 in Theorem 7.9 can be regarded as a graded refinement of this result
which holds for all pointed Kripke models.

Akin to Theorem 7.7, Theorem 7.9 relies on a correspondence between positive
bisimulations and Duplicator winning strategies in the _positive_ variant of
the corresponding back-and-forth game. In this game, Spoiler can play in
either $A$ or $B$, and the winning condition is the same as in the existential
positive variant of the game (cf. §5.3).

##  8\. An axiomatic perspective: Arboreal categories

In the previous sections we have seen that the comonads $\mathbb{E}_{k}$,
$\mathbb{P}_{n}$ and $\mathbb{M}_{k}$ exhibit a similar behaviour. In each
case, their coalgebras can be represented concretely as forest-ordered
structures, and preservation of corresponding logic fragments can be captured
in terms of natural relations between co-free coalgebras, such as the
homomorphism preorder, the isomorphism and bisimilarity relations, and
variations thereof.

It is natural to ask if we can reason about a _generic_ game comonad. (Note,
however, that there is as yet no mathematical definition of a game comonad—you
know one when you see one!) To this end, we introduce the framework of
arboreal categories, which capture in an axiomatic way the main features of
the categories of coalgebras for game comonads. In §9, we will show how this
axiomatic approach can be used to give a uniform treatment of equi-resource
homomorphism preservation theorems in logic.

###  8.1. Arboreal categories

Within the categories of coalgebras $\mathbf{EM}(\mathbb{E}_{k})$,
$\mathbf{EM}(\mathbb{P}_{n})$ and $\mathbf{EM}(\mathbb{M}_{k})$, a class of
objects that plays a key role is that of paths (see Definition 7.1): they
allow us to define pathwise embeddings, open maps, bisimulations, and so
forth. It turns out that to axiomatise the concrete notion of path, as well as
a considerable part of the structure of the aforementioned categories of
coalgebras, all we need is a “good” factorisation system.

####  8.1.1. Proper factorisation systems and paths

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 each commutative square

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

admits a diagonal filler (cf. Definition 7.5). For any class $\mathscr{H}$ of
morphisms in $\operatorname{\mathscr{C}}$, let
${}^{\scaleobj{0.7}{\boxslash}}\mathscr{H}$ (respectively,
$\mathscr{H}^{\mkern 1.0mu\scaleobj{0.7}{\boxslash}}$) be the class of
morphisms having the left (respectively, right) lifting property with respect
to all morphisms in $\mathscr{H}$.

###### Definition 8.1.

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

  1. (i)

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

  2. (ii)

$\mathscr{Q}={}^{\scaleobj{0.7}{\boxslash}}\mathscr{M}$ and
$\mathscr{M}=\mathscr{Q}^{\mkern 1.0mu\scaleobj{0.7}{\boxslash}}$.

A _proper factorisation system_ is a weak factorisation system satisfying the
additional condition:

  1. (iii)

Every arrow in $\mathscr{Q}$ is an epimorphism and every arrow in
$\mathscr{M}$ a monomorphism.

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$.

Let $\operatorname{\mathscr{C}}$ be a category endowed with 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$, whose
elements are equivalence classes $[m]$ of embeddings $m\colon S\rightarrowtail
X$ (whenever convenient, we denote an equivalence class $[m]$ by any of its
representatives). For any morphism $f\colon X\to Y$ and embedding $m\colon
S\rightarrowtail X$, we can consider the
$(\mathscr{Q},\mathscr{M})$-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$, and in fact it defines a functor from
$\operatorname{\mathscr{C}}$ to the category of posets and monotone maps.

###### Definition 8.2.

An object $X$ of $\operatorname{\mathscr{C}}$ is called a _path_ provided the
poset $\operatorname{\mathbb{S}}{X}$ is a finite linear order. Paths will be
denoted by $P,Q$ and variations thereof. A _path embedding_ is an embedding
$P\rightarrowtail X$ whose domain is a path.

###### Example 8.3.

In the categories $\mathbf{EM}(\mathbb{E}_{k})$, $\mathbf{EM}(\mathbb{P}_{n})$
and $\mathbf{EM}(\mathbb{M}_{k})$, consider the proper factorisation systems
$(\mathscr{Q},\mathscr{M})$ where $\mathscr{Q}$ consists of the surjective
homomorphisms, and $\mathscr{M}$ consists of the embeddings in the sense of
Definition 7.2. In each case, the axiomatic notion of path coincides with the
concrete one given in Definition 7.1.

####  8.1.2. Arboreal categories defined

Now that we have an abstract notion of path, we can define path embeddings,
pathwise embeddings, bisimulations, and so forth, by generalising in a
straightforward manner the definitions given in the concrete setting. In
particular, we can define a notion of bisimilarity in any category equipped
with a proper factorisation system.

###### Remark 8.4.

The bisimilarity relation in arboreal categories is reminiscent of (and
inspired by) the notion of _open-map bisimilarity_ introduced in (Joyal et
al., 1993, 1996). However, there are some differences: while the latter takes
as parameter a full subcategory whose objects are called “paths”, in the
arboreal setting the notion of path is completely determined by the
factorisation system (which is thus the only “parameter”). Moreover, the
arboreal notion of open morphism is a refinement of the one used in (Joyal et
al., 1993, 1996), which in turn is a special case of the axiomatic concept of
open map in toposes (Joyal and Moerdijk, 1994). However, the two notions of
open morphisms coincide for pathwise embeddings (Abramsky and Reggio, 2023,
Lemma 4.1).

The next step is to identify sufficient conditions on the category so that
this notion of bisimilarity is well-behaved. In this regard, the sub-poset

$\operatorname{\mathbb{P}}{X}$

of $\operatorname{\mathbb{S}}{X}$ consisting of the path embeddings plays a
central role. In order for the maps
$\exists_{f}\colon\operatorname{\mathbb{S}}{X}\to\operatorname{\mathbb{S}}{Y}$
to descend to maps
$\operatorname{\mathbb{P}}{X}\to\operatorname{\mathbb{P}}{Y}$, we need that
the quotient of a path is again a path. This in turn requires that the
factorisation system $(\mathscr{Q},\mathscr{M})$ is _stable_ , i.e. for every
${e\in\mathscr{Q}}$ and ${m\in\mathscr{M}}$ with common codomain, the pullback
of $e$ along $m$ exists and belongs to $\mathscr{Q}$. Together with three
additional axioms ensuring that the collection of paths behaves as expected,
this leads to the notion of an arboreal category:

###### Definition 8.5.

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

Paths are connected:

Coproducts of paths exist and each path $P$ is _connected_ , i.e. every arrow
$P\to\coprod_{i\in I}{Q_{i}}$ into a coproduct of paths (indexed by a non-
empty set $I$) factors through some coproduct injection.

2-out-of-3 property:

Given arrows $f\colon P\to Q$ and $g\colon Q\to Q^{\prime}$ between paths, if
any two of $f$, $g$ and $g\circ f$ are quotients, then so is the third.

Path-generation:

Each object is _path-generated_ , i.e. it is the colimit of the paths that
embed into it.111111More precisely, for each object $X$, the cocone consisting
of all path embeddings into $X$, with morphisms between paths the embeddings
that make the obvious triangles commute, is a colimit cocone. Equivalently,
the full subcategory of $\operatorname{\mathscr{A}}$ defined by the paths is
_dense_ (Abramsky and Reggio, 2023, Theorem 5.1).

###### Example 8.6.

We give some examples of arboreal categories:

  1. (1)

The category of forests and forest morphisms is arboreal, when equipped with
the factorisation system (surjective morphisms, injective morphisms). The
paths are the finite chains, i.e. the forests consisting of a single branch.
Coproducts are given by disjoint union; in particular, the initial object is
the empty forest. Finite chains are easily seen to be connected, and the
2-out-of-3 property holds because forest morphisms preserve height. Finally,
each forest is path-generated because it is the colimit of the diagram given
by its branches and the embeddings between them.

The category $\operatorname{\mathscr{T}}$ of non-empty trees and forest
morphisms is equivalent to the category of forests (see Remark 6.6) and so it
also arboreal. Paths in $\operatorname{\mathscr{T}}$ are the non-empty finite
chains. Non-empty coproducts in $\operatorname{\mathscr{T}}$ are given by
smash sum, with the roots identified, and the initial object of
$\operatorname{\mathscr{T}}$ is the one-element tree.

  2. (2)

The categories of coalgebras $\mathbf{EM}(\mathbb{E}_{k})$,
$\mathbf{EM}(\mathbb{P}_{n})$ and $\mathbf{EM}(\mathbb{M}_{k})$, equipped with
the factorisation systems defined in Example 8.3, are arboreal. Coproducts in
$\mathbf{EM}(\mathbb{E}_{k})$ and $\mathbf{EM}(\mathbb{P}_{n})$ are computed
in the category of forests, while coproducts in $\mathbf{EM}(\mathbb{M}_{k})$
are computed in $\operatorname{\mathscr{T}}$. The validity of the axioms
defining arboreal categories then follows from the corresponding fact for
forests and non-empty trees.

  3. (3)

If $X$ is a forest, seen as a posetal category, then the category
$\widehat{X}$ of presheaves over $X$ is arboreal with respect to the
factorisation system (epimorphisms, monomorphisms). The paths are the
representable functors along with the initial object, and the path-generation
property amounts to the well-known fact that representables in a presheaf
category are dense. See (Reggio and Riba, 2023) for more details.

This generalises item 1: just observe that, if $X=\mathbb{N}$ is the poset of
natural numbers with the usual total order, $\widehat{\mathbb{N}}$ is
equivalent to the category of forests and their morphisms. Moreover, taking as
$X$ a one-element poset, we see that the category of sets and functions is
also a (trivial) example of arboreal category, in which the paths are the
empty set and the singletons.

###  8.2. Games in arboreal categories

####  8.2.1. The functor $\operatorname{\mathbb{P}}$

The next result provides an analogue to the forgetful functor from the
category $\mathbf{EM}(\mathbb{G})$ of coalgebras for a game comonad
$\mathbb{G}$ into the category of forests, and is a key tool in the theory of
arboreal categories.

###### Proposition 8.7.

Let $\operatorname{\mathscr{A}}$ be an arboreal category. The assignment

$(f\colon X\to Y)\ \longmapsto\
(\exists_{f}\colon\operatorname{\mathbb{P}}{X}\to\operatorname{\mathbb{P}}{Y})$

yields a functor
$\operatorname{\mathbb{P}}\colon\operatorname{\mathscr{A}}\to\operatorname{\mathscr{T}}$
into the category $\operatorname{\mathscr{T}}$ of non-empty trees and forest
morphisms.

###### Example 8.8.

In the case of modal logic,
$\operatorname{\mathbb{P}}\colon\mathbf{EM}(\mathbb{M}_{k})\to\operatorname{\mathscr{T}}$
is naturally isomorphic to the functor sending a synchronization tree to its
underlying tree order. The same is true for $\mathbf{EM}(\mathbb{E}_{k})$ and
$\mathbf{EM}(\mathbb{P}_{n})$, up to the equivalence between
$\operatorname{\mathscr{T}}$ and the category of forests (see Remark 6.6). The
fact that each $\operatorname{\mathbb{P}}{X}$ is a _non-empty_ tree is due to
the fact that arboreal categories have an initial object (obtained as an empty
coproduct) which is a path; concretely, in the case of
$\mathbf{EM}(\mathbb{E}_{k})$ and $\mathbf{EM}(\mathbb{P}_{n})$, this is the
empty coalgebra.

####  8.2.2. The arboreal game $\mathscr{G}$

The tree order on $\operatorname{\mathbb{P}}X$ and the associated covering
relation $\prec$ (cf. Footnote 7) allow us to define abstract games in any
arboreal category $\operatorname{\mathscr{A}}$ by essentially playing on the
corresponding trees. Let $X,Y$ be any two objects of
$\operatorname{\mathscr{A}}$. We define a back-and-forth game

$\mathscr{G}(X,Y)$

played by Spoiler and Duplicator as follows:

  * •

Positions in the game are pairs of path embeddings
$(m,n)\in\operatorname{\mathbb{P}}{X}\times\operatorname{\mathbb{P}}{Y}$. The
winning relation
$\mathscr{W}(X,Y)\subseteq\operatorname{\mathbb{P}}{X}\times\operatorname{\mathbb{P}}{Y}$
consists of the pairs $(m,n)$ such that
$\operatorname{dom}(m)\cong\operatorname{dom}(n)$.

  * •

Let $\bot_{X}$ and $\bot_{Y}$ be the roots of $\operatorname{\mathbb{P}}{X}$
and $\operatorname{\mathbb{P}}{Y}$, respectively. If
$(\bot_{X},\bot_{Y})\notin\mathscr{W}(X,Y)$, Duplicator loses the game.
Otherwise, the initial position is $(\bot_{X},\bot_{Y})$.

  * •

At the start of each round, with current position
$(m,n)\in\operatorname{\mathbb{P}}{X}\times\operatorname{\mathbb{P}}{Y}$,
either Spoiler chooses some $m^{\prime}\succ m$ and Duplicator must respond
with some $n^{\prime}\succ n$, or Spoiler chooses some $n^{\prime\prime}\succ
n$ and Duplicator must respond with $m^{\prime\prime}\succ m$.

  * •

Duplicator wins the round if they are able to respond and the new position is
in $\mathscr{W}(X,Y)$. Duplicator wins the game if they have a strategy that
is winning after $t$ rounds, for all $t\geq 0$.

The game $\mathscr{G}(X,Y)$ is an abstraction of the back-and-forth games
introduced in §3. For example, when
$\operatorname{\mathscr{A}}=\mathbf{EM}(\mathbb{E}_{k}^{I})$,
$X=\mathscr{F}^{I}(A)$ and $Y=\mathscr{F}^{I}(B)$ with $A,B$
$\sigma$-structures, the game $\mathscr{G}(X,Y)$ is equivalent to the
$k$-round Ehrenfeucht–Fraïssé game played between $A$ and $B$. Similarly for
$\mathbf{EM}(\mathbb{P}_{n}^{I})$ and $\mathbf{EM}(\mathbb{M}_{k})$.

In the concrete setting, we have four variants of each game, depending on
whether Spoiler can choose in both structures or only in one, and on whether
the winning condition is given by the existence of a partial homomorphism or a
partial isomorphism (or, in the case of modal logic, whether unary relations
should only be preserved or also reflected). Accordingly, along with the basic
back-and-forth games, which capture the full fragments $\mathcal{L}$, we have
their existential, positive, and existential positive variants, which capture
$\exists\mathcal{L}$, ${}^{+}\mathcal{L}$, and $\exists^{+}\mathcal{L}$,
respectively.

Likewise, we can define the following variants of the game $\mathscr{G}(X,Y)$:

  * •

In the _existential game_

$\exists\mathscr{G}(X,Y)$

Spoiler plays only in $\operatorname{\mathbb{P}}{X}$ and Duplicator responds
in $\operatorname{\mathbb{P}}{Y}$; the winning relation $\mathscr{W}(X,Y)$ is
the same as in $\mathscr{G}(X,Y)$.

  * •

In the _positive game_

${}^{+}\mathscr{G}(X,Y)$

Spoiler can play in either $\operatorname{\mathbb{P}}{X}$ or
$\operatorname{\mathbb{P}}{Y}$; the winning relation
$\mathscr{W}^{+}(X,Y)\subseteq\operatorname{\mathbb{P}}{X}\times\operatorname{\mathbb{P}}{Y}$
consists of the pairs $(m,n)$ such that there exists a morphisms
$\operatorname{dom}(m)\to\operatorname{dom}(n)$.

  * •

In the _existential positive game_

$\exists^{+}\mathscr{G}(X,Y)$

Spoiler plays only in $\operatorname{\mathbb{P}}{X}$ and Duplicator responds
in $\operatorname{\mathbb{P}}{Y}$; the winning relation $\mathscr{W}^{+}(X,Y)$
is the same as in ${}^{+}\mathscr{G}(X,Y)$.

The following result relates the games $\mathscr{G}$, $\exists^{+}\mathscr{G}$
and $\exists\mathscr{G}$ to the corresponding relations induced by
bisimulations, morphisms, and pathwise embeddings, respectively; the case of
the game ${}^{+}\mathscr{G}$ is discussed below.

###### Theorem 8.9.

The following statements hold for all objects $X,Y$ of an arboreal category
$\operatorname{\mathscr{A}}$:

  1. (1)

Suppose $X$ and $Y$ admit a product in $\operatorname{\mathscr{A}}$.
Duplicator has a winning strategy in the game $\mathscr{G}(X,Y)$ if, and only
if, $X$ and $Y$ are bisimilar.

  2. (2)

Suppose the functor
$\operatorname{\mathbb{P}}\colon\operatorname{\mathscr{A}}\to\operatorname{\mathscr{T}}$
is faithful. Duplicator has a winning strategy in the game
$\exists^{+}\mathscr{G}(X,Y)$ if, and only if, there exists a morphism $X\to
Y$.

  3. (3)

Duplicator has a winning strategy in the game $\exists\mathscr{G}(X,Y)$ if,
and only if, there exists a pathwise embedding $X\to Y$.

###### Remark 8.10.

We comment on the additional assumptions in items 1 and 2 of Theorem 8.9. The
existence of a product of $X$ and $Y$ in item 1 is needed to construct the
vertex $W$ of a bisimulation between $X$ and $Y$ as an $\mathscr{M}$-subobject
of $X\times Y$.

Concerning item 2, the following are equivalent for any arboreal category
$\operatorname{\mathscr{A}}$:

  1. (a)

The functor
$\operatorname{\mathbb{P}}\colon\operatorname{\mathscr{A}}\to\operatorname{\mathscr{T}}$
is faithful.

  2. (b)

For any two paths $P,Q$ in $\operatorname{\mathscr{A}}$, there exists at most
one morphism $P\to Q$.

A Duplicator winning strategy in $\exists^{+}\mathscr{G}(X,Y)$ induces a
cocone with vertex $Y$ over the diagram of path embeddings into $X$. The
assumption that
$\operatorname{\mathbb{P}}\colon\operatorname{\mathscr{A}}\to\operatorname{\mathscr{T}}$
be faithful ensures, by item (b), that any diagram of paths commutes, and so
this is a _compatible_ cocone which yields a mediating morphism $X\to Y$
because $X$ is path-generated. This additional assumption is not needed in
item 3, because for any two paths $P,Q$ there is always at most one embedding
$P\rightarrowtail Q$ (Abramsky and Reggio, 2023, Lemma 3.15(c)).

The categories of coalgebras $\mathbf{EM}(\mathbb{E}_{k}^{I})$,
$\mathbf{EM}(\mathbb{P}_{n}^{I})$ and $\mathbf{EM}(\mathbb{M}_{k})$ satisfy
all the assumptions in Theorem 8.9, which can thus be regarded as an axiomatic
generalisation of Theorems 5.3, 7.4 and 7.7.

A similar result holds for the positive game ${}^{+}\mathscr{G}(X,Y)$, but
requires extra care; see (Abramsky et al., 2024a). First of all, since the
concrete notion of positive bisimulation in Definition 7.8 involves a set-
theoretic bijection, we need to reformulate this notion slightly in the
arboreal setting. Given objects $X,Y$ of an arboreal category
$\operatorname{\mathscr{A}}$, we call _positive bisimulation_ from $X$ to $Y$
a triple of arrows $(f,\iota,g)$

${W_{1}}$${W_{2}}$${X}$${Y}$$\scriptstyle{\iota}$$\scriptstyle{f}$$\scriptstyle{g}$

where $f$ and $g$ are open pathwise embeddings and
$\operatorname{\mathbb{P}}{\iota}$ is a bijection.

The existence of a Duplicator winning strategy in the game
${}^{+}\mathscr{G}(X,Y)$ is equivalent to the existence of a positive
bisimulation from $X$ to $Y$, provided that $\operatorname{\mathscr{A}}$
satisfies some further properties. In addition to requiring that $X$ and $Y$
admit a product, and that
$\operatorname{\mathbb{P}}\colon\operatorname{\mathscr{A}}\to\operatorname{\mathscr{T}}$
be faithful, we require that each path be _tree-connected_ —a strong form of
connectedness which is satisfied in the categories
$\mathbf{EM}(\mathbb{E}_{k})$, $\mathbf{EM}(\mathbb{P}_{n})$ and
$\mathbf{EM}(\mathbb{M}_{k})$. The latter condition is related to the functor
$\operatorname{\mathbb{P}}$ being a (Street) _fibration_ and implies that
every arrow admits a decomposition of the form $g\circ\iota$ such that
$\operatorname{\mathbb{P}}{\iota}$ is a bijection and $g$ is a pathwise
embedding, which is used to construct a positive bisimulation from $X$ to
$Y$.121212The notion of tree-connectedness is introduced in a forthcoming work
by Tomáš Jakl and the second author, where it is shown that, under appropriate
assumptions, the functor $\operatorname{\mathbb{P}}$ is a fibration and has a
right adjoint.

##  9\. Arboreal adjunctions

In the examples, the bisimilarity relation available in the arboreal
categories $\mathbf{EM}(\mathbb{E}_{k})$, $\mathbf{EM}(\mathbb{P}_{n})$ and
$\mathbf{EM}(\mathbb{M}_{k})$ is used to compare (pointed) relational
structures $A,B$ by testing bisimilarity of the co-free coalgebras $F(A)$ and
$F(B)$ or, in the presence of the equality symbol, of the coalgebras
$\mathscr{F}^{I}(A)$ and $\mathscr{F}^{I}(B)$. In other words, we transfer the
bisimilarity relation along a right adjoint functor. This leads to the
following definition:

###### Definition 9.1.

An _arboreal adjunction_ is an adjunction

(4)
${\operatorname{\mathscr{E}}}$$\top$${\operatorname{\mathscr{A}}}$$\scriptstyle{F}$$\scriptstyle{L}$

where $\operatorname{\mathscr{A}}$ is an arboreal category and
$\operatorname{\mathscr{E}}$ is any category. We shall refer to
$\operatorname{\mathscr{E}}$ as the _extensional category_ ; this is typically
a category of (pointed) relational structures.

###### Example 9.2.

The Eilenberg–Moore adjunction associated with any of the comonads
$\mathbb{E}_{k}$, $\mathbb{P}_{n}$ and $\mathbb{M}_{k}$ is arboreal. The
composite adjunctions as in eq. (2) are also arboreal.

###### Remark 9.3.

_Resource-indexed_ arboreal adjunctions can also be defined, to take into
account the resource parameters.

###  9.1. $F$-bisimilarity

Given an arboreal adjunction as in eq. (4), the _$F$ -bisimilarity_ relation
$\mathrel{\raisebox{1.5pt}{$\underline{\leftrightarrow}$}}_{F}$ between
objects $a,b$ of $\operatorname{\mathscr{E}}$ is defined by

$a\mathrel{\raisebox{1.5pt}{$\underline{\leftrightarrow}$}}_{F}b\ \text{ if,
and only if, }\ Fa\mathrel{\raisebox{1.5pt}{$\underline{\leftrightarrow}$}}Fb\
\text{ (i.e., $Fa$ and $Fb$ are bisimilar in $\operatorname{\mathscr{A}}$).}$

With this notation, item 1 of Theorem 8.9 entails that the equivalence
relations $\equiv_{\mathrm{FO}_{k}}$, $\equiv_{L^{n}_{\infty,\omega}}$ and
$\equiv_{\mathrm{ML}_{k}}$ between (pointed) structures coincide with
$\mathrel{\raisebox{1.5pt}{$\underline{\leftrightarrow}$}}_{F}$ for an
appropriate choice of the right adjoint functor $F$. Similarly, we can
transfer other relations from the arboreal category to the extensional one,
yielding e.g. relations

$\cong_{F}\ \text{ and }\ \to_{F}$

between objects of $\operatorname{\mathscr{E}}$.

One may ask if there is an _upper bound_ to the expressive power of the
$F$-bisimilarity relation induced by an arboreal adjunction. Note that
isomorphic objects are always $F$-bisimilar. Could we devise, for instance, an
arboreal adjunction

(5)
${\mathbf{Struct}(\sigma)}$$\top$${\operatorname{\mathscr{A}}}$$\scriptstyle{F}$$\scriptstyle{L}$

such that $\mathrel{\raisebox{1.5pt}{$\underline{\leftrightarrow}$}}_{F}$
coincides with isomorphism of structures? The next result provides an answer
when the arboreal category $\operatorname{\mathscr{A}}$ is _locally finitely
presentable_ (in the sense of, e.g., (Adámek and Rosický, 1994; Gabriel and
Ulmer, 1971)) and the adjunction is _finitely accessible_ , i.e. $F$ preserves
filtered colimits. Note that these assumptions are satisfied in the examples
arising from game comonads: all arboreal categories in Example 8.6 are locally
finitely presentable and all adjunctions in Example 9.2 are finitely
accessible.

###### Theorem 9.4 ((Reggio and Riba, 2023)).

Given an arboreal adjunction as in eq. (5), suppose that
$\operatorname{\mathscr{A}}$ is locally finitely presentable and the
adjunction is finitely accessible. Then
${\equiv_{L_{\infty,\omega}}}\subseteq{\mathrel{\raisebox{1.5pt}{$\underline{\leftrightarrow}$}}_{F}}$.

In other words, under the assumptions of the previous theorem, the
$F$-bisimilarity relation cannot distinguish two structures that satisfy the
same sentences in $L_{\infty,\omega}$ or, equivalently, that are _potentially
isomorphic_ (Karp, 1965). In fact, this bound is tight: there exists a
finitely accessible arboreal adjunction such that
${\equiv_{L_{\infty,\omega}}}={\mathrel{\raisebox{1.5pt}{$\underline{\leftrightarrow}$}}_{F}}$,
namely the one induced by the infinitary Ehrenfeucht–Fraïssé comonad
$\mathbb{E}_{\omega}$ in Proposition 4.5 (composed with the adjunction
$H\dashv J$ between $\sigma$-structures and $\sigma^{I}$-structures).

###### Remark 9.5.

Theorem 9.4 is a special case of a more general result which applies not only
to extensional categories of the form $\mathbf{Struct}(\sigma)$ but, more
generally, to categories of models of _cartesian theories_ (see (Coste, 1976)
or (Johnstone, 2002, §D1.3)). Furthermore, if we replace $F$-bisimilarity with
_$F$ -back-and-forth equivalence_, which relates objects $a$ and $b$ exactly
when Duplicator has a winning strategy in the game $\mathscr{G}(F(a),F(b))$,
then the previous theorem can be extended to _wooded categories_ , a
considerable weakening of the notion of arboreal
category.131313$F$-bisimilarity and $F$-back-and-forth equivalence coincide in
any arboreal category with binary products by Theorem 8.9, but need not
coincide in wooded categories.

For more details see (Reggio and Riba, 2023), which is based on the use of
Gabriel–Ulmer duality for locally finitely presentable categories (Gabriel and
Ulmer, 1971), and on Hodges’ _word-constructions_ (Hodges, 1974, 1975).

###  9.2. The bisimilar companion property and homomorphism preservation
theorems

The following property of arboreal adjunctions turns out to be a key _dividing
line_ :

###### Definition 9.6.

An arboreal adjunction $L\dashv
F\colon\operatorname{\mathscr{E}}\to\operatorname{\mathscr{A}}$, with induced
comonad $\mathbb{G}\coloneqq LF$, has the _bisimilar companion property_ if
$a\mathrel{\raisebox{1.5pt}{$\underline{\leftrightarrow}$}}_{F}\mathbb{G}(a)$
for all objects $a$ of $\operatorname{\mathscr{E}}$.

The arboreal adjunctions associated with the comonads $\mathbb{M}_{k}$ have
the bisimilar companion property; in fact, the idempotency of the modal
comonads implies the stronger property $a\cong_{F}\mathbb{G}(a)$. On the other
hand, the arboreal adjunctions arising from the comonads $\mathbb{E}_{k}$ and
$\mathbb{P}_{n}$ do not have the bisimilar companion property. In between,
there are e.g. the _guarded comonads_ (Abramsky and Marsden, 2021),
corresponding to guarded fragments of first-order logic (Andréka et al.,
1998), which satisfy the bisimilar companion property but are not idempotent.

The bisimilar companion property is correlated with the tractability of the
corresponding logics: the modal and guarded fragments are decidable and have
the tree-model property (Vardi, 1997; Grädel, 2001), while the quantifier rank
and finite-variable fragments (which are “expressive”, in the sense that they
cover the whole of first-order logic) do not. These observations provide a
first step towards using structural properties of comonadic semantics to
classify logic fragments and their expressive power.

From the comonadic perspective, the bisimilar companion property is central to
the analysis of homomorphism preservation theorems in logic (Abramsky and
Reggio, 2024). Preservation theorems relate the syntactic shape of formulas to
the semantic property of being preserved under a class of transformations.
E.g. the classical _homomorphism preservation theorem_ (HPT), due to Łoś,
Lyndon and Tarski (Łoś, 1955; Tarski, 1955; Lyndon, 1959), states that a
first-order sentence is preserved under homomorphisms between models (of a
theory $T$) if, and only if, it is equivalent (modulo $T$) to an existential
positive sentence. Rossman’s _Finite HPT_ (Rossman, 2008), a seminal result in
finite model theory, shows that the classical HPT holds relative to finite
relational structures (with $T=\emptyset$ the empty theory). This is a
striking result, as most preservation theorems fail on finite structures, see
e.g. (Tait, 1959; Ajtai and Gurevich, 1987). On his way to the celebrated
Finite HPT, Rossman established the following _Equirank HPT_ , a remarkable
resource-sensitive refinement of the classical result:

###### Theorem 9.7.

Let $\varphi$ be a first-order sentence of quantifier rank $\leq k$ in a
relational signature $\sigma$. Then $\varphi$ is preserved under homomorphisms
between $\sigma$-structures if, and only if, it is equivalent to an
existential positive sentence $\psi$ of quantifier rank $\leq k$.

To rephrase the previous result in a categorical language, we introduce the
following terminology for an arbitrary full subcategory
$\operatorname{\mathscr{D}}$ of the extensional category
$\operatorname{\mathscr{E}}$:

  * •

$\operatorname{\mathscr{D}}$ 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}}$.

  * •

Given a relation $\nabla$ on the class of objects of
$\operatorname{\mathscr{E}}$, $\operatorname{\mathscr{D}}$ is _upwards closed
(in $\operatorname{\mathscr{E}}$) with respect to $\nabla$_ if

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

  * •

If the previous condition is satisfied and $\nabla$ is an equivalence
relation, we say that $\operatorname{\mathscr{D}}$ is _saturated under
$\nabla$_.

For any arboreal adjunction $L\dashv
F\colon\operatorname{\mathscr{E}}\to\operatorname{\mathscr{A}}$, we can then
consider the following statement:

  1. (HP)

For any full subcategory $\operatorname{\mathscr{D}}$ of
$\operatorname{\mathscr{E}}$ saturated under
$\mathrel{\raisebox{1.5pt}{$\underline{\leftrightarrow}$}}_{F}$,
$\operatorname{\mathscr{D}}$ is closed under morphisms precisely when it is
upwards closed with respect to $\to_{F}$.

When considering the arboreal adjunction in eq. (2) with
$\mathbb{G}=\mathbb{E}_{k}$ the Ehrenfeucht–Fraïssé comonad, the full
subcategories of $\mathbf{Struct}(\sigma)$ saturated under
$\mathrel{\raisebox{1.5pt}{$\underline{\leftrightarrow}$}}_{F}$ coincide with
the model classes of sentences in $\mathrm{FO}_{k}$, and those that are
upwards closed with respect to $\to_{F}$ with the model classes of sentences
in $\exists^{+}\mathrm{FO}_{k}$. Therefore, in this case, property (HP)
coincides with the Equirank HPT.

In general, property (HP) can be regarded as an abstract formulation of an
_equi-resource homomorphism preservation theorem_ , stating that the
complexity of a sentence $\varphi$ invariant under homomorphisms can be
preserved when passing to an equivalent existential positive sentence $\psi$.

The right-to-left implication in (HP) is always satisfied and corresponds to
the fact that existential positive sentences are preserved under
homomorphisms. Consider now the reverse implication: let
$\operatorname{\mathscr{D}}$ be a full subcategory of
$\operatorname{\mathscr{E}}$ closed under morphisms and saturated under
$\mathrel{\raisebox{1.5pt}{$\underline{\leftrightarrow}$}}_{F}$, and suppose
that $a\to_{F}b$ for objects $a,b$ of $\operatorname{\mathscr{E}}$. By
definition, this means that there is an arrow $F(a)\to F(b)$ and so, as $L$ is
left adjoint to $F$, there is an arrow $\mathbb{G}(a)=LF(a)\to b$. If the
arboreal adjunction satisfies the bisimilar companion property, we get

(6)
$a\,\mathrel{\raisebox{1.5pt}{$\underline{\leftrightarrow}$}}_{F}\,\mathbb{G}(a)\,\to\,b.$

Therefore, $a\in\operatorname{\mathscr{D}}$ implies
$b\in\operatorname{\mathscr{D}}$, and so $\operatorname{\mathscr{D}}$ is
upwards closed with respect to $\to_{F}$. That is,

###### Proposition 9.8.

(HP) holds for any arboreal adjunction with the bisimilar companion property.

The previous proposition yields, for example, equi-resource homomorphism
preservation theorems for (graded) modal logic and guarded logic. Moreover,
these results relativise to finite structures because the corresponding
comonads restrict to finite structures; see (Abramsky and Reggio, 2024, §§5.1,
5.3).

When an arboreal adjunction does _not_ have the bisimilar companion property,
it can happen that
$a\mathbin{\centernot\mathrel{\raisebox{1.5pt}{$\underline{\leftrightarrow}$}}}_{F}\mathbb{G}(a)$
and so we cannot use eq. (6) to derive (HP). We may try to “force” the
bisimilar companion property by constructing companions $a^{*}\rightleftarrows
a$ and $\mathbb{G}(a)^{*}\rightleftarrows\mathbb{G}(a)$ that are
$F$-bisimilar:

${a^{*}}$${{\mathrel{\raisebox{1.5pt}{$\underline{\leftrightarrow}$}}_{F}}}$${\mathbb{G}(a)^{*}}$${a}$${{\rightleftarrows_{F}}}$${\mathbb{G}(a)}$${b}$

Since it is always the case that $a\rightleftarrows_{F}\mathbb{G}(a)$ (i.e.,
$a\to_{F}\mathbb{G}(a)$ and $\mathbb{G}(a)\to_{F}a$), we are essentially
upgrading the relation $\rightleftarrows_{F}$ to the finer relation
$\mathrel{\raisebox{1.5pt}{$\underline{\leftrightarrow}$}}_{F}$. This is the
strategy adopted by Rossman to prove his homomorphism preservation theorems;
for example the Equirank HPT is based on an upgrading of the relation
$\equiv_{\exists^{+}\mathrm{FO}_{k}}$ to the relation
$\equiv_{\mathrm{FO}_{k}}$. This kind of _upgrading argument_ is a powerful
tool in finite model theory for obtaining preservation theorems and, more
generally, expressive completeness results; see (Otto, 2011) for an overview
of this method.

A fully axiomatic proof of the Equirank HPT, in the language of arboreal
adjunctions, was given in (Abramsky and Reggio, 2024) using the argument
outlined above. The main hurdle is to construct the companions $a^{*}$ and
$\mathbb{G}(a)^{*}$, which are called _extendable covers_ of $a$ and
$\mathbb{G}(a)$ in _op. cit._ These are defined as colimits of certain
countable chains of sections in the extensional category, similar to a small
object argument in abstract homotopy theory; we come back to this topic in the
next section.

Finally, let us mention that it is an open problem whether a Finite Equirank
HPT holds. On the other hand, by combining the classical (respectively,
Finite) HPT with the main combinatorial construction in (Bova and Chen, 2019),
one obtains a _(Finite) Equivariable HPT_. An axiomatic understanding of the
latter, as well as of the Finite HPT, has so far been elusive; partial results
were obtained in (Paine, 2020).

##  10\. Towards a homotopical view on logical resources

Many questions in (finite) model theory, and more generally in logic, can be
phrased as _model existence_ problems: is there a (finite) model satisfying a
collection of logically specified properties? In classical model theory, the
Compactness Theorem is a basic tool to tackle these problems. On the other
hand, in finite and resource-sensitive model theory one typically addresses a
model existence problem via the _model construction_ method, which consists in
explicitly constructing a model satisfying the desired properties. We saw an
example of this in §9.2, where an upgrading argument is combined with the
construction of extendable covers of certain relational structures.

In general, an object obtained by means of a model construction argument is
overdetermined, in the sense that it is specified up to isomorphism and not up
to equivalence with respect to the prescribed logical properties. This idea is
pervasive in mathematics and computer science: we may not want to distinguish
between two topological spaces that are homotopy equivalent, or two programs
that on the same input give the same output.

Our aim in this section is to make the analogy between resource-sensitive
model theory and homotopy more precise using the language of abstract
homotopy, also called _categorical homotopy_. We posit that categorical
homotopy provides a flexible setting in which to manipulate objects up to
logical equivalence and perform constructions that are invariant under such
equivalences; this idea is illustrated in the case of modal logic in §10.2.

###  10.1. Quillen model categories

The extremely influential concept of _model category_ was introduced by Daniel
Quillen to provide an abstract setting for homotopy theory (Quillen, 1967).
Broadly speaking, a model category is a category equipped with a notion of
weak equivalences $\mathsf{W}$ between objects, along with classes
$\mathsf{C}$ and $\mathsf{F}$ of “good” injections and surjections,
respectively.

###### Definition 10.1.

A _(Quillen) model structure_ on a (locally small, finitely bicomplete)
category $\operatorname{\mathscr{D}}$ is a triple
$(\mathsf{W},\mathsf{C},\mathsf{F})$ of classes of morphisms in
$\operatorname{\mathscr{D}}$ satisfying the following two properties:

  1. (i)

The class $\mathsf{W}$ has the 2-out-of-3 property: given composable morphisms
$u\colon X\to Y$ and $v\colon Y\to Z$, if any two of $u,v$, and $v\circ u$ are
in $\mathsf{W}$, so is the third.

  2. (ii)

$(\mathsf{C}\cap\mathsf{W},\mathsf{F})$ and
$(\mathsf{C},\mathsf{F}\cap\mathsf{W})$ are weak factorisation systems (cf.
Definition 8.1).

A _(Quillen) model category_ is a category $\operatorname{\mathscr{D}}$
equipped with a model structure $(\mathsf{W},\mathsf{C},\mathsf{F})$.

We refer to the arrows in $\mathsf{W}$, $\mathsf{C}$ and $\mathsf{F}$ as _weak
equivalences_ , _cofibrations_ and _fibrations_ , respectively. The arrows in
$\mathsf{C}\cap\mathsf{W}$ are called _trivial cofibrations_ , and those in
$\mathsf{F}\cap\mathsf{W}$ _trivial fibrations_. Cofibrations and fibrations
are denoted, respectively, by $\operatorname{\leavevmode\hbox to17.67pt{\vbox
to4.14pt{\pgfpicture\makeatletter\hbox{\hskip 3.23892pt\lower-2.06998pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{} {{}{}}{}{}{{
{\pgfsys@beginscope <EMAIL_ADDRESS>\pgfsys@setlinewidth{0.31999pt}\pgfsys@roundcap\pgfsys@roundjoin{} {}{}{}
{}{}{}
\pgfsys@setlinewidth{0.31999pt}\pgfsys@moveto{0.0pt}{1.7637pt}\pgfsys@curveto{0.11198pt}{1.10231pt}{1.34401pt}{0.11023pt}{1.68001pt}{0.0pt}\pgfsys@curveto{1.34401pt}{-0.11023pt}{0.11198pt}{-1.10231pt}{0.0pt}{-1.7637pt}\pgfsys@stroke\pgfsys@endscope}}
}{}{}{{}}{ { {\pgfsys@beginscope{{}}
\pgfsys@setdash{}{0.0pt}\pgfsys@miterjoin{} {} {} {}
\pgfsys@moveto{-3.23892pt}{0.0pt}\pgfsys@lineto{-0.2pt}{1.76999pt}\pgfsys@lineto{0.0pt}{0.0pt}\pgfsys@lineto{-0.2pt}{-1.76999pt}\pgfsys@closepath\pgfsys@fillstroke\pgfsys@endscope}}
}{}{}{{}}\pgfsys@moveto{3.13893pt}{0.0pt}\pgfsys@lineto{13.8264pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{ {{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{-1.0}{0.0}{0.0}{-1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{12.38638pt}{0.0pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}$ and
$\operatorname{\leavevmode\hbox to14.63pt{\vbox
to4.14pt{\pgfpicture\makeatletter\hbox{\hskip 0.2pt\lower-2.06998pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{} {{}{}}{}{}{ {
{\pgfsys@beginscope \pgfsys@setdash{}{0.0pt}\pgfsys@miterjoin{} {} {} {}
\pgfsys@moveto{2.71016pt}{0.0pt}\pgfsys@lineto{0.2pt}{1.73265pt}\pgfsys@lineto{0.0pt}{0.0pt}\pgfsys@lineto{0.2pt}{-1.73265pt}\pgfsys@closepath\pgfsys@fillstroke\pgfsys@endscope}}
}{}{}{{}}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{11.12639pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{ {{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{11.22638pt}{0.0pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}$, and weak
equivalences by
$\mathrel{\vphantom{\rightarrow}\mathchoice{\ooalign{$\displaystyle\bullet\mkern
1.0mu$\cr$\displaystyle\operatorname{\leavevmode\hbox to17.47pt{\vbox
to3.85pt{\pgfpicture\makeatletter\hbox{\hskip 0.2pt\lower-1.92369pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{}
{{}{}}{}{}{}{}{}{{}}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{16.67184pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{15.23183pt}{0.0pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}$\cr}}{\ooalign{$\textstyle\bullet\mkern
1.0mu$\cr$\textstyle\operatorname{\leavevmode\hbox to17.47pt{\vbox
to3.85pt{\pgfpicture\makeatletter\hbox{\hskip 0.2pt\lower-1.92369pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{}
{{}{}}{}{}{}{}{}{{}}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{16.67184pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{15.23183pt}{0.0pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}$\cr}}{\ooalign{$\scriptstyle\bullet\mkern
1.0mu$\cr$\scriptstyle\operatorname{\leavevmode\hbox to17.47pt{\vbox
to3.85pt{\pgfpicture\makeatletter\hbox{\hskip 0.2pt\lower-1.92369pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{}
{{}{}}{}{}{}{}{}{{}}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{16.67184pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{15.23183pt}{0.0pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}$\cr}}{\ooalign{$\scriptscriptstyle\bullet\mkern
1.0mu$\cr$\scriptscriptstyle\operatorname{\leavevmode\hbox to17.47pt{\vbox
to3.85pt{\pgfpicture\makeatletter\hbox{\hskip 0.2pt\lower-1.92369pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{}
{{}{}}{}{}{}{}{}{{}}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{16.67184pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{15.23183pt}{0.0pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}$\cr}}}$. E.g.,
$\mathrel{\vphantom{\operatorname{\leavevmode\hbox to14.63pt{\vbox
to4.14pt{\pgfpicture\makeatletter\hbox{\hskip 0.2pt\lower-2.06998pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{} {{}{}}{}{}{
}{}{}{{}}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{11.12639pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{ {{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{11.22638pt}{0.0pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}\mathchoice{\ooalign{$\displaystyle\bullet\mkern
1.0mu$\cr$\displaystyle\operatorname{\leavevmode\hbox to17.47pt{\vbox
to4.14pt{\pgfpicture\makeatletter\hbox{\hskip 0.2pt\lower-2.06998pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{} {{}{}}{}{}{
}{}{}{{}}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{13.97183pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{ {{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{14.07182pt}{0.0pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}$\cr}}{\ooalign{$\textstyle\bullet\mkern
1.0mu$\cr$\textstyle\operatorname{\leavevmode\hbox to17.47pt{\vbox
to4.14pt{\pgfpicture\makeatletter\hbox{\hskip 0.2pt\lower-2.06998pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{} {{}{}}{}{}{
}{}{}{{}}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{13.97183pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{ {{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{14.07182pt}{0.0pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}$\cr}}{\ooalign{$\scriptstyle\bullet\mkern
1.0mu$\cr$\scriptstyle\operatorname{\leavevmode\hbox to17.47pt{\vbox
to4.14pt{\pgfpicture\makeatletter\hbox{\hskip 0.2pt\lower-2.06998pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{} {{}{}}{}{}{
}{}{}{{}}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{13.97183pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{ {{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{14.07182pt}{0.0pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}$\cr}}{\ooalign{$\scriptscriptstyle\bullet\mkern
1.0mu$\cr$\scriptscriptstyle\operatorname{\leavevmode\hbox to17.47pt{\vbox
to4.14pt{\pgfpicture\makeatletter\hbox{\hskip 0.2pt\lower-2.06998pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{} {{}{}}{}{}{
}{}{}{{}}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{13.97183pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{ {{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{14.07182pt}{0.0pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}$\cr}}}$ denotes a
trivial fibration.

###### Remark 10.2.

The data defining a model structure is overdetermined: any two of the classes
$\mathsf{W}$, $\mathsf{C}$ and $\mathsf{F}$ determine the third. For example,
an arrow is a weak equivalence exactly when it can be factored as a trivial
cofibration followed by a trivial fibration. In fact, by a result of Joyal
(see (Joyal, 2008, Proposition E.1.10) or (Riehl, 2014, Theorem 15.3.1)), a
model structure on a category is completely determined by its cofibrations
together with its class of _fibrant_ objects:

###### Definition 10.3.

An object $X$ of a model category is _fibrant_ if the unique morphism
$X\to\mathbf{1}$ to the terminal object is a fibration.

A convenient notion of morphism between model categories is that of Quillen
adjunction:

###### Definition 10.4.

A _Quillen adjunction_ between model categories $\operatorname{\mathscr{D}}$
and $\operatorname{\mathscr{D}}^{\prime}$ is an adjoint pair of functors

${\operatorname{\mathscr{D}}}$$\top$${\operatorname{\mathscr{D}}^{\prime}}$$\scriptstyle{G}$$\scriptstyle{F}$

such that $F$ preserves cofibrations and $G$ preserves fibrations.

A special class of model categories that we will encounter in the context of
modal logic is that of Cisinski model categories (Cisinski, 2006). Recall that
a model structure $(\mathsf{W},\mathsf{C},\mathsf{F})$ on a Grothendieck topos
is a _Cisinski model structure_ if it satisfies the following properties:

  1. (i)

it is _cofibrantly generated_ , i.e. there exist (small) sets $I,J$ permitting
the small object argument141414See e.g. (Riehl, 2014, §12.2) for a discussion
of what it means to “permit the small object argument”. such that
$\mathsf{C}={}^{\scaleobj{0.7}{\boxslash}}(I^{\mkern
1.0mu\scaleobj{0.7}{\boxslash}})$ and
$\mathsf{C}\cap\mathsf{W}={}^{\scaleobj{0.7}{\boxslash}}(J^{\mkern
1.0mu\scaleobj{0.7}{\boxslash}})$.

  2. (ii)

$\mathsf{C}$ coincides with the class of monomorphisms.

By Remark 10.2, a Cisinski model structure is completely determined by its
class of fibrant objects.

###  10.2. A model category for modal logic

Fix an arbitrary positive integer $k$ and recall from §6.1.1 the category
$\mathbf{EM}(\mathbb{M}_{k})$ of Eilenberg–Moore coalgebras for the modal
comonad $\mathbb{M}_{k}$. We denote by

$\mathbf{S}_{k}$

its (wide) subcategory having the same objects but morphisms the pathwise
embeddings. Concretely, $\mathbf{S}_{k}$ can be thought of as the category of
synchronization trees of height $\leq k$ and homomorphisms of Kripke models
that reflect the unary relations (cf. Theorem 6.4).

The category $\mathbf{S}_{k}$ is typically neither complete nor cocomplete. In
fact, if the modal vocabulary contains at least one unary relation symbol,
then $\mathbf{S}_{k}$ admits neither an initial object nor a terminal object.
We can (co)complete it by embedding it into a presheaf category: if
$\mathbf{P}_{k}$ denotes the full subcategory of $\mathbf{S}_{k}$ defined by
the paths (i.e., the finite branches), the restricted Yoneda embedding

(7) $\mathbf{S}_{k}\to\widehat{\mathbf{P}_{k}},\ \ \
A\mapsto\left(\mathbf{S}_{k}(-,A)\colon\mathbf{P}_{k}^{\mathrm{op}}\to\operatorname{\mathbf{Set}}\right)$

is full and faithful because $\mathbf{P}_{k}$ is dense in $\mathbf{S}_{k}$. We
can thus identify $\mathbf{S}_{k}$ (as well as $\mathbf{P}_{k}$) with a full
subcategory of $\widehat{\mathbf{P}_{k}}$. Note that the category
$\mathbf{P}_{k}$ is a preorder; for simplicity, we shall work with a small
skeleton of the class of paths, so that $\mathbf{P}_{k}$ can be identified
with a (small) forest.

We argue that the presheaf categories $\widehat{\mathbf{P}_{k}}$ offer a
setting in which some key notions and constructions in modal logic admit a
natural homotopical interpretation.

###### Proposition 10.5.

The category $\widehat{\mathbf{P}_{k}}$ admits a Cisinski model structure in
which an object $X$ is fibrant if, and only if, it satisfies the following
property: For all arrows $i\colon P\to Q$ in $\mathbf{P}_{k}$, if there is an
arrow $Q\to X$ then every arrow $P\to X$ admits a lifting along $i$:

${P}$${X}$${Q}$$\scriptstyle{i}$

What is more, the stratification by depth of modal formulas induces a tower of
Quillen adjunctions

${\widehat{\mathbf{P}_{1}}}$${\widehat{\mathbf{P}_{2}}}$${\widehat{\mathbf{P}_{3}}}$${\widehat{\mathbf{P}_{4}}}$$\scriptstyle{\top}$$\scriptstyle{\top}$$\scriptstyle{\top}$$\scriptstyle{\
\ \ \cdots}$

Restricting this model structure to the subcategory $\mathbf{S}_{k}$, we
recover familiar classes of Kripke homomorphisms. In fact, an arrow $f\colon
A\to B$ in $\mathbf{S}_{k}$ is a

  * •

cofibration if, and only if, it is an embedding of Kripke models, and a

  * •

trivial fibration if, and only if, it is a (surjective) _p-morphism_
(Blackburn et al., 2002, Definition 2.10).

We show how to use this homotopical structure to give a simple interpretation
of the following preservation result:

###### Theorem 10.6.

A modal formula of depth $\leq k$ is preserved under extensions of Kripke
models if, and only if, it is equivalent to an existential modal formula of
depth $\leq k$. Further, the result relativises to finite Kripke models.

The first part of the previous result, without reference to the modal depth of
formulas, was first proved by van Benthem (cf. (Andréka et al., 1998)) and
provides a semantic characterisation of the existential fragment
$\exists\mathrm{ML}$ of modal logic. As such, it is akin to the classical
Łoś–Tarski preservation theorem for first-order logic (Łoś, 1955; Tarski,
1955), which states that a first-order sentence is preserved under extensions
of models if, and only if, it is equivalent to an existential sentence. The
resource-sensitive refinement, which takes into account the modal depth of
formulas, and the relativisation to finite Kripke models are due to Rosen
(Rosen, 1997).

In the same spirit of the categorical account of homomorphism preservation
theorems in §9.2, the first part of Theorem 10.6 can be reformulated as
follows:

  1. (EP)

For any full subcategory $\operatorname{\mathscr{D}}$ of
$\mathbf{Struct}_{\bullet}(\sigma)$ saturated under
$\equiv_{\mathrm{ML}_{k}}$, $\operatorname{\mathscr{D}}$ is closed under
embeddings precisely when it is upwards closed with respect to
$\Rrightarrow_{\exists\mathrm{ML}_{k}}$.

Property (EP) can be proved by an upgrading argument, which upgrades the
relation $\Rrightarrow_{\exists\mathrm{ML}_{k}}$ to the relation
$\equiv_{\mathrm{ML}_{k}}$. For the non-trivial direction in (EP), suppose
that $\operatorname{\mathscr{D}}$ is a full subcategory of
$\mathbf{Struct}_{\bullet}(\sigma)$ saturated under $\equiv_{\mathrm{ML}_{k}}$
and closed under embeddings. If $(A,a),(B,b)\in\operatorname{\mathscr{D}}$
satisfy

$(A,a)\Rrightarrow_{\exists\mathrm{ML}_{k}}(B,b)$

then, by item 3 in Theorem 7.4, there is an arrow $f\colon F(A,a)\to F(B,b)$
in $\mathbf{S}_{k}$ from the $k$-unravelling of $(A,a)$ to that of $(B,b)$. To
conclude that $\operatorname{\mathscr{D}}$ is upwards closed with respect to
$\Rrightarrow_{\exists\mathrm{ML}_{k}}$, it suffices to find a Kripke model
$X$ as displayed below (note that we use the bisimilar companion property).

${X}$${{\equiv_{\mathrm{ML}_{k}}}}$${F(B,b)}$${(A,a)}$${{\equiv_{\mathrm{ML}_{k}}}}$${F(A,a)}$${F(B,b)}$${{\equiv_{\mathrm{ML}_{k}}}}$${(B,b)}$$\scriptstyle{f}$

In turn, such an $X$ can be obtained by taking an appropriate decomposition of
$f$ as a cofibration followed by a trivial fibration (any arrow in a model
category admits such a decomposition, but we need to ensure that $X$ is a
Kripke model and not an arbitrary presheaf):

###### Lemma 10.7.

Any morphism $(A_{1},a_{1})\to(A_{2},a_{2})$ in $\mathbf{S}_{k}$ can be
factored as a cofibration followed by a trivial fibration

$(A_{1},a_{1})\operatorname{\leavevmode\hbox to14.63pt{\vbox
to4.14pt{\pgfpicture\makeatletter\hbox{\hskip 0.2pt\lower-2.06998pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{} {{}{}}{}{}{}{}{}{{}}{
}{}{}{{}}\pgfsys@moveto{3.13893pt}{0.0pt}\pgfsys@lineto{13.8264pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{ {{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{-1.0}{0.0}{0.0}{-1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{12.38638pt}{0.0pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}X\mathrel{\vphantom{\operatorname{\leavevmode\hbox
to14.63pt{\vbox to4.14pt{\pgfpicture\makeatletter\hbox{\hskip
0.2pt\lower-2.06998pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{} {{}{}}{}{}{
}{}{}{{}}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{11.12639pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{ {{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{11.22638pt}{0.0pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}\mathchoice{\ooalign{$\displaystyle\bullet\mkern
1.0mu$\cr$\displaystyle\operatorname{\leavevmode\hbox to17.47pt{\vbox
to4.14pt{\pgfpicture\makeatletter\hbox{\hskip 0.2pt\lower-2.06998pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{} {{}{}}{}{}{
}{}{}{{}}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{13.97183pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{ {{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{14.07182pt}{0.0pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}$\cr}}{\ooalign{$\textstyle\bullet\mkern
1.0mu$\cr$\textstyle\operatorname{\leavevmode\hbox to17.47pt{\vbox
to4.14pt{\pgfpicture\makeatletter\hbox{\hskip 0.2pt\lower-2.06998pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{} {{}{}}{}{}{
}{}{}{{}}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{13.97183pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{ {{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{14.07182pt}{0.0pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}$\cr}}{\ooalign{$\scriptstyle\bullet\mkern
1.0mu$\cr$\scriptstyle\operatorname{\leavevmode\hbox to17.47pt{\vbox
to4.14pt{\pgfpicture\makeatletter\hbox{\hskip 0.2pt\lower-2.06998pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{} {{}{}}{}{}{
}{}{}{{}}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{13.97183pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{ {{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{14.07182pt}{0.0pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}$\cr}}{\ooalign{$\scriptscriptstyle\bullet\mkern
1.0mu$\cr$\scriptscriptstyle\operatorname{\leavevmode\hbox to17.47pt{\vbox
to4.14pt{\pgfpicture\makeatletter\hbox{\hskip 0.2pt\lower-2.06998pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{} {{}{}}{}{}{
}{}{}{{}}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{13.97183pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{ {{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{14.07182pt}{0.0pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}$\cr}}}(A_{2},a_{2})$

with $X\in\mathbf{S}_{k}$. Moreover, if $A_{1}$ and $A_{2}$ are finite Kripke
models, we can assume that $X$ is finite.

We have seen above that cofibrations and trivial fibrations between objects of
$\mathbf{S}_{k}$ coincide with embeddings and p-morphisms, respectively. Since
the latter preserve and reflect _all_ modal formulas, the Kripke model $X$
provided by Lemma 10.7 satisfies the upgrading argument. This proves the first
part of Theorem 10.6; the relativisation to finite models follows from the
fact that we can take $X$ to be finite if the $k$-unravellings $F(A,a)$ and
$F(B,b)$ are finite, which is the case if $A$ and $B$ are finite.

The characterisation of p-morphisms between objects of $\mathbf{S}_{k}$ as the
trivial fibrations in the model structure on $\widehat{\mathbf{P}_{k}}$
suggests the following definition.

###### Definition 10.8.

A _Morita equivalence_ between objects $X$ and $Y$ of a model category is a
span of trivial fibrations connecting the two objects:

$X\mathrel{\vphantom{\operatorname{\leavevmode\hbox to14.63pt{\vbox
to4.14pt{\pgfpicture\makeatletter\hbox{\hskip 0.2pt\lower-2.06998pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{} {{}{}}{}{}{
}{}{}{{}}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{11.12639pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{ {{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{11.22638pt}{0.0pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}\mathchoice{\ooalign{$\displaystyle\bullet$\cr$\displaystyle\operatorname{\leavevmode\hbox
to18.89pt{\vbox to4.14pt{\pgfpicture\makeatletter\hbox{\hskip
0.2pt\lower-2.06998pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{} {{}{}}{}{}{
}{}{}{{}}\pgfsys@moveto{3.09999pt}{0.0pt}\pgfsys@lineto{18.49411pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{ {{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{-1.0}{0.0}{0.0}{-1.0}{3.0pt}{0.0pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\mkern
1.0mu$\cr}}{\ooalign{$\textstyle\bullet$\cr$\textstyle\operatorname{\leavevmode\hbox
to18.89pt{\vbox to4.14pt{\pgfpicture\makeatletter\hbox{\hskip
0.2pt\lower-2.06998pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{} {{}{}}{}{}{
}{}{}{{}}\pgfsys@moveto{3.09999pt}{0.0pt}\pgfsys@lineto{18.49411pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{ {{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{-1.0}{0.0}{0.0}{-1.0}{3.0pt}{0.0pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\mkern
1.0mu$\cr}}{\ooalign{$\scriptstyle\bullet$\cr$\scriptstyle\operatorname{\leavevmode\hbox
to18.89pt{\vbox to4.14pt{\pgfpicture\makeatletter\hbox{\hskip
0.2pt\lower-2.06998pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{} {{}{}}{}{}{
}{}{}{{}}\pgfsys@moveto{3.09999pt}{0.0pt}\pgfsys@lineto{18.49411pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{ {{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{-1.0}{0.0}{0.0}{-1.0}{3.0pt}{0.0pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\mkern
1.0mu$\cr}}{\ooalign{$\scriptscriptstyle\bullet$\cr$\scriptscriptstyle\operatorname{\leavevmode\hbox
to18.89pt{\vbox to4.14pt{\pgfpicture\makeatletter\hbox{\hskip
0.2pt\lower-2.06998pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{} {{}{}}{}{}{
}{}{}{{}}\pgfsys@moveto{3.09999pt}{0.0pt}\pgfsys@lineto{18.49411pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{ {{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{-1.0}{0.0}{0.0}{-1.0}{3.0pt}{0.0pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\mkern
1.0mu$\cr}}}Z\mathrel{\vphantom{\operatorname{\leavevmode\hbox to14.63pt{\vbox
to4.14pt{\pgfpicture\makeatletter\hbox{\hskip 0.2pt\lower-2.06998pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{} {{}{}}{}{}{
}{}{}{{}}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{11.12639pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{ {{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{11.22638pt}{0.0pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}\mathchoice{\ooalign{$\displaystyle\bullet\mkern
1.0mu$\cr$\displaystyle\operatorname{\leavevmode\hbox to17.47pt{\vbox
to4.14pt{\pgfpicture\makeatletter\hbox{\hskip 0.2pt\lower-2.06998pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{} {{}{}}{}{}{
}{}{}{{}}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{13.97183pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{ {{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{14.07182pt}{0.0pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}$\cr}}{\ooalign{$\textstyle\bullet\mkern
1.0mu$\cr$\textstyle\operatorname{\leavevmode\hbox to17.47pt{\vbox
to4.14pt{\pgfpicture\makeatletter\hbox{\hskip 0.2pt\lower-2.06998pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{} {{}{}}{}{}{
}{}{}{{}}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{13.97183pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{ {{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{14.07182pt}{0.0pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}$\cr}}{\ooalign{$\scriptstyle\bullet\mkern
1.0mu$\cr$\scriptstyle\operatorname{\leavevmode\hbox to17.47pt{\vbox
to4.14pt{\pgfpicture\makeatletter\hbox{\hskip 0.2pt\lower-2.06998pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{} {{}{}}{}{}{
}{}{}{{}}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{13.97183pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{ {{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{14.07182pt}{0.0pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}$\cr}}{\ooalign{$\scriptscriptstyle\bullet\mkern
1.0mu$\cr$\scriptscriptstyle\operatorname{\leavevmode\hbox to17.47pt{\vbox
to4.14pt{\pgfpicture\makeatletter\hbox{\hskip 0.2pt\lower-2.06998pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{} {{}{}}{}{}{
}{}{}{{}}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{13.97183pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{ {{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{14.07182pt}{0.0pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}$\cr}}}Y$

We say that $X$ and $Y$ are _Morita equivalent_ if there exists a Morita
equivalence between them.151515The terminology “Morita equivalence” arises
from the theory of Lie groupoids (see e.g. (Zhu, 2009)), and is used with a
different meaning in algebra (for rings inducing equivalent categories of
modules) and categorical logic (to refer to theories with equivalent
categories of models in any topos).

###### Remark 10.9.

While Morita equivalent objects are clearly weakly equivalent, the converse
need not hold. On the other hand, in view of Kenneth Brown’s Factorization
lemma (Brown, 1973, p. 421), combined with Whitehead’s theorem (see e.g.
(Hirschhorn, 2003, Theorem 7.5.10)), Morita equivalence between fibrant
objects coincides with homotopy equivalence.

Given $k$-unravellings $F(A,a)$ and $F(B,b)$ of pointed Kripke models $(A,a)$
and $(B,b)$, respectively, any bisimulation between $F(A,a)$ and $F(B,b)$ in
the arboreal category $\mathbf{EM}(\mathbb{M}_{k})$ induces a Morita
equivalence between $F(A,a)$ and $F(B,b)$ in the model category
$\widehat{\mathbf{P}_{k}}$. In general, there are more Morita equivalences
than bisimulations, since _every_ presheaf in $\widehat{\mathbf{P}_{k}}$ can
in principle be the vertex of a Morita equivalence. However, it turns out that
$F(A,a)$ and $F(B,b)$ are bisimilar in $\mathbf{EM}(\mathbb{M}_{k})$ if, and
only if, they are Morita equivalent in $\widehat{\mathbf{P}_{k}}$. Thus, by
item 3 in Theorem 7.7,

$(A,a)\equiv_{\mathrm{ML}_{k}}(B,b)\ \Longleftrightarrow\ \text{ $F(A,a)$ and
$F(B,b)$ are Morita equivalent in $\widehat{\mathbf{P}_{k}}$}.$

Moreover, Morita equivalence in $\widehat{\mathbf{P}_{\omega}}$, where
$\mathbf{P}_{\omega}=\bigcup_{k<\omega}{\mathbf{P}_{k}}$, captures precisely
bisimilarity of Kripke models, in the usual sense of modal logic.

This observation allows, for example, to study Hennessy–Milner classes of
Kripke models via _presheaves of Morita equivalences_ ; for more details, we
refer the interested reader to (Reggio, 2023).

###  10.3. Through the lens of modal logic: presheaves over forests

It is well known that presheaves over posets are an appropriate setting for
modal logic, so the occurrence of the presheaf categories
$\widehat{\mathbf{P}_{k}}$ in the homotopy interpretation of (bounded depth)
modal logic outlined in §10.2 is perhaps not surprising.

However, it is worth observing that the perspective of game comonads and
arboreal categories points to a modal-like view on many fragments of
(infinitary) first-order logic and corresponding decompositions of structures.
A similar idea was put forward by Otto in (Otto, 2011) through the study of
modal translations induced by _observable configurations_ of relational
structures. We outline two connections between arboreal categories and modal
logic which may be important for extending the homotopical approach to other
fragments of first-order logic.

The first connection stems from a simple rephrasing of item 1 in Theorem 8.9.
Fix an arboreal category $\operatorname{\mathscr{A}}$ with binary products; we
shall assume that $\operatorname{\mathscr{A}}$ contains, up to isomorphism,
only a set $\Gamma$ of paths. Consider the modal vocabulary whose set of unary
relation symbols is $\Gamma$ and whose only binary relation symbol is denoted
by $\frown$. For each object $X$ of $\operatorname{\mathscr{A}}$, the tree
$\operatorname{\mathbb{P}}{X}$ can be regarded as a Kripke model for this
vocabulary, where $\frown$ is interpreted as the covering relation $\prec$
associated with the tree order, and the interpretation of $P\in\Gamma$
consists of the (equivalence classes of) path embeddings
$m\in\operatorname{\mathbb{P}}{X}$ whose domain is isomorphic to $P$. We write
$\mathbb{P}^{*}{X}$ for the ensuing Kripke model, whose distinguished element
is the root. With this notation, item 1 in Theorem 8.9 states that:

###### Theorem 10.10.

$X,Y\in\operatorname{\mathscr{A}}$ are bisimilar if, and only if,
$\mathbb{P}^{*}{X}$ and $\mathbb{P}^{*}{Y}$ are bisimilar as Kripke models.

When combined with the $F$-bisimilarity relation induced by an arboreal
adjunction (see §9.1), the previous result can be regarded as a
categorification of Otto’s slogan “Bisimulation as the master game” (Otto,
2011, §6.2.4). For example, in the case of the pebbling comonad, it implies
that structures $A,B$ satisfy the same sentences in $n$-variable infinitary
logic $L^{n}_{\infty,\omega}$ if, and only if, the corresponding tree-ordered
Kripke models are bisimilar. If $A$ and $B$ are finite structures, a similar
statement holds with $\mathrm{FO}^{n}$ instead of $L^{n}_{\infty,\omega}$, cf.
Corollary 3.5, but the trees are always infinite.

The second connection arises from considering presheaves over categories of
paths. The arboreal category $\operatorname{\mathscr{A}}$ embeds into the
presheaf category over its full subcategory of paths (cf. Footnote 11). The
full subcategory of paths is a preorder if, and only if, the functor
$\operatorname{\mathbb{P}}\colon\operatorname{\mathscr{A}}\to\operatorname{\mathscr{T}}$
is faithful. On the other hand, the subcategory
$\operatorname{\mathscr{A}}_{p}$ of $\operatorname{\mathscr{A}}$ defined by
the paths and the _embeddings_ between them is always a preorder and in fact,
upon fixing a small skeleton, it is a forest order; cf. Remark 8.10. The
restricted Yoneda embedding gives a functor

$\mathcal{I}\colon\operatorname{\mathscr{A}}\to\widehat{\operatorname{\mathscr{A}}_{p}},\
\ \
X\mapsto\left(\operatorname{\mathscr{A}}(-,X)\colon\operatorname{\mathscr{A}}_{p}^{\mathrm{op}}\to\operatorname{\mathbf{Set}}\right)$

which is not faithful in general, unless we restrict it to the wide
subcategory of $\operatorname{\mathscr{A}}$ defined by the pathwise
embeddings, cf. eq. (7). Yet, the category
$\widehat{\operatorname{\mathscr{A}}_{p}}$ is arboreal by item 3 in Example
8.6, and the functor $\mathcal{I}$ preserves and reflects the bisimilarity
relation.161616This (as yet unpublished) result was obtained by the second-
named author in collaboration with Colin Riba. This observation is central to
the study of Morita equivalence in the presheaf categories
$\widehat{\mathbf{P}_{k}}$ in the modal case, and suggests the possibility of
extending the homotopical analysis beyond modal logic.

Let us conclude by pointing out that objects of $\widehat{\mathbf{P}_{k}}$ can
be regarded as generalised Kripke models (for simplicity, we assume that the
modal language contains a single binary relation symbol $\frown$):

###### Definition 10.11.

A _generalised Kripke model structure_ on a presheaf
$X\in\widehat{\mathbf{P}_{k}}$ is given by:

  * •

an object $\dot{P}\in\mathbf{P}_{k}$ and a distinguished element $\dot{x}\in
X(\dot{P})$, and

  * •

for each unary relation symbol $S$, a set $\\{S_{Q}^{X}\subseteq X(Q)\mid
Q\in\mathbf{P}_{k}\\}$.

For $x_{1}\in X(Q_{1})$ and $x_{2}\in X(Q_{2})$, $x_{1}\frown x_{2}$ if and
only if

  1. (i)

$Q_{1}\prec Q_{2}$ in the forest order of $\mathbf{P}_{k}$, and

  2. (ii)

the unique embedding $i\colon Q_{1}\rightarrowtail Q_{2}$ satisfies
$X(i)\colon x_{2}\mapsto x_{1}$.

We denote this by $(X,\dot{P},\dot{x})$, or even just $(X,\dot{x})$, and refer
to it as a _generalised Kripke model_.

Each $A\in\mathbf{S}_{k}$ (identified with the corresponding representable
presheaf) can be equipped with a canonical structure of generalised Kripke
model. Recall that, for all $Q\in\mathbf{P}_{k}$, the elements of $A(Q)$ are
the embeddings $Q\rightarrowtail A$. In turn, each such embedding determines a
unique element of $A$, namely the image of the top element of $Q$. We let
$\dot{P}$ be the unique root of $\mathbf{P}_{k}$ such that there is a (unique)
embedding $m\colon\dot{P}\rightarrowtail A$, and let $\dot{x}=m\in
A(\dot{P})$. For each unary relation symbol $S$ and object
$Q\in\mathbf{P}_{k}$, we take as $S_{Q}^{A}$ the set of embeddings
$Q\rightarrowtail A$ whose corresponding element of $A$ satisfies $S$.
Finally, under the correspondence between elements of $A$ and embeddings
$Q\rightarrowtail A$ (with $Q\in\mathbf{P}_{k}$), the relation $\frown$ in
Definition 10.11 coincides with the accessibility relation of $A$.

We can then extend in a straightforward manner the satisfaction relation for
modal formulas from Kripke models to generalised Kripke models. Alternatively,
generalised Kripke models can be studied using the usual Kripke semantics by
considering their _externalisation_ : this essentially amounts to constructing
a transition system from a presheaf using the Grothendieck construction.

###### Definition 10.12.

The _externalisation_ of a generalised Kripke model $(X,\dot{x})$ is the
Kripke model $\mathbf{Ext}(X,\dot{x})$ defined as follows: the elements of
$\mathbf{Ext}(X,\dot{x})$ are the tuples $(Q,y)$ such that $y\in X(Q)$, and
the distinguished element is $(\dot{P},\dot{x})$. The accessibility relation
$\frown$ is defined as in Definition 10.11, and similarly for the unary
relation symbols (i.e., $(Q,y)$ satisfies $S$ if $y\in S_{Q}^{X}$).

For all generalised Kripke models $(X,\dot{x})$ and all modal formulas
$\varphi$, we have

$X,\dot{x}\models\varphi\ \Longleftrightarrow\
\mathbf{Ext}(X,\dot{x})\models\varphi.$

Moreover, the assignment $(X,\dot{x})\mapsto\mathbf{Ext}(X,\dot{x})$ is
functorial with respect to the obvious notion of morphism of generalised
Kripke models (which are, in particular, natural transformations). The
externalisation functor allows us to give a logic (or model-theoretic) meaning
to the homotopical structure on $\widehat{\mathbf{P}_{k}}$. In fact, if $f$ is
a morphism of generalised Kripke models that reflects the unary relations,
then (the underlying natural transformation of) $f$ is a

  * •

cofibration if, and only if, $\mathbf{Ext}(f)$ is an embedding of Kripke
models, and a

  * •

trivial fibration if, and only if, $\mathbf{Ext}(f)$ is a p-morphism.

If we take the presheaf category $\widehat{\operatorname{\mathscr{A}}_{p}}$,
where $\operatorname{\mathscr{A}}$ is the arboreal category corresponding to,
say, $n$-variable logic or first-order logic with bounded quantifier rank, the
approach outlined above yields a _translation_ $(\ \ )^{*}$ of these logic
fragments into modal logic (for the category $\widehat{\mathbf{P}_{k}}$, this
translation is the identity). The properties of this translation remain to be
fully understood, and may allow one to extend the techniques described in
§10.2 to first-order logic. Consider for example the following

_Open problem._ Does an Equirank Łoś–Tarski theorem hold?

Working with the arboreal category corresponding to the Ehrenfeucht–Fraïssé
comonad, a positive answer to this question would follow if we could prove
that for every first-order sentence $\varphi$ that is preserved under
embeddings, its modal translation $\varphi^{*}$ is also preserved under
embeddings.

## References

  * (1)
  * Abramsky (2020) S. Abramsky. 2020.  Whither semantics?  Theoretical Computer Science 807 (2020), 3–14.
  * Abramsky (2022a) S. Abramsky. 2022a.  Notes on presheaf representations of strategies and cohomological refinements of $k$-consistency and $k$-equivalence.  Preprint available at https://arxiv.org/abs/2206.12156. (2022).
  * Abramsky (2022b) S. Abramsky. 2022b.  Structure and power: an emerging landscape.  Fundamenta Informaticae 186, 1-4 (2022), 1–26.  DOI:http://dx.doi.org/10.3233/FI-222116
  * Abramsky et al. (2017) S. Abramsky, A. Dawar, and P. Wang. 2017.  The pebbling comonad in finite model theory. In 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). 1–12.
  * Abramsky et al. (2022) S. Abramsky, T. Jakl, and T. Paine. 2022.  Discrete Density Comonads and Graph Parameters. In Coalgebraic Methods in Computer Science. CMCS 2022 (Lecture Notes in Computer Science), Helle Hvid Hansen and Fabio Zanasi (Eds.), Vol. 13225\. Springer International Publishing, 23–44.
  * Abramsky et al. (2024a) S. Abramsky, T. Laure, and L. Reggio. 2024a.  Existential and positive games: a comonadic and axiomatic view. (2024).  Forthcoming.
  * Abramsky and Marsden (2021) S. Abramsky and D. Marsden. 2021.  Comonadic semantics for guarded fragments. In Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS.
  * Abramsky and Marsden (2022) S. Abramsky and D. Marsden. 2022.  Comonadic semantics for hybrid logic. In 47th International Symposium on Mathematical Foundations of Computer Science (MFCS) (Leibniz International Proceedings in Informatics), Vol. 241. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 7:1–7:14.
  * Abramsky et al. (2024b) S. Abramsky, T. Montacute, and N. Shah. 2024b.  Linear arboreal categories.  (2024).  http://arxiv.org/abs/2301.10088 To appear in the proceedings of MFPS 2024.
  * Abramsky and Reggio (2021) S. Abramsky and L. Reggio. 2021.  Arboreal Categories and Resources. In 48th International Colloquium on Automata, Languages, and Programming (ICALP 2021) (Leibniz International Proceedings in Informatics), Vol. 198. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 115:1–115:20.
  * Abramsky and Reggio (2023) S. Abramsky and L. Reggio. 2023.  Arboreal Categories: An Axiomatic Theory of Resources.  Logical Methods in Computer Science 19, 3 (2023), 14:1–14:36.  DOI:http://dx.doi.org/10.46298/lmcs-19(3:14)2023
  * Abramsky and Reggio (2024) S. Abramsky and L. Reggio. 2024.  Arboreal categories and equi-resource homomorphism preservation theorems.  Ann. Pure Appl. Logic 175, 6 (2024), Paper No. 103423, 41.  DOI:http://dx.doi.org/10.1016/j.apal.2024.103423
  * Abramsky and Shah (2018) S. Abramsky and N. Shah. 2018.  Relating Structure and Power: Comonadic Semantics for Computational Resources. In 27th EACSL Annual Conference on Computer Science Logic (CSL). 2:1–2:17.
  * Abramsky and Shah (2021) S. Abramsky and N. Shah. 2021.  Relating Structure and Power: Comonadic Semantics for Computational Resources.  Journal of Logic and Computation 31, 6 (2021), 1390–1428.
  * Adámek and Rosický (1994) J. Adámek and J. Rosický. 1994.  Locally presentable and accessible categories. London Mathematical Society Lecture Note Series, Vol. 189.  Cambridge University Press, Cambridge.
  * Ajtai and Gurevich (1987) M. Ajtai and Y. Gurevich. 1987.  Monotone versus Positive.  J. ACM 34, 4 (1987), 1004–1015.  DOI:http://dx.doi.org/10.1145/31846.31852
  * Andréka et al. (1998) H. Andréka, J. van Benthem, and I. Németi. 1998.  Modal Languages and Bounded Fragments of Predicate Logic.  Journal of Philosophical Logic 27, 3 (1998), 217–274.
  * Barwise (1977) J. Barwise. 1977.  On Moschovakis closure ordinals.  Journal of Symbolic Logic 42, 2 (1977), 292–296.
  * Blackburn et al. (2002) P. Blackburn, M. de Rijke, and Y. Venema. 2002.  Modal Logic. Cambridge Tracts in Theoretical Computer Science, Vol. 53.  Cambridge University Press.
  * Bova and Chen (2019) S. Bova and H. Chen. 2019.  How Many Variables are Needed to Express an Existential Positive Query?  Theory of Computing Systems 63, 7 (2019), 1573–1594.
  * Brown (1973) K. S. Brown. 1973.  Abstract Homotopy Theory and Generalized Sheaf Cohomology.  Trans. Amer. Math. Soc. 186 (1973), 419–458.
  * Chatzidakis (1997) Z. Chatzidakis. 1997.  Model theory of finite fields and pseudo-finite fields.  Vol. 88. 95–108.  DOI:http://dx.doi.org/10.1016/S0168-0072(97)00017-1 Joint AILA-KGS Model Theory Meeting (Florence, 1995).
  * Cisinski (2006) D.-C. Cisinski. 2006.  Les préfaisceaux comme modèles des types d’homotopie.  Astérisque 308 (2006), xxiv+390.
  * Ó Conghaile (2022) A. Ó Conghaile. 2022.  Cohomology in Constraint Satisfaction and Structure Isomorphism. In 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022) (Leibniz International Proceedings in Informatics), S. Szeider, R. Ganian, and A. Silva (Eds.), Vol. 241. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 75:1–75:16.  DOI:http://dx.doi.org/10.4230/LIPIcs.MFCS.2022.75
  * Ó Conghaile and Dawar (2021) A. Ó Conghaile and A. Dawar. 2021.  Game Comonads & Generalised Quantifiers. In 29th EACSL Annual Conference on Computer Science Logic, CSL (LIPIcs), Vol. 183. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 16:1–16:17.
  * Coste (1976) M. Coste. 1976.  Une approche logique des théories définissables par limites projectives finies.  Séminaire Bénabou. Université Paris-Nord.
  * Dawar et al. (2021) A. Dawar, T. Jakl, and L. Reggio. 2021.  Lovász-type theorems and game comonads. In Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS.
  * Dvořák (2010) Z. Dvořák. 2010.  On recognizing graphs by numbers of homomorphisms.  Journal of Graph Theory 64, 4 (2010), 330–342.
  * Ehrenfeucht (1960) A. Ehrenfeucht. 1960.  An application of games to the completeness problem for formalized theories.  Fund. Math. 49 (1960), 129–141.
  * Fagin (1974) R. Fagin. 1974.  Generalized first-order spectra and polynomial-time recognizable sets.  In Complexity of computation (Proc. SIAM-AMS Sympos., New York, 1973). SIAM-AMS Proc., Vol. VII. Amer. Math. Soc., Providence, RI, 43–73.
  * Feder and Vardi (1998) T. Feder and M. Y. Vardi. 1998.  The Computational Structure of Monotone Monadic SNP and Constraint Satisfaction: A Study through Datalog and Group Theory.  SIAM J. Comput. 28, 1 (1998), 57–104.  DOI:http://dx.doi.org/10.1137/S0097539794266766
  * Fraïssé (1954) R. Fraïssé. 1954.  Sur quelques classifications des systèmes de relations.  Publ. Sci. Univ. Alger. Sér. A 1 (1954), 35–182.
  * Gabriel and Ulmer (1971) P. Gabriel and F. Ulmer. 1971.  Lokal präsentierbare Kategorien. Lecture Notes in Mathematics, Vol. 221.  Springer-Verlag, Berlin-New York.
  * Grädel (2001) E. Grädel. 2001.  Why are modal logics so robustly decidable? World Scientific Publishing Co., Inc., USA, 393–408.
  * Grädel et al. (2007) E. Grädel, P. G. Kolaitis, L. Libkin, M. Marx, J. Spencer, M. Y. Vardi, Y. Venema, and S. Weinstein. 2007.  Finite Model Theory and Its Applications (Texts in Theoretical Computer Science. An EATCS Series).  Springer-Verlag, Berlin, Heidelberg. xiii+440 pages.  DOI:http://dx.doi.org/10.1007/3-540-68804-8
  * Grohe (2020) M. Grohe. 2020.  Counting Bounded Tree Depth Homomorphisms. In Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science. 507–520.
  * Hella (1996) L. Hella. 1996.  Logical Hierarchies in PTIME.  Information and Computation 129, 1 (1996), 1–19.  DOI:http://dx.doi.org/10.1006/inco.1996.0070
  * Hennessy and Milner (1980) M. Hennessy and R. Milner. 1980.  On observing nondeterminism and concurrency. In Automata, Languages and Programming. Springer Berlin Heidelberg, Berlin, Heidelberg, 299–309.
  * Hirschhorn (2003) P. S. Hirschhorn. 2003.  Model categories and their localizations. Mathematical Surveys and Monographs, Vol. 99.  American Mathematical Society, Providence, RI. xvi+457 pages.
  * Hodges (1974) W. Hodges. 1974.  A Normal Form for Algebraic Constructions.  Bulletin of the London Mathematical Society 6, 1 (1974), 57–60.
  * Hodges (1975) W. Hodges. 1975.  A Normal Form for Algebraic Constructions II.  Logique et Analyse 18, 71/72 (1975), 429–487.  http://www.jstor.org/stable/44083994
  * Hrushovski (2002) E. Hrushovski. 2002.  Pseudo-finite fields and related structures.  In Model theory and applications. Quad. Mat., Vol. 11. Aracne, Rome, 151–212.
  * Immerman (1982) N. Immerman. 1982.  Upper and lower bounds for first order expressibility.  J. Comput. System Sci. 25, 1 (1982), 76–98.
  * Immerman (1999) N. Immerman. 1999.  Descriptive complexity.  Springer-Verlag, New York. xvi+268 pages.  DOI:http://dx.doi.org/10.1007/978-1-4612-0539-5
  * Isbell (1991) J. Isbell. 1991.  Some inequalities in hom sets.  Journal of Pure and Applied Algebra 76, 1 (1991), 87–110.
  * Jakl et al. (2022) T. Jakl, D. Marsden, and N. Shah. 2022.  A game comonadic account of Courcelle and Feferman-Vaught-Mostowski theorems.  Preprint available at https://arxiv.org/abs/2205.05387. (2022).
  * Jakl et al. (2023) T. Jakl, D. Marsden, and N. Shah. 2023.  A categorical account of composition methods in logic. In 2023 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). 1–14.  DOI:http://dx.doi.org/10.1109/LICS56636.2023.10175751
  * Johnstone (2002) P. T. Johnstone. 2002.  Sketches of an elephant: a topos theory compendium. Vol. 2. Oxford Logic Guides, Vol. 44.  The Clarendon Press, Oxford University Press, Oxford.
  * Joyal (1981) A. Joyal. 1981.  Une théorie combinatoire des séries formelles.  Adv. in Math. 42, 1 (1981), 1–82.
  * Joyal (2008) A. Joyal. 2008.  The Theory of Quasi-Categories and its Applications. (2008).  https://mat.uab.cat/~kock/crm/hocat/advanced-course/Quadern45-2.pdf Lectures for the Advanced Course on Simplicial Methods in Higher Categories, CRM.
  * Joyal and Moerdijk (1994) A. Joyal and I. Moerdijk. 1994.  A completeness theorem for open maps.  Ann. Pure Appl. Logic 70, 1 (1994), 51–86.
  * Joyal et al. (1993) A. Joyal, M. Nielsen, and G. Winskel. 1993.  Bisimulation and open maps. In Proceedings of 8th Annual IEEE Symposium on Logic in Computer Science. 418–427.
  * Joyal et al. (1996) A. Joyal, M. Nielsen, and G. Winskel. 1996.  Bisimulation from Open Maps.  Information and Computation 127, 2 (1996), 164–185.
  * Karp (1965) C. R. Karp. 1965.  Finite-quantifier equivalence.  In Theory of Models (Proc. 1963 Internat. Sympos. Berkeley). North-Holland, Amsterdam, 407–412.
  * Kolaitis and Vardi (1992) P. G. Kolaitis and M. Y. Vardi. 1992.  Infinitary logics and $0$-$1$ laws.  Inform. and Comput. 98, 2 (1992), 258–294.
  * Kolaitis and Vardi (1995) P. G. Kolaitis and M. Y. Vardi. 1995.  On the expressive power of Datalog: tools and a case study.  J. Comput. Syst. Sci. 51, 1 (1995), 110–134.  DOI:http://dx.doi.org/10.1006/jcss.1995.1055
  * Kurtonina and de Rijke (1997) N. Kurtonina and M. de Rijke. 1997.  Simulating without Negation.  Journal of Logic and Computation 7, 4 (08 1997), 501–522.  DOI:http://dx.doi.org/10.1093/logcom/7.4.501
  * van Leeuwen (1990a) J. van Leeuwen (Ed.). 1990a.  Handbook of theoretical computer science. Vol. A.  Elsevier Science Publishers, B.V., Amsterdam; MIT Press, Cambridge, MA. x+996 pages.  Algorithms and complexity.
  * van Leeuwen (1990b) J. van Leeuwen (Ed.). 1990b.  Handbook of theoretical computer science. Vol. B.  Elsevier Science Publishers, B.V., Amsterdam; MIT Press, Cambridge, MA. xiv+1273 pages.  Formal models and semantics.
  * Libkin (2004) L. Libkin. 2004.  Elements of Finite Model Theory.  Springer.
  * Łoś (1955) J. Łoś. 1955.  On the extending of models. I.  Fund. Math. 42 (1955), 38–54.
  * Lovász (1967) L. Lovász. 1967.  Operations with structures.  Acta Math. Acad. Sci. Hungar. 18 (1967), 321–328.
  * Lyndon (1959) R. C. Lyndon. 1959.  Properties preserved under homomorphism.  Pacific J. Math. 9 (1959), 143–154.
  * Mesablishvili (2006) B. Mesablishvili. 2006.  Monads of effective descent type and comonadicity.  Theory Appl. Categ. 16, 1 (2006), 1–45.  http://www.tac.mta.ca/tac/volumes/16/1/16-01abs.html
  * Nešetřil and Ossona de Mendez (2006) J. Nešetřil and P. Ossona de Mendez. 2006.  Tree-depth, subgraph coloring and homomorphism bounds.  European Journal of Combinatorics 27, 6 (2006), 1022–1041.
  * Otto (2011) M. Otto. 2011.  Model theoretic methods for fragments of FO and special classes of (finite) structures.  In Finite and Algorithmic Model Theory, J. Esparza, C. Michaux, and C. Steinhorn (Eds.). London Mathematical Society Lecture Note Series, Vol. 379. Cambridge University Press, 271–341.
  * Otto (2023) M. Otto. 2023.  Graded modal logic and counting bisimulation.  Preprint available at https://arxiv.org/abs/1910.00039. (2023).
  * Paine (2020) T. Paine. 2020.  A Pebbling Comonad for Finite Rank and Variable Logic, and an Application to the Equirank-variable Homomorphism Preservation Theorem.  Electronic Notes in Theoretical Computer Science 352 (2020), 191–209.
  * Pultr (1973) A. Pultr. 1973.  Isomorphism types of objects in categories determined by numbers of morphisms.  Acta Scientiarum Mathematicarum 35 (1973), 155–160.
  * Quillen (1967) D. G. Quillen. 1967.  Homotopical algebra. Vol. 43.  Springer-Verlag, Berlin-New York. iv+156 pages.  DOI:http://dx.doi.org/10.1007/BFb0097438
  * Reggio (2022) L. Reggio. 2022.  Polyadic sets and homomorphism counting.  Advances in Mathematics 410 (2022), Paper No. 108712.  DOI:http://dx.doi.org/10.1016/j.aim.2022.108712
  * Reggio (2023) L. Reggio. 2023.  A model category for modal logic.  (2023).  DOI:http://dx.doi.org/10.48550/arXiv.2310.12068
  * Reggio and Riba (2023) L. Reggio and C. Riba. 2023.  Finitely accessible arboreal adjunctions and Hintikka formulae. (2023).  Preprint available at https://arxiv.org/abs/2304.12709.
  * Riehl (2014) E. Riehl. 2014.  Categorical Homotopy Theory.  Cambridge University Press.  DOI:http://dx.doi.org/10.1017/CBO9781107261457
  * Robertson and Seymour (1986) N. Robertson and P. D. Seymour. 1986.  Graph minors. II. Algorithmic aspects of tree-width.  Journal of algorithms 7, 3 (1986), 309–322.
  * Rosen (1997) E. Rosen. 1997.  Modal logic over finite structures.  J. Logic Lang. Inform. 6, 4 (1997), 427–439.
  * Rossman (2008) B. Rossman. 2008.  Homomorphism Preservation Theorems.  J. ACM 55, 3 (2008), 15:1–15:53.
  * Tait (1959) W. W. Tait. 1959.  A counterexample to a conjecture of Scott and Suppes.  The Journal of Symbolic Logic 24, 1 (1959), 15–16.  DOI:http://dx.doi.org/10.2307/2964569
  * Tarski (1955) A. Tarski. 1955.  Contributions to the theory of models. III.  Nederl. Akad. Wetensch. Proc. Ser. A. 58 (1955), 56–64 = Indagationes Math. 17, 56–64 (1955).
  * Trakhtenbrot (1950) B. A. Trakhtenbrot. 1950.  The impossibility of an algorithm for the decision problem for finite domains.  Doklady Akad. Nauk SSSR (N.S.) (1950), 569–572.
  * Ulmer (1968) F. Ulmer. 1968.  Properties of dense and relative adjoint functors.  J. Algebra 8 (1968), 77–95.  DOI:http://dx.doi.org/10.1016/0021-8693(68)90036-7
  * Väänänen (2003) J. Väänänen. 2003.  Pseudo-finite model theory.  Vol. 24. 169–183.  http://www.mat.unb.br/~matcont/volume24.html 8th Workshop on Logic, Language, Informations and Computation—WoLLIC 2001 (Brasília).
  * Vardi (1997) M. Y. Vardi. 1997.  Why is modal logic so robustly decidable? Technical Report 97-274. Rice University.  https://hdl.handle.net/1911/96465
  * Zhu (2009) C. Zhu. 2009.  $n$-Groupoids and Stacky Groupoids.  International Mathematics Research Notices 2009, 21 (2009), 4087–4141.  DOI:http://dx.doi.org/10.1093/imrn/rnp080