*This is an extended version of the conference paper [JMS23]

[a] [b] [c]

# A categorical account of
composition methods in logic

Tomáš Jakl 0000-0003-1930-4904  ,  Dan Marsden 0000-0003-0579-0323  and  Nihil
Shah 0000-0003-2844-0828  Institute of Mathematics, Czech Academy of Sciences
Faculty of Information Technology, Czech Technical University
<EMAIL_ADDRESS>University of Nottingham<EMAIL_ADDRESS>University of Cambridge<EMAIL_ADDRESS>
###### Abstract.

We present a categorical theory of the composition methods in finite model
theory – a key technique enabling modular reasoning about complex structures
by building them out of simpler components. The crucial results required by
the composition methods are Feferman–Vaught–Mostowski (FVM) type theorems,
which characterize how logical equivalence behaves under composition and
transformation of models.

Our results are developed by extending the recently introduced game comonad
semantics for model comparison games. This level of abstraction allow us to
give conditions yielding FVM type results in a uniform way. Our theorems are
parametric in the classes of models, logics and operations involved.
Furthermore, they naturally account for the existential and positive
existential fragments, and extensions with counting quantifiers of these
logics. We also reveal surprising connections between FVM type theorems, and
classical concepts in the theory of monads.

We illustrate our methods by recovering many classical theorems of practical
interest, including a refinement of a previous result by Dawar, Severini, and
Zapata concerning the 3-variable counting logic and cospectrality. To
highlight the importance of our techniques being parametric in the logic of
interest, we prove a family of FVM theorems for products of structures,
uniformly in the logic in question, which cannot be done using specific game
arguments.

This is an extended version of the LiCS 2023 conference paper of the same
name.

###### Key words and phrases:

Category theory, Comonads, Finite model theory, Feferman-Vaught-Mostowski
theorems, Composition methods, Distributive laws

Tomáš Jakl was funded by the EXPRO project 20-31529X awarded by the Czech
Science Foundation and was also supported by the Institute of Mathematics,
Czech Academy of Sciences (RVO 67985840), Dan Marsden was supported by EPSRC
grant EP/T00696X/1: Resources and co-resources: a junction between categorical
semantics and descriptive complexity, Nihil Shah was funded by UKRI under UK
government’s Horizon Europe funding guarantee grant EP/X028259/1.

##  1\. Introduction

_Composition methods_ constitute a family of techniques in finite model theory
for understanding the logical properties of complex structures [Lib04]. One
works in a modular fashion, building a structure out of simpler components.
The larger structure can then be understood in terms of the logical properties
of its parts, and how they behave under the operations used in the
construction.

The first result of this type was proved by Mostowski [Mos52], who showed that
the first-order theory of the product of two structures $A\times B$ is
determined by the first-order theories of $A$ and $B$. Later, Feferman and
Vaught famously proved a very general result for first-order logic, which
included showing that the same holds true for infinite products and infinite
disjoint unions of structures of the same type [FV59]. Since then many more
Feferman–Vaught–Mostowski (FVM) theorems111The terser Feferman–Vaught type
theorem is more common in the literature. have been shown for various
operations, logics and types of structures. These theorems have important
applications in the theory of algorithms [Mak04], for example in the
development of algorithmic meta-theorems such as Courcelle’s theorem [CE12].

For our purposes, the typical form of an FVM theorem for a fixed $n$-ary
operation $H$ and logics $L_{1},\ldots,L_{n+1}$ is as follows. Given
structures $A_{1},\dots,A_{n}$ and $B_{1},\dots,B_{n}$,

$\displaystyle\mbox{For all $i$,}\quad A_{i}\equiv_{L_{i}}B_{i},$ (1)
$\displaystyle\mbox{implies}\quad
H(A_{1},\,\ldots,\,A_{n})\equiv_{L_{n+1}}H(B_{1},\,\ldots,\,B_{n}).$

Here $\equiv_{L}$ denotes equivalence with respect to the logic $L$.
Typically, $n$ is either one or two. For example, writing $\equiv_{FO}$ for
equivalence in first-order logic, Mostowski’s result is given in the form of
(1) as:

$A_{1}\equiv_{FO}B_{1}\enspace\mbox{and}\enspace
A_{2}\equiv_{FO}B_{2}\enspace\mbox{implies}\enspace A_{1}\times
A_{2}\equiv_{FO}B_{1}\times B_{2}$

A key tool in finite model theory for establishing that two structures are
logically equivalent is that of a model comparison game. Examples of such
games are the Ehrenfeucht–Fraïssé [Ehr60, Fra55], pebbling [KV92] and
bisimulation games [HM80], establishing equivalence in fragments of first
order and modal logic. FVM theorems are typically proven using these games,
building a winning strategy for the composite structure out of winning
strategies for the components.

Despite their usefulness, working with model comparison games often requires
intricate combinatorial arguments that have to be carefully adapted with even
the slightest change of problem domain. To mitigate the difficulty with using
game arguments directly, finite model theorists introduced higher-level
methods such as locality arguments or 0–1 laws to establish model equivalences
or inexpressibility.

The recently introduced _game comonad_ framework [ADW17, AS21] provides a new
such tool. This provides a unifying formalism for reasoning about model
comparison games, using categorical methods. The definition of a comonad
enables a transfer of results from the formally dual theory of monads,
commonly encountered in the categorical semantics of computation and universal
algebra [Mog89, Mog91, Man76]. Game comonads are designed to encapsulate a
particular model comparison game, and are the key abstraction allowing us to
give uniform results, whilst avoiding making arguments specific to a
particular logic or its corresponding game.

The early work on game comonads focused on capturing many important logics
[AM21, CD21, MS22], laying the foundations for further developments. More
recent results recover classical theorems from finite model theory, as well as
completely new results [Pai20, DJR21, AM22, Reg22]. See [Abr22] for a recent
survey and [AR21, AR23] for an axiomatic formulation.

Until now, there has been no account of the composition methods with the game
comonad framework. We close this gap by introducing a novel method for proving
FVM theorems within the game comonad approach, giving results uniformly in the
classes of structures, operations and logics involved. Instantiating the
abstract results for our example game comonads yields concrete FVM theorems
with respect to four typical fragments of first-order logic:

  1. (1)

_the positive existential fragment_ , i.e. the fragment of first-order logic
of formulas not using universal quantification or negations,

  2. (2)

_the existential fragment_ i.e. the fragment of first-order logic of formulas
not using universal quantification, and in which negation can only be applied
to atomic formulas.

  3. (3)

_counting logic_ , i.e. the extension of first-order logic with counting
quantifiers,

  4. (4)

_full_ first-order logic.

As is standard in finite model theory [Lib04, EF95], it is natural to grade
these logics by a resource parameter, such as quantifier depth.
Correspondingly, the game comonadic approach to grading is to consider
collections of comonads $\mathbb{C}_{k}$, indexed by a resource parameter $k$.
As a source of concrete examples we shall consider three particular game
comonads, ${\mathbb{E}_{k}}$, ${\mathbb{P}_{k}}$ and ${\mathbb{M}_{k}}$. The
pair ${\mathbb{E}_{k}}$ and ${\mathbb{P}_{k}}$ capture first-order logic, with
their resource parameters being quantifier depth and variable count
respectively. The comonad ${\mathbb{M}_{k}}$ encapsulates modal logic up to
modal depth $k$.

Conventionally, proving an FVM theorem involves cleverly combining several
winning model-comparison game strategies to form a winning strategy on the
composite structures. In our game comonads approach, we only need to find a
collection of morphisms of a specified form to obtain an FVM theorem for the
positive existential logic. This collection of morphisms is a formal witness
to a combination of strategies. Perhaps surprisingly, to witness equivalence
in the counting logic, the same collection of morphisms only has to satisfy
two additional axioms which coincide with the standard definition of Kleisli
law [MM07].

Although of practical interest, the FVM theorems in Sections 3 and 4 are
relatively straightforward to prove. We present them in detail for pedagogical
reasons to develop the ideas gradually. The abstract FVM theorem for the full
fragment is more technically challenging. This theorem shows that two
additional assumptions suffice to extend an FVM theorem from counting logic to
the full logic. We can rephrase these assumptions categorically as showing the
operation lifts to a parametric relative right adjoint over an appropriate
category. Surprising connections arise with classical results in monad theory,
generalizing the notion of bilinear map and its classifying tensor product
from ordinary linear algebra [Koc71a, JMS22b].

Our three running example game comonads
${\mathbb{E}_{k}},{\mathbb{P}_{k}},{\mathbb{M}_{k}}$ are introduced in Section
2, along with some necessary background on comonads. Sections 3, 4 and 5 all
follow the same pattern. We introduce the categorical structure abstracting
logical equivalence with respect to the studied logical fragment, establish
the corresponding categorical FVM theorem and illustrate this with concrete
examples. The examples in Section 4 include a new refinement of a result by
Dawar, Severini, and Zapata [DSZ17], showing that equivalence in 3-variable
counting logic without equality and with restricted conjunctions implies
cospectrality. In Section 6 we observe that techniques from Section 5 also
automatically entail FVM theorems for the existential fragment. Section 7
develops FVM theorems for products of structures, uniformly in the logic of
interest, greatly generalising Mostowski’s original result. Unlike our
methods, which are parametric in the choice of game comonad, a typical game
argument cannot be used to prove such a result, as the game is tied to a
specific choice of logic.

In fact, the game comonads ${\mathbb{E}_{k}}$ and ${\mathbb{P}_{k}}$ naturally
deal with first-order logic _without equality_. There is a standard and very
flexible technique for incorporating equality, and other “enrichments” of
logics [AS21]. This is introduced and related to FVM theorems in Section 8,
and illustrated with further examples, including the handling of weak-
bisimulation.

### Related Work

Our work can be viewed as comprising model theoretic meta-theorems about the
compositionality of logics, parameterised by both the logics and operations of
interest. From this perspective, the original Feferman-Vaught theorem [FV59,
FV67] is essentially a meta-theorem parameterised by a form of generalised
product, which can be specialised to yield specific compositionality results
specifically for first-order logic. A similar generalised product meta-theorem
is used in the setting of modal or temporal logics in [Rab01, Rab07]. This
work considers specific extensions of modal logic of varying expressive power,
but does not go as far as being parameterised by the logics of interest, as in
the current work. As well as positive results, this work also considers
failure of compositionality, which is outside the scope of the present work.

Surveys of useful compositionality results, for first-order, monadic and
guarded second order logic can be found in [Mak04, BCL08].

Elementary equivalence is studied from a rather different categorical
perspective to our own in [BR18]. The compatible interaction of composition
and observable behaviour is captured by bialgebraic semantics [TP97]. Although
bialgebraic semantics has a rather different intention to the current work,
the use of a form of distributive law to witness compositionality bares some
intriguing similarity to our results.

Corollary 6.4 in [FR23] is the only other example of an FVM theorem in the
setting of game comonads. It is in fact proved concretely, by making use of
the fact that open pathwise-embeddings are precisely strong epimorphisms in
the category of pp-trees. Our work on FVM theorems for game comonads has been
motivated by our comonadic account of the Courcelle theorem [JMS22a], where
FVM theorems are an essential ingredient.

##  2\. Preliminaries

###  2.1. Categories of Relational Structures

We assume familiarity with the basic definitions of category theory, including
categories, functors and natural transformations, as can be found in any
standard introduction such as [AT10] or [Awo10]. Background on comonads, and
any less standard material is introduced as needed.

A _relational signature_ $\sigma$ is a set of _relation symbols_ , each with
an associated strictly positive natural number _arity_. A $\sigma$-structure
$A$ consists of a  _universe_ set, also denoted $A$, and for each relation
symbol $R\in\sigma$ of arity $n$, an $n$-ary relation $R^{A}$ on $A$. A
_morphism of $\sigma$-structures_ $f\colon A\rightarrow B$ is a function of
type $A\rightarrow B$, preserving relations, in the sense that for $n$-ary
$R\in\sigma$

$R^{A}(a_{1},\ldots,a_{n})\quad\mbox{implies}\quad
R^{B}(f(a_{1}),\ldots,f(a_{n})).$

For a fixed $\sigma$, $\sigma$-structures and their morphisms form our main
category of interest $\mathcal{R}(\sigma)$. We will also have need of the
category of pointed relational structures $\mathcal{R}_{*}(\sigma)$. Here the
objects $(A,a)$ are a $\sigma$-structure $A$ with a distinguished element
$a\in A$. The morphisms are $\sigma$-structure morphisms that also preserve
the distinguished element.

###  2.2. Comonads

A _comonad in Kleisli form_ on a category $\mathcal{C}$ is a triple
$(\mathbb{C},\varepsilon,(-)^{*})$ where

  * •

$\mathbb{C}$ is an object map
$\mathrm{obj}(\mathcal{C})\to\mathrm{obj}(\mathcal{C})$,

  * •

the _counit_ $\varepsilon$ is an $\mathrm{obj}({\mathcal{C}})$-indexed family
of morphisms $\varepsilon_{A}\colon\mathbb{C}(A)\to A$, for
$A\in\mathrm{obj}(\mathcal{C})$, and

  * •

the operation $(-)^{*}$ maps morphisms $f:\mathbb{C}(A)\rightarrow B$ to their
_coextension_ $f^{*}:\mathbb{C}(A)\rightarrow\mathbb{C}(B)$,

subject to the following equations:

$\displaystyle(\varepsilon_{A})^{*}=\mathrm{id}_{\mathbb{C}(A)},\quad\varepsilon_{B}\circ
f^{*}=f,\quad(g\circ f^{*})^{*}=g^{*}\circ f^{*},$ (2)

It is then standard [Man76] that $\mathbb{C}$ can be equivalently presented in
what is referred to as _comonoid form_ $(\mathbb{C},\varepsilon,\delta)$ where
$\mathbb{C}$ is an endofunctor on $\mathcal{C}$ and the rest are natural
transformation: a _counit_ $\varepsilon:\mathbb{C}\Rightarrow{I\mkern-1.0mud}$
(where ${I\mkern-1.0mud}\colon\mathcal{C}\to\mathcal{C}$ is the identity
functor) and a _comultiplication_
$\delta:\mathbb{C}\Rightarrow\mathbb{C}^{2}$. This triple is required to
satisfy
$\varepsilon\circ\delta=\mathrm{id}=\mathbb{C}(\varepsilon)\circ\delta$ and
$\delta\circ\delta=\mathbb{C}(\delta)\circ\delta$. These equations specify
that $(\mathbb{C},\varepsilon,\delta)$ form a comonoid at an appropriate level
of abstraction.

######  Lemma 1.

Every comonad in Kleisli form $(\mathbb{C},\varepsilon,(-)^{*})$ induces a
comonad in comonoid form $(\mathbb{C},\varepsilon,\delta)$ where $\mathbb{C}$
is extended to morphisms by setting $\mathbb{C}(f\colon A\to
B)=(f\circ\varepsilon_{A})^{*}$ and $\delta_{A}$ is the coextension of the
identity morphism $\mathrm{id}_{\mathbb{C}(A)}^{*}$.

Conversely, a comonad in comonoid form $(\mathbb{C},\varepsilon,\delta)$ gives
a comonad in Kleisli form $(\mathbb{C},\varepsilon,(-)^{*})$ by setting
$f^{*}=\mathbb{C}(f)\circ\delta_{A}$. These translations are inverse to each
other.

We now introduce the game comonads that we shall regularly refer to in our
examples. Each is parameterized by a positive integer $k$. The first two
comonads are defined over $\mathcal{R}(\sigma)$.

Ehrenfeucht–Fraïssé comonad ${\mathbb{E}_{k}}$:

The universe of ${\mathbb{E}_{k}}(A)$ consists of non-empty words

$[a_{1},\dots,a_{n}]$

with $a_{1},\dots,a_{n}$ from $A$ and $n\leq k$. The counit
$\varepsilon_{A}\colon{\mathbb{E}_{k}}(A)\to A$ maps $[a_{1},\ldots,a_{n}]$ to
$a_{n}$.

For an $n$-ary relational symbol $R\in\sigma$ and
$s_{1},\dots,s_{n}\in{\mathbb{E}_{k}}(A)$, set
$R^{{\mathbb{E}_{k}}(A)}(s_{1},\ldots,s_{n})$ iff:

  1. (1):

the $s_{i}$ are _pairwise comparable in the prefix order on words_ , i.e. for
every $i,j$ either $s_{i}$ is a prefix of $s_{j}$ or vice versa, and

  2. (2):

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

The coextension of $h:{\mathbb{E}_{k}}(A)\rightarrow B$ is

$h^{*}([a_{1},\,\ldots,\,a_{n}])\,=\,[h([a_{1}]),\,h([a_{1},a_{2}]),\,\ldots,\,h([a_{1},\ldots,a_{n}])].$

Pebbling comonad ${\mathbb{P}_{k}}$:

The universe of ${\mathbb{P}_{k}}(A)$ consists of non-empty words

$[(p_{1},a_{1}),\,\dots,\,(p_{n},a_{n})]$

of unrestricted (finite) length such that $a_{1},\dots,a_{n}\in A$ and
$p_{1},\dots,p_{n}$ are _pebble indexes_ , that is,
$p_{1},\dots,p_{n}\in\\{0,\dots,k-1\\}$. The counit $\varepsilon_{A}$ maps
$[(p_{1},a_{1}),\dots,(p_{n},a_{n})]$ to $a_{n}$.

For $n$-ary $R\in\sigma$, set $R^{{\mathbb{P}_{k}}(A)}(s_{1},\ldots,s_{n})$
iff:

  1. (1):

The $s_{i}$ are pairwise comparable in the prefix order on words.

  2. (2):

For $s_{i},s_{j}$ with $s_{i}$ a prefix word of $s_{j}$, the pebble index of
the last pair of $s_{i}$ does not reappear in the remaining elements of
$s_{j}$.

  3. (3):

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

For $h\colon{\mathbb{P}_{k}}(A)\rightarrow B$, the coextension $h^{*}$ acts on
words as:

$h^{*}([(p_{1},a_{1}),\ldots,(p_{n},a_{n})])\,=\,[(p_{1},h([a_{1}])),\ldots,(p_{n},h([a_{1},\ldots,a_{n}]))]$

We say that a signature $\sigma$ is a  _modal signature_ if it only has
relational symbols of arity one or two.

Modal comonad ${\mathbb{M}_{k}}$:

Defined over $\mathcal{R}_{*}(\sigma)$ for a modal signature $\sigma$, the
universe of ${\mathbb{M}_{k}}(A,a_{0})$ consists of paths in $A$ starting from
$a_{0}$, i.e. sequences

$a_{0}\xrightarrow{R_{1}}a_{1}\xrightarrow{R_{2}}a_{2}\xrightarrow{R_{3}}\ldots\xrightarrow{R_{n}}a_{n}$

such that $n\leq k$ and, for every $i$, $R_{i}\in\sigma$ and
$R_{i}^{A}(a_{i-1},a_{i})$. The counit and coextension act as for
${\mathbb{E}_{k}}$.

Given a sequence
$s^{\prime}=a_{0}\xrightarrow{R_{1}}\ldots\xrightarrow{R_{n-1}}a_{n-1}$ and
its extension $s$ by $a_{n-1}\xrightarrow{R_{n}}a_{n}$ in
${\mathbb{M}_{k}}(A,a_{0})$, then
$R_{n}^{{\mathbb{M}_{k}}(A,a_{0})}(s^{\prime},s)$ and
$R_{n}^{{\mathbb{M}_{k}}(A,a_{0})}$ only consists of such pairs. For a unary
$P\in\sigma$, $P^{{\mathbb{M}_{k}}(A,a_{0})}(s)$ iff $P^{A}(a_{n})$.

######  Theorem 2 ([ADW17, AS21]).

${\mathbb{E}_{k}}$, ${\mathbb{M}_{k}}$ and ${\mathbb{P}_{k}}$ are comonads in
Kleisli form.

The intuition for each of these comonads is that they encode the moves within
one structure during the corresponding model comparison game. We shall
introduce their mathematical properties as needed in later sections. See
[AS21] for detailed discussions of all three comonads.

##  3\. FVM theorems for positive existential fragments

For a game comonad $\mathbb{C}$, we introduce the following two relations on
structures:

  * •

$A\Rrightarrow_{\exists^{+}\mathbb{C}}B$ if there exists a morphism
$\mathbb{C}(A)\to B$.

  * •

$A\equiv_{\exists^{+}\mathbb{C}}B$ if $A\Rrightarrow_{\exists^{+}\mathbb{C}}B$
and $B\Rrightarrow_{\exists^{+}\mathbb{C}}A$.

It is a standard fact, formulated categorically in [AS21], that

$\displaystyle A\Rrightarrow_{\exists^{+}{\mathbb{E}_{k}}}B\quad\mbox{if and
only if}\quad$ for every positive existential sentence $\varphi$ of quantifier
$\displaystyle\text{depth at most $k$},\ A\models\varphi\text{ implies
}B\models\varphi.$

Therefore $A\equiv_{\exists^{+}{\mathbb{E}_{k}}}B$ if and only if structures
$A$ and $B$ agree on the quantifier depth $k$ fragment. Similarly,
$A\Rrightarrow_{\exists^{+}{\mathbb{P}_{k}}}B$ and
$A\equiv_{\exists^{+}{\mathbb{P}_{k}}}B$ correspond to the same relationships,
but for the $k$ variable fragment [ADW17].

######  Remark 3.

For conciseness, in this section, and Sections 4, 5 and 7, references to
first-order logic implicitly means the variant _without equality_ and with
infinite conjunctions and disjunctions, as is common in finite model theory.
We shall return to the variant with equality in Section 8. Note, however, that
typically logical equivalence of two _finite_ structures in a fragment of
logic with infinite conjunctions and disjunctions is the same as in the
corresponding fragment of first-order logic with finite conjunctions and
disjunctions.

We now consider FVM theorems for $\Rrightarrow_{\exists^{+}\mathbb{C}}$ and
$\equiv_{\exists^{+}\mathbb{C}}$, parametric in $\mathbb{C}$. To motivate our
abstract machinery, we first consider a warm-up example, that is nevertheless
sufficient to highlight the key ideas. For a signature $\sigma$, and
$\tau\subseteq\sigma$, the _$\tau$ -reduct_ of a $\sigma$-structure $A$ is the
$\tau$-structure on the same universe which interprets all the relation
symbols in $\tau$ as in $A$. We aim to show that equivalence in positive
existential first-order logic with quantifier rank ${\leq}\,k$ is preserved by
taking $\tau$-reducts of $\sigma$-structures for any $\tau\subseteq\sigma$. We
can view the $\tau$-reduct operation as a functor

$(-)|_{\tau}:\mathcal{R}(\sigma)\to\mathcal{R}(\tau)$

which sends a $\sigma$-structure to its $\tau$-reduct and a homomorphism of
$\sigma$-structures $f\colon A\to B$ is sent to the homomorphism
$f|_{\tau}\colon A|_{\tau}\to B|_{\tau}$ with the same underlying function as
$f$ has.

Observe that taking reducts admits an FVM theorem for the Ehrenfeucht–Fraïssé
comonad ${\mathbb{E}_{k}}$, viewed as a comonad on both $\mathcal{R}(\sigma)$
and $\mathcal{R}(\tau)$ categories. Given the logical reading of
$\Rrightarrow_{\exists^{+}{\mathbb{E}_{k}}}$, it is an easy observation that
$A\Rrightarrow_{\exists^{+}{\mathbb{E}_{k}}}B$ implies
$A|_{\tau}\Rrightarrow_{\exists^{+}{\mathbb{E}_{k}}}B|_{\tau}$. Indeed, if the
positive existential sentences of quantifier depth ${\leq}\,k$ in signature
$\sigma$ that are true in $A$ are also true in $B$, then the same must hold
for the positive existential sentences in the reduced signature $\tau$.

In this case, the FVM theorem can be proved using an ad-hoc argument about the
operation involved. However, to identify a general strategy, we would like to
prove this fact categorically. Given a morphism $f\colon{\mathbb{E}_{k}}(A)\to
B$ in $\mathcal{R}(\sigma)$ witnessing
$A\Rrightarrow_{\exists^{+}{\mathbb{E}_{k}}}B$, we wish to construct an
$\overline{f}\colon{\mathbb{E}_{k}}(A|_{\tau})\to B|_{\tau}$ witnessing
$A|_{\tau}\Rrightarrow_{\exists^{+}{\mathbb{E}_{k}}}B|_{\tau}$. To this end,
observe that there is a morphism of $\tau$-structures

$\kappa_{A}\colon{\mathbb{E}_{k}}(A|_{\tau})\to{\mathbb{E}_{k}}(A)|_{\tau}$

which sends a word $[a_{1},\dots,a_{n}]$ in ${\mathbb{E}_{k}}(A|_{\tau})$ to
the same word in ${\mathbb{E}_{k}}(A)|_{\tau}$. Therefore, $\overline{f}$ can
be computed as the composite

${\mathbb{E}_{k}}(A|_{\tau})\xrightarrow{\kappa_{A}}{\mathbb{E}_{k}}(A)|_{\tau}\xrightarrow{f|_{\tau}}B|_{\tau}.$
(3)

It is immediate that, since the definition of $\kappa_{A}$ was not specific to
$A$, there is such a morphism for every structure. Consequently, we obtain the
following trivial pair of FVM theorems:

$\displaystyle A\Rrightarrow_{\exists^{+}{\mathbb{E}_{k}}}B$
$\displaystyle\enspace\mbox{implies}\enspace
A|_{\tau}\Rrightarrow_{\exists^{+}{\mathbb{E}_{k}}}B|_{\tau}$ $\displaystyle
A\equiv_{\exists^{+}{\mathbb{E}_{k}}}B$
$\displaystyle\enspace\mbox{implies}\enspace
A|_{\tau}\equiv_{\exists^{+}{\mathbb{E}_{k}}}B|_{\tau}$

As this exercise demonstrates, all that is required to prove an FVM theorem
for the relations $\Rrightarrow_{\exists^{+}{\mathbb{E}_{k}}}$ or
$\equiv_{\exists^{+}{\mathbb{E}_{k}}}$, and a unary operation $H$, is to
define for every structure $A$ a morphism of $\sigma$-structures
$\kappa_{A}\colon{\mathbb{E}_{k}}(H(A))\rightarrow H({\mathbb{E}_{k}}(A))$. It
is not difficult to see that the same proof goes through when we parameterise
over the comonads involved and allow operations of arbitrary arity. We obtain
our first abstract FVM theorem. thmFVMpe Let
$\mathbb{C}_{1},\dots,\mathbb{C}_{n}$ and $\mathbb{D}$ be comonads on
categories $\mathcal{C}_{1},\dots,\mathcal{C}_{n}$, and $\mathcal{D}$
respectively, and

$H\colon\mathcal{C}_{1}\times\dots\times\mathcal{C}_{n}\to\mathcal{D}$

a functor. If for every
$A_{1}\in\mathrm{obj}(\mathcal{C}_{1}),\,\dots,\,A_{n}\in\mathrm{obj}(\mathcal{C}_{n})$
there exists a morphism

$\mathbb{D}(H(A_{1},\dots,A_{n}))\xrightarrow{\\!\\!\\!\overset{\kappa_{A_{1},\dots,A_{n}}}{\quad}\\!\\!\\!}H(\mathbb{C}_{1}(A_{1}),\dots,\mathbb{C}_{n}(A_{n}))$
(4)

in $\mathcal{D}$, then

$A_{1}\Rrightarrow_{\exists^{+}\mathbb{C}_{1}}B_{1},\;\ldots,\;A_{n}\Rrightarrow_{\exists^{+}\mathbb{C}_{n}}B_{n}$

implies

$H(A_{1},\dots,A_{n})\Rrightarrow_{\exists^{+}\mathbb{D}}H(B_{1},\dots,B_{n})$

The same result holds when replacing $\Rrightarrow_{\exists^{+}\mathbb{C}}$
with $\equiv_{\exists^{+}\mathbb{C}}$.

######  Proof 3.1.

Let $f_{i}\colon\mathbb{C}_{i}(A_{i})\to B_{i}$ be the morphism witnessing the
relation $A_{i}\Rrightarrow_{\exists^{+}\mathbb{C}_{i}}B_{i}$, for
$i\in\\{1,\dots,n\\}$. Since $H$ is a functor, the morphism $\overline{f}$
defined as the composition

$\mathbb{D}(H(A_{1},\dots,A_{n}))\xrightarrow{\ H(f_{1},\dots,f_{n})\ \circ\
\kappa_{A_{1},\dots,A_{n}}\ }H(B_{1},\dots,B_{n})$

witnesses the relation
$H(A_{1},\dots,A_{n})\Rrightarrow_{\exists^{+}\mathbb{D}}H(B_{1},\dots,B_{n})$.

The corresponding statement for $\equiv_{\exists^{+}\mathbb{C}}$ is obtained
by applying the same argument also to the collection of morphisms
$g_{i}\colon\mathbb{C}_{i}(B_{i})\to A_{i}$ that witness
$B_{i}\Rrightarrow_{\exists^{+}\mathbb{C}_{i}}A_{i}$, for
$i\in\\{1,\dots,n\\}$.

######  Remark 4 (Infinitary Operations).

For readability reasons, we state this as well as the other abstract FVM
theorems, such as Theorems 4.2 and 5.12 below, for operations of finite
arities only. Nevertheless, all these statements hold verbatim for infinitary
operations as well.

###  3.1. Examples

As our first simple application of Theorem 3, we obtain an FVM theorem showing
that $\Rrightarrow_{\exists^{+}{\mathbb{P}_{k}}}$ is preserved by taking the
disjoint union $A_{1}\uplus A_{2}$ of two $\sigma$-structures $A_{1}$,
$A_{2}$. The universe of $A_{1}\uplus A_{2}$ can be encoded as pairs $(i,a)$
where $i\in\\{1,2\\}$ and $a\in A_{i}$. For $r$-ary relation $R\in\sigma$, the
interpretation $R^{A_{1}\uplus A_{2}}$ is defined as

$R^{A_{1}\uplus A_{2}}((i_{1},a_{1}),\dots,(i_{r},a_{r}))$

if and only if there exists an $i$ such that for all $1\leq j\leq r$,
$i_{j}=i$ and $R^{A_{i}}(a_{1},\dots,a_{r})$. We define a morphism of
$\sigma$-structures

$\kappa_{A_{1},A_{2}}\colon{\mathbb{P}_{k}}(A_{1}\uplus
A_{2})\rightarrow{\mathbb{P}_{k}}A_{1}\uplus{\mathbb{P}_{k}}A_{2}$

which sends a word $s=[(p_{1},(i_{1},a_{1})),\dots,(p_{n},(i_{n},a_{n}))]$ in
${\mathbb{P}_{k}}(A_{1}\uplus A_{2})$ to the pair $(i_{n},\nu(s))$, where the
word $\nu(s)$ is the restriction of $s$ to the pairs $(p_{j},a_{j})$ such that
$i_{j}=i_{n}$. Since the definition of $\kappa_{A_{1},A_{2}}$ is not specific
to the structures $A_{1},A_{2}$, by Theorem 3, the following holds:

$\displaystyle
A_{1}\Rrightarrow_{\exists^{+}{\mathbb{P}_{k}}}B_{1}\enspace\mbox{and}\enspace
A_{2}\Rrightarrow_{\exists^{+}{\mathbb{P}_{k}}}B_{2}$
$\displaystyle\mbox{implies}\quad A_{1}\uplus
A_{2}\Rrightarrow_{\exists^{+}{\mathbb{P}_{k}}}B_{1}\uplus B_{2}$

Consequently, the same statement holds with
$\Rrightarrow_{\exists^{+}{\mathbb{P}_{k}}}$ replaced by
$\equiv_{\exists^{+}{\mathbb{P}_{k}}}$. The statement demonstrates that if
both $A_{1}$ and $B_{1}$, and $A_{2}$ and $B_{2}$, satisfy the same sentences
of the positive existential fragment of $k$-variable logic, then the disjoint
unions $A_{1}\uplus A_{2}$ and $B_{1}\uplus B_{2}$ also satisfy the same
sentences of that fragment. Similar $\kappa$ morphisms can be defined to
demonstrate that $\Rrightarrow_{\exists^{+}{\mathbb{P}_{k}}}$,
$\equiv_{\exists^{+}{\mathbb{P}_{k}}}$ and also
$\Rrightarrow_{\exists^{+}{\mathbb{E}_{k}}}$ and
$\equiv_{\exists^{+}{\mathbb{E}_{k}}}$ are preserved by taking disjoint unions
of _arbitrary_ sets of $\sigma$-structures. Even in the case of relatively
simple operations on structures, it may be the case that logical equivalence
is not preserved. [Counterexample] For the modal fragment, a positive modal
formula is one without negation or the $\Box$ modality. As shown in [AS21],
for pointed structures

$A=(A,a)\enspace\mbox{and}\enspace B=(B,b)$

in a modal signature, $A\Rrightarrow_{\exists^{+}{\mathbb{M}_{k}}}B$ if and
only if for every positive modal formula $\varphi$ of modal depth at most $k$,
$A\models\varphi$ implies $B\models\varphi$, and therefore
$A\equiv_{\exists^{+}{\mathbb{M}_{k}}}B$ if and only if the two structures
agree on positive modal formulae with modal depth bounded by $k$.

Categorically, the disjoint union of $\sigma$-structures is their _coproduct_
in $\mathcal{R}(\sigma)$. The formal definition of coproducts is unimportant
for this example, but we note that coproduct of two _pointed_
$\sigma$-structures $(A_{1},a_{1})+(A_{2},a_{2})$ in $\mathcal{R}_{*}(\sigma)$
is a quotient of their disjoint union, where the distinguished points $a_{1}$
and $a_{2}$ are identified. Unlike with ${\mathbb{E}_{k}}$ and
${\mathbb{P}_{k}}$, the relations $\Rrightarrow_{\exists^{+}{\mathbb{M}_{k}}}$
and $\equiv_{\exists^{+}{\mathbb{M}_{k}}}$ are _not_ preserved by this
operation on pointed $\sigma$-structures, essentially because the two
components can interact. This shows that although coproduct FVM theorems are
relatively simple, it is by no means automatic that they will hold.

For every binary relation $R$ in a modal signature $\sigma$, there is an
operation $(A_{1},a_{1})\stackrel{{\scriptstyle R}}{{\vee}}(A_{2},a_{2})$
which combines the two pointed structures by adding a new initial point
$\star$ with $R$-transitions to $a_{1}$ and $a_{2}$. Operations such as this
are commonly found when modelling concurrent systems with process calculi
[Sti01, Ros10]. Intuitively this operation avoids the interactions that caused
problems in Counterexample 3.1.

There is a morphism of pointed $\sigma$-structures

$\kappa_{(A_{1},a_{1}),(A_{2},a_{2})}\colon\mathbb{M}_{k+1}((A_{1},a_{1})\stackrel{{\scriptstyle
R}}{{\vee}}(A_{2},a_{2}))\rightarrow{\mathbb{M}_{k}}((A_{1},a_{1}))\stackrel{{\scriptstyle
R}}{{\vee}}{\mathbb{M}_{k}}((A_{2},a_{2}))$

All sequences in the domain are of the form

$*\xrightarrow{R}(i,c_{0})\xrightarrow{R_{1}}\ldots\xrightarrow{R_{n}}(i,c_{n}),$

with $i\in\\{1,2\\}$ and each $(i,c_{j})\in A_{1}\uplus A_{2}$ in the same
component. Then, $\kappa_{(A_{1},a_{1}),(A_{2},a_{2})}$ must preserve the
distinguished element, and for sequences of length greater than one it sends
$*\xrightarrow{R}(i,c_{0})\xrightarrow{R_{1}}\ldots\xrightarrow{R_{n}}(i,c_{n})$
to $(i,c_{0}\xrightarrow{R_{1}}\ldots\xrightarrow{R_{n}}c_{n})$. Applying
Theorem 3 yields the FVM theorem:

$\displaystyle(A_{1},a_{1})\Rrightarrow_{\exists^{+}{\mathbb{M}_{k}}}(B_{1},b_{1})\enspace\mbox{and}\enspace(A_{2},a_{2})\Rrightarrow_{\exists^{+}{\mathbb{M}_{k}}}(B_{2},b_{2})$
$\displaystyle\mbox{implies}\quad(A_{1},a_{1})\stackrel{{\scriptstyle
R}}{{\vee}}(A_{2},a_{2})\Rrightarrow_{\exists^{+}\mathbb{M}_{k+1}}(B_{1},b_{1})\stackrel{{\scriptstyle
R}}{{\vee}}(B_{2},b_{2})$

Notice that the resource index actually _increases_ from $k$ to $k+1$ because
of the shape of $\kappa$.

A nice feature of the generality of Theorem 3 is that for different comonads
$\mathbb{C}$ and $\mathbb{D}$ over the same category $\mathcal{C}$, a natural
transformation between the functors $\mathbb{C}\Rightarrow\mathbb{D}$ or, more
generally, a collection of morphisms

$\\{\kappa_{A}\colon\mathbb{D}A\rightarrow\mathbb{C}A\mid
A\in\mathrm{obj}(\mathcal{C})\\}$

can be seen as instances of (4), with $H$ equal to the identity functor
${I\mkern-1.0mud}\colon\mathcal{C}\to\mathcal{C}$. This allows us to provide
semantic translations for the logics captured by game comonads, a question
that had not previously been addressed. For example, if we consider
$\mathbb{P}_{2}$ as a comonad over $\mathcal{R}_{*}(\sigma)$ where
$\mathbb{P}_{2}(A,a_{0})$ has distinguished point $[(0,a_{0})]$, then for
every $k\in\mathbb{N}$ and object $(A,a_{0})$ we define a morphism of pointed
$\sigma$-structures

$\kappa_{(A,a_{0})}\colon{\mathbb{M}_{k}}(A,a_{0})\rightarrow\mathbb{P}_{2}(A,a_{0})$

which sends the sequence of transitions

$a_{0}\xrightarrow{R_{1}}\ldots\xrightarrow{R_{n-1}}a_{n-1}\xrightarrow{R_{n}}a_{n}$

in ${\mathbb{M}_{k}}(A,a_{0})$ to the word in $\mathbb{P}_{2}(A,a_{0})$ where
elements are labeled by the parity of their position

$[(0,a_{0}),(1,a_{1}),\dots,(n\bmod 2,a_{n})].$

Applying Theorem 3 yields the well-known fact that structures which satisfy
the same sentences of the positive existential fragment of two-variable logic
must also satisfy the same positive modal formulas for any modal depth $k$

$\displaystyle(A,a_{0})\equiv_{\exists^{+}\mathbb{P}_{2}}(B,b_{0})$
$\displaystyle\mbox{implies}\quad(\forall k\in\mathbb{N}.\ \
(A,a_{0})\equiv_{\exists^{+}{\mathbb{M}_{k}}}(B,b_{0})).$

Similarly, there exist morphisms
$\kappa_{A}\colon{\mathbb{E}_{k}}A\rightarrow{\mathbb{P}_{k}}A$ for every $A$
in $\mathcal{R}(\sigma)$ where $[a_{1},\dots,a_{n}]$ with $n\leq k$ is sent to
$[(0,a_{1}),\dots(n-1,a_{n})]$ demonstrating that
$\Rrightarrow_{\exists^{+}{\mathbb{P}_{k}}}$ refines
$\Rrightarrow_{\exists^{+}{\mathbb{E}_{k}}}$.

##  4\. FVM theorems for counting logic

We now consider another relationship induced by a game comonad. To do so, we
first introduce one of the two standard categories associated with any
comonad.

###  4.1. Kleisli category

Given a comonad $\mathbb{C}$ on a category $\mathcal{C}$, the _Kleisli
category_ [Kle65] $\mathsf{Kl}(\mathbb{C})$ for $\mathbb{C}$ on $\mathcal{C}$
is a category which

  * •

has the same objects as $\mathcal{C}$, and

  * •

the morphisms of type $A\rightarrow B$ in $\mathsf{Kl}(\mathbb{C})$ are the
morphisms of type $\mathbb{C}(A)\to B$ in $\mathcal{C}$. To avoid ambiguity,
we shall write $f:A\to_{\mathbb{C}}B$ if we intend $f$ to be understood as a
Kleisli morphism.

  * •

For an object $A$, the identity morphism $A\to_{\mathbb{C}}A$ is the counit
component $\varepsilon_{A}:\mathbb{C}(A)\rightarrow A$.

  * •

The composite of morphisms $f\colon A\to_{\mathbb{C}}B$ and $g\colon
B\to_{\mathbb{C}}C$ is given by $g\circ f^{*}$, where we recall
$f^{*}:\mathbb{C}(A)\rightarrow\mathbb{C}(B)$ is the coextension of
$f\colon\mathbb{C}(A)\to B$. As composition is different to that in the base
category, we use the distinct notation $g\mathbin{\bullet}f$ for the composite
of $f$ and $g$.

The axioms for a comonad in Kleisli form ensure that this is a well-defined
category. Notice that the morphisms in the Kleisli category are exactly those
that were important for positive existential fragments in Section 3.

The motivation for the Kleisli construction is that there is an obvious
forgetful functor
$U_{\mathbb{C}}:\mathsf{Kl}(\mathbb{C})\rightarrow\mathcal{C}$, and this
functor has an identity on objects right adjoint _cofree functor_
$F_{\mathbb{C}}:\mathcal{C}\rightarrow\mathsf{Kl}(\mathbb{C})$, and this
adjunction induces the original comonad.

As with any category, we can consider the isomorphisms in
$\mathsf{Kl}(\mathbb{C})$. We shall write

$A\equiv_{\\#\mathbb{C}}B$

if structures $A$ and $B$ are isomorphic in the Kleisli category. For finite
structures, the relations $A\equiv_{\\#{\mathbb{E}_{k}}}B$ and
$A\equiv_{\\#{\mathbb{P}_{k}}}B$ correspond to equivalence in counting logic
[ADW17, AS21]. The ideas of Theorem 3 can be extended to establish an FVM
theorem for counting fragments and the $\equiv_{\\#\mathbb{C}}$ relation. All
that is required is to impose extra conditions on the collection of morphisms
(4). Furthermore, these extra conditions turn out to be those of the well-
known Kleisli laws related to lifting functors to Kleisli categories [MM07].

To motivate our comonadic method, we return to the minimal reduct example from
Section 3. We can show that $A\equiv_{\\#{\mathbb{E}_{k}}}B$ implies
$A|_{\tau}\equiv_{\\#{\mathbb{E}_{k}}}B|_{\tau}$, via a similar ad-hoc
argument to before. In our setting, we wish to establish that, for mutually
inverse morphisms $f\colon A\to_{{\mathbb{E}_{k}}}B$ and $g\colon
B\to_{{\mathbb{E}_{k}}}A$ in $\mathsf{Kl}({\mathbb{E}_{k}})$, the composites
$f|_{\tau}\circ\kappa_{A}$ and $g|_{\tau}\circ\kappa_{B}$, constructed as in
(3), are also mutually inverse in the Kleisli category. In the following we
analyse the abstract setting in which the relation $\equiv_{\\#\mathbb{C}}$ is
defined and derive a general result, similar to Theorem 3.

###  4.2. Kleisli laws

Akin to our motivating example, we assume a unary operation
$H:\mathcal{C}\rightarrow\mathcal{D}$, comonads
$(\mathbb{C},\varepsilon^{\mathbb{C}},(-)^{*})$ on $\mathcal{C}$ and
$(\mathbb{D},\varepsilon^{\mathbb{D}},(-)^{*})$ on $\mathcal{D}$, and also a
collection of morphisms

$\\{\kappa_{A}\colon\mathbb{D}H(A)\to H\mathbb{C}(A)\mid
A\in\mathrm{obj}(\mathcal{C})\\},$

as in Theorem 3. We wish to find conditions on this collection of morphisms
ensuring that $A\equiv_{\\#\mathbb{C}}B$ implies
$H(A)\equiv_{\\#\mathbb{D}}H(B)$. Rephrasing, we require axioms such that if
$f\colon A\to_{\mathbb{C}}B$ and $g\colon B\to_{\mathbb{C}}A$ are mutually
inverse, then the composites

$H(f)\circ\kappa_{A}\colon H(A)\to_{\mathbb{D}}H(B)\quad\mbox{and}\quad
H(g)\circ\kappa_{B}\colon H(B)\to_{\mathbb{D}}H(A)$

are also mutually inverse. To do so, we observe that if both

$H(\varepsilon_{A})\circ\kappa_{A}=\varepsilon_{H(A)}$ (5)

and

$H(f^{*})\circ\kappa_{A}=\kappa_{B}\circ(H(f)\circ\kappa_{A})^{*}$ (6)

then, from $g\mathbin{\bullet}f=\mathrm{id}$ in $\mathsf{Kl}(\mathbb{D})$
(i.e. $g\circ f^{*}=\varepsilon_{A}$), we obtain that

$\displaystyle(H(g)\circ\kappa_{B})\mathbin{\bullet}(H(f)\circ\kappa_{A})$
$\displaystyle=H(g)\circ\kappa_{B}\circ(H(f)\circ\kappa_{A})^{*}$ definition
of $\mathbin{\bullet}$ $\displaystyle=H(g)\circ H(f^{*})\circ\kappa_{A}$ (6)
$\displaystyle=H(g\circ f^{*})\circ\kappa_{A}$ functoriality
$\displaystyle=H(\varepsilon_{A})\circ\kappa_{A}$ assumption
$\displaystyle=\varepsilon_{H(A)}:\mathbb{D}(H(A))\to H(A)$ (5)

and, similarly, $f\mathbin{\bullet}g=\mathrm{id}$ implies that

$(H(f)\circ\kappa_{A})\mathbin{\bullet}(H(g)\circ\kappa_{B})$

equals to identity in $\mathsf{Kl}(\mathbb{D})$. In fact, equations (5) and
(6) are equivalent to requiring that the $\kappa_{A}$ constitute a natural
transformation $\kappa:\mathbb{D}\circ H\Rightarrow H\circ\mathbb{C}$ making
the following two diagrams commute:

${\mathbb{D}\circ
H}$${H\circ\mathbb{C}}$${H}$$\scriptstyle{\kappa}$$\scriptstyle{\varepsilon_{H}}$$\scriptstyle{H\varepsilon}$
${\mathbb{D}\circ H}$${\mathbb{D}^{2}\circ H}$${\mathbb{D}\circ
H\circ\mathbb{C}}$${H\circ\mathbb{C}}$${H\circ\mathbb{C}^{2}}$$\scriptstyle{\kappa}$$\scriptstyle{\delta_{H}}$$\scriptstyle{\mathbb{D}\kappa}$$\scriptstyle{\kappa_{\mathbb{C}}}$$\scriptstyle{H\delta}$
(7)

Such a $\kappa$ is referred to as a _Kleisli law_ [MM07].

######  Lemma 5.

A collection of morphisms $\\{\kappa_{A}\\}$ satisfies equations (5) and (6)
for every $f\colon\mathbb{C}(A)\to B$ iff $\kappa$ is a Kleisli law.

######  Proof 4.1.

For the left to right implication, $\kappa$ is natural since, for any $g\colon
A\to B$, we set
$f=\mathbb{C}(A)\xrightarrow{\varepsilon_{A}}A\xrightarrow{g}B$ and observe
that $H(\mathbb{C}(g))=H(f^{*})$ and
$\mathbb{D}(H(g))=(H(g)\circ\varepsilon_{H(A)})^{*}=(H(f)\circ\kappa)^{*}$ by
(5). Naturality then follows from (6). Commutativity of the oblong in (7)
follows by setting $f=\mathbb{C}(A)\xrightarrow{\mathrm{id}}\mathbb{C}(A)$. We
then have $(H(f)\circ\kappa_{A})^{*}=\mathbb{D}(\kappa_{A})\circ\delta_{H(A)}$
and
$\kappa_{A}\circ\mathbb{D}(\kappa_{A})\circ\delta_{H(A)}=H(f^{*})\circ\kappa_{A}=H(\delta_{A})\circ\kappa_{A}$
from which the result follows by (5).

Conversely, for an $f\colon\mathbb{C}(A)\to B$, by the oblong law in (7) and
naturality of $\kappa$,
$H(f^{*})\circ\kappa_{A}=H(\mathbb{C}(f))\circ\kappa_{\mathbb{C}(A)}\circ\mathbb{D}(\kappa_{A})\circ\delta_{H(A)}=\kappa_{B}\circ\mathbb{D}(H(f))\circ\mathbb{D}(\kappa_{A})\circ\delta_{H(A)}=\kappa_{B}\circ(H(f)\circ\kappa_{A})^{*}$.

######  Remark 6.

Kleisli laws for monads given by a collection of morphisms satisfying (5) and
(6) appeared in the study of relative monads [Ahr12, Ahr15], under the name
_colax morphisms_. Kleisli laws correspond precisely to liftings of the
operation $H\colon\mathcal{C}\to\mathcal{D}$ to operations
$\mathsf{Kl}(\mathbb{C})\to\mathsf{Kl}(\mathbb{D})$ commuting with the cofree
functors $\mathcal{C}\to\mathsf{Kl}(\mathbb{C})$ and
$\mathcal{D}\to\mathsf{Kl}(\mathbb{D})$. See for example [Mul93, Jac94].
Furthermore, a Kleisli law $\kappa:\mathbb{C}\Rightarrow\mathbb{D}$ with
respect to the identity functor (as the operation) is the same thing as a
_comonad morphism_.

We will typically be interested in operations of arity greater than one, so we
immediately extend our definitions.

######  Remark 7 (Notation).

For a set $I$, and family of categories $\\{\mathcal{C}_{i}\\}_{i\in I}$, we
shall write $\vv{A_{i}}\mkern 1.0mu$ for a family of objects, with each
$A_{i}\in\mathcal{C}_{i}$, and similarly $\vv{f_{i}}\mkern 1.0mu$ for families
of morphisms. These form the _product category_ $\prod_{i\in
I}\mathcal{C}_{i}$, with composition and identities defined componentwise.
Given a family of comonads
$\mathbb{C}_{i}:\mathcal{C}_{i}\rightarrow\mathcal{C}_{i}$, they induce a
comonad $\prod_{i}\mathbb{C}_{i}$ on the product category, again
componentwise.

Using this notation, we define the $n$-ary version of the axioms from Lemma 5.
_Kleisli laws_ for an $n$-ary operation $H$ are the natural transformations
$\kappa\colon\mathbb{D}\circ H\Rightarrow H\circ\prod_{i}\mathbb{C}_{i}$ such
that the following diagrams commute:

  1. (K1)

${\mathbb{D}\circ
H}$${H\circ\prod_{i}\mathbb{C}_{i}}$${H}$$\scriptstyle{\kappa}$$\scriptstyle{\varepsilon_{H}}$$\scriptstyle{H(\prod_{i}\varepsilon)}$

  2. (K2)

${\mathbb{D}\circ H}$${\mathbb{D}^{2}\circ H}$${\mathbb{D}\circ
H\circ\prod_{i}\mathbb{C}_{i}}$${H\circ\prod_{i}\mathbb{C}_{i}}$${H\circ\prod_{i}\mathbb{C}^{2}_{i}}$$\scriptstyle{\kappa}$$\scriptstyle{\delta_{H}}$$\scriptstyle{\mathbb{D}\kappa}$$\scriptstyle{\kappa}$$\scriptstyle{H(\prod_{i}\delta)}$

In fact, n-ary Kleisli laws are a special case of ordinary (unary) Kleisli
laws, as will be shown in Lemma 8.

For a family of comonads
$\mathbb{C}_{i}:\mathcal{C}_{i}\rightarrow\mathcal{C}_{i}$, we will say that a
functor
$H^{\prime}:\prod_{i}\mathsf{Kl}(\mathbb{C}_{i})\rightarrow\mathsf{Kl}(\mathbb{D}_{i})$
is a _Kleisli lifting_ of functor
$H:\prod_{i}\mathcal{C}_{i}\rightarrow\mathcal{D}$ if the following diagram
commutes:

${\prod_{i}\mathsf{Kl}(\mathcal{C}_{i})}$${\mathsf{Kl}(\mathbb{D})}$${\prod_{i}\mathbb{C}_{i}}$${\mathcal{D}}$$\scriptstyle{H^{\prime}}$$\scriptstyle{H}$$\scriptstyle{\prod_{i}F_{\mathbb{C}_{i}}}$$\scriptstyle{F_{\mathbb{D}}}$
(8)

######  Lemma 8.

Given a family of comonads
$\mathbb{C}_{i}:\mathcal{C}_{i}\rightarrow\mathcal{C}_{i}$:

  1. (1)

The Kleisli construction commutes with products, in that the following
equation holds

$\mathsf{Kl}(\prod\nolimits_{i}\mathbb{C}_{i})=\prod\nolimits_{i}\mathsf{Kl}(\mathbb{C}_{i})$

  2. (2)

The forgetful functor and cofree functors of the product comonad

$U_{\prod_{i}\mathbb{C}_{i}}:\mathsf{Kl}(\prod\nolimits_{i}\mathbb{C}_{i})\rightarrow\prod\nolimits_{i}\mathcal{C}_{i}\qquad
F_{\prod_{i}\mathbb{C}_{i}}:\prod\nolimits_{i}\mathcal{C}_{i}\rightarrow\mathsf{Kl}(\prod\nolimits_{i}\mathbb{C}_{i})$

are given by the product $\prod_{i}U_{\mathbb{C}_{i}}$ of forgetful and
product $\prod_{i}F_{\mathbb{C}_{i}}$ of cofree functors, respectively.

  3. (3)

An n-ary Kleisli laws of type $\mathbb{D}\circ H\Rightarrow
H\circ\prod_{i}\mathbb{C}_{i}$ is the same thing as a (unary) Kleisli law
involving the product comonad $\prod_{i}\mathbb{C}_{i}$.

  4. (4)

n-ary Kleisli laws bijectively correspond to Kleisli liftings of $H$.

######  Proof 4.2.

Items 1 and 2 are routine calculations from the definitions. Item 3 follows
directly from the definitions, and so we can reduce the bijective relationship
between n-ary Kleisli laws and Kleisli liftings to the well-known unary case.
See for example [Mul93]. This establishes item 4.

The argument presented for a unary opereration generalises smoothly to
operations of any arity, yielding an FVM theorem for counting fragments.
thmFVMcounting Let $\mathbb{C}_{1},\dots,\mathbb{C}_{n}$ and $\mathbb{D}$ be
comonads on categories $\mathcal{C}_{1},\dots,\mathcal{C}_{n}$ and
$\mathcal{D}$, respectively, and
$H\colon\prod_{i}\mathcal{C}_{i}\to\mathcal{D}$ a functor. If there exists a
Kleisli law of type $\mathbb{D}\circ H\Rightarrow
H\circ\prod\nolimits_{i}\mathbb{C}_{i}$ then

$A_{1}\equiv_{\\#\mathbb{C}_{1}}B_{1}\;\ldots,\;A_{n}\equiv_{\\#\mathbb{C}_{n}}B_{n}$

implies

$H(A_{1},\dots,A_{n})\;\equiv_{\\#\mathbb{D}}\;H(B_{1},\dots,B_{n}).$

######  Proof 4.3.

Assume $A_{1}\equiv_{\\#\mathbb{C}_{1}}B_{1}$, …,
$A_{n}\equiv_{\\#\mathbb{C}_{n}}B_{n}$ or, equivalently,

$F_{\mathbb{C}_{1}}(A_{1})\cong F_{C_{1}}(B_{1}),\enspace\ldots,\enspace
F_{\mathbb{C}_{n}}(A_{n})\cong F_{\mathbb{C}_{n}}(B_{n}).$

The assumed Kleisli law induces a Kleisli lifting
$H^{\prime}\colon\prod_{i}\mathsf{Kl}(\mathbb{C}_{i})\rightarrow\mathsf{Kl}(\mathbb{D}_{i})$
by item 4 of Lemma 8, which by functoriality implies

$H^{\prime}(F_{\mathbb{C}_{1}}(A_{1}),\ldots,F_{\mathbb{C}_{n}}(A_{n}))\cong
H^{\prime}(F_{C_{1}}(B_{1}),\ldots,F_{\mathbb{C}_{n}}(B_{n})).$

By the commutativity of (8) we have
$F_{\mathbb{D}}(H(A_{1},\ldots,A_{n}))\cong
F_{\mathbb{D}}(H(B_{1},\ldots,B_{n}))$, which encodes the required property.

###  4.3. Examples

The collection of $\kappa$ morphisms described in each of Examples 3.1, 3.1
and 3.1 of Section 3.1 are natural and satisfy axioms (K1) and (K2).
Therefore, by applying Theorem 4.2 to the Kleisli laws in Examples 3.1 and 3.1
we have that $\equiv_{\\#{\mathbb{E}_{k}}}$ and $\equiv_{\\#{\mathbb{P}_{k}}}$
are preserved by taking coproducts of structures and the merge operation maps
$\equiv_{\\#{\mathbb{M}_{k}}}$ to $\equiv_{\\#\mathbb{M}_{k+1}}$. Recalling
Remark 6, by applying Theorem 4.2 to the comonad morphism in Example 3.1 we
have that for all $k\in\mathbb{N}$, $\equiv_{\\#\mathbb{P}_{2}}$ refines
$\equiv_{\\#{\mathbb{M}_{k}}}$, and $\equiv_{\\#{\mathbb{P}_{k}}}$ refines
$\equiv_{\\#{\mathbb{E}_{k}}}$.

[Cospectrality] Two graphs $G$ and $H$ are _cospectral_ if the adjacency
matrices of $G$ and $H$ have the same multiset of eigenvalues. We shall use
Theorem 4.2 to strengthen a result in [DSZ17] showing that equivalence in
3-variable counting logic _with equality_ implies cospectrality.

Since cospectrality is a notion on graphs, we move to the full subcategory of
loopless undirected graphs in signature $\sigma=\\{E\\}$ where $E$ is a binary
edge relation. The comonad ${\mathbb{P}_{k}}$ restricts to this category and
we also consider a comonad $\mathtt{Cos}$ defined in [AJP22, Section 3] which
characterizes cospectrality, in that $G\equiv_{\\#\mathtt{Cos}}H$ is
equivalent to $G$ and $H$ being cospectral. The universe of $\mathtt{Cos}(G)$
can be encoded as pairs $(c,v_{i})$ where $c$ is a closed walk
$v_{0}\xrightarrow{E}v_{1}\xrightarrow{E}\ldots\xrightarrow{E}v_{n}\xrightarrow{E}v_{0}$
that passes through $v_{i}$. Two pairs $(c,v_{i}),(c^{\prime},v_{j})$ are
adjacent in $\mathtt{Cos}(G)$ if $c=c^{\prime}$ and $v_{i}$ is adjacent to
$v_{j}$ in the closed walk $c$. The counit $\varepsilon_{G}$ maps $(c,v_{i})$
to $v_{i}$. For $h\colon\mathtt{Cos}(G)\rightarrow H$, the coextension $h^{*}$
maps the pair $(c,v_{i})$ with $c$ being the closed walk
$v_{0}\xrightarrow{E}v_{1}\xrightarrow{E}\ldots\xrightarrow{E}v_{n}\xrightarrow{E}v_{0}$
to $(d,h(c,v_{i}))$ where $d$ is the closed walk
$h(c,v_{0})\xrightarrow{E}h(c,v_{1})\xrightarrow{E}\ldots\xrightarrow{E}h(c,v_{n})\xrightarrow{E}h(c,v_{0})$.

We define a comonad morphism $\kappa\colon\mathtt{Cos}(G)\to\mathbb{P}_{3}(G)$
where $(c,v_{i})$ is mapped to the word

$[(2,v_{0}),(1,v_{1}),(0,v_{2}),(1,v_{3}),\dots,(i\bmod 2,v_{i})].$

Recalling Remark 6, we apply Theorem 4.2, deducing that
$\equiv_{\\#\mathbb{P}_{3}}$ implies $\equiv_{\\#\mathtt{Cos}}$. Since
$\equiv_{\\#\mathbb{P}_{3}}$ captures equivalence in 3-variable counting logic
_without equality_ and $\equiv_{\\#\mathtt{Cos}}$ captures cospectrality, we
have avoided the need for equality in the logic. This fact is also a
consequence of [DJR21, Theorem 32] and the original theorem of Dawar,
Severini, and Zapata [DSZ17]. However, the same reasoning allows us to define
a comonad morphism $\mathtt{Cos}\Rightarrow\mathbb{PR}_{3}$ where
$\mathbb{PR}_{3}$ is the pebble-relation comonad from [MS22], capturing the
restricted conjunction fragment of $3$-variable counting logic. The universe
of $\mathbb{PR}_{3}(G)$ consists of pairs $(s,i)$ with $s\in\mathbb{P}_{3}(G)$
is a sequence of length $n$ and $i\in\\{0,1,\dots,n\\}$ is an index into the
sequence $s$. In this case, $(c,v_{i})$ is mapped to the pair $(s,i)$ where
$s=\kappa(c,v_{n})$. Intuitively, $s$ enumerates the entire closed walk $c$
and the index $i$ picks out $v_{i}$ in this walk. This proves a genuine
strengthening of the previous result.

The forthcoming thesis [Sha24] takes a look at the quantum monad
$\mathbf{Q}_{d}$ from [ABdSZ17] on categories of structures with a
distinguished ‘commeasurablity’ relation. For each $d>0$, $\mathbf{Q}_{d}(A)$
is a structure on $d$-dimensional projector-valued measurements of $A$ and is
used for modeling perfect quantum strategies in a non-local homomorphism game.
In [Sha24], it is showed that there is a Kleisli law
${\mathbb{E}_{k}}\circ\mathbf{Q}_{d}\Rightarrow\mathbf{Q}_{d}\circ{\mathbb{E}_{k}}$,
giving us that the equivalence in the counting fragment
$A\equiv_{\\#{\mathbb{E}_{k}}}B$ implies
$\mathbf{Q}_{d}(A)\equiv_{\\#{\mathbb{E}_{k}}}\mathbf{Q}_{d}(B)$.

##  5\. FVM theorems for the full logic

In Sections 3 and 4 we described FVM theorems for the equivalence relations
$\equiv_{\exists^{+}\mathbb{C}}$ and $\equiv_{\\#\mathbb{C}}$, typically
expressing logical equivalence for the positive existential and counting logic
variants. To do the same for the full logic requires us to move from the
Kleisli category to the richer setting of the _Eilenberg–Moore category of
coalgebras_.

For a comonad $\mathbb{C}$ on $\mathcal{C}$, a pair $(A,\alpha)$ where
$\alpha\colon A\to\mathbb{C}(A)$ is a morphism in $\mathcal{C}$ is a
_$\mathbb{C}$ -coalgebra_ or simply just _coalgebra_ if the following two
diagrams commute.

${A}$${\mathbb{C}(A)}$${A}$$\scriptstyle{\alpha}$$\scriptstyle{\mathrm{id}}$$\scriptstyle{\varepsilon_{A}}$
${A}$${\mathbb{C}(A)}$${\
\mathbb{C}(A)}$${\mathbb{C}(\mathbb{C}(A))}$$\scriptstyle{\alpha}$$\scriptstyle{\alpha}$$\scriptstyle{\delta_{A}}$$\scriptstyle{\mathbb{C}(\alpha)}$
(9)

A _morphism of coalgebras_ $f\colon(A,\alpha)\to(B,\beta)$ is a morphism
$f\colon A\to B$ such that $\beta\circ f=\mathbb{C}(f)\circ\alpha$. We write
$\mathsf{EM}(\mathbb{C})$ for the Eilenberg–Moore category of coalgebras of
$\mathbb{C}$.

The original motivation for the Eilenberg-Moore construction is that there is
an obvious forgetful functor
$U^{\mathbb{C}}:\mathsf{EM}(\mathbb{C})\rightarrow\mathcal{C}$, mapping
$(A,\alpha)$ to $A$, and it has a right adjoint _cofree coalgebra_ functor
$F^{\mathbb{C}}:\mathcal{C}\rightarrow\mathsf{EM}(\mathbb{C})$, such that the
adjunction $U^{\mathbb{C}}\dashv F^{\mathbb{C}}$ induces the comonad
$\mathbb{C}$. We will need the cofree construction in later developments.
Concretely its action on objects is
$F^{\mathbb{C}}(A)=(\mathbb{C}(A),\delta_{A})$.

######  Remark 9.

A coalgebra $(A,\alpha)$ of any of the game comonads defined in Section 2.2 is
endowed with a preorder $\sqsubseteq_{\alpha}$, where $x\sqsubseteq_{\alpha}y$
whenever the word $\alpha(x)$ is a prefix of $\alpha(y)$. A _forest order_ is
a poset in which the set of predecessors of any element in a finite chain. It
follows from the axioms in (9) that $\sqsubseteq_{\alpha}$ is a forest order
on the universe. Furthermore, one can check that $\sqsubseteq_{\alpha}$ is
_compatible_ with the relational structure of $A$. This means that
$R^{A}(a_{1},\dots,a_{n})$ implies that for every $i,j$ either
$a_{i}\sqsubseteq_{\alpha}a_{j}$ or $a_{j}\sqsubseteq_{\alpha}a_{i}$.

In fact $\mathsf{EM}({\mathbb{E}_{k}})$ is equivalent to the category of
$\sigma$-structures endowed with a compatible forest order of depth
${\leq}\,k$. Similar characterisations of the categories
$\mathsf{EM}({\mathbb{P}_{k}})$ and $\mathsf{EM}({\mathbb{M}_{k}})$ can be
made as well, cf. [AS21, Section 9].

We are now almost ready to define the relation $\equiv_{\mathbb{C}}$. Given
$A,B\in\mathcal{C}$, define $A\equiv_{\mathbb{C}}B$ if there exists a span of
_open pathwise-embeddings_

$F^{\mathbb{C}}(A)\leftarrow Z\rightarrow F^{\mathbb{C}}(B).$

We postpone the definition of open pathwise-embeddings to Section 5.3.

In terms of our example comonads, $A\equiv_{{\mathbb{E}_{k}}}B$ and
$A\equiv_{{\mathbb{P}_{k}}}B$ correspond to agreement on first-order sentences
of $k$-bounded quantifier depth and variable count respectively [AS21].
Similarly, $(A,a)\equiv_{{\mathbb{M}_{k}}}(B,b)$ characterises agreement on
modal formulae of modal depth at most $k$.

Returning again to the example of reducts, showing the trivial fact that
$A\equiv_{{\mathbb{E}_{k}}}B$ implies
$A|_{\tau}\equiv_{{\mathbb{E}_{k}}}B|_{\tau}$ in our setting suggests the
strategy:

  1. (1)

Lift an $n$-ary operation $H$ to the level of coalgebras, in a manner that
commutes with the construction $F^{\mathbb{C}}(-)$ of cofree coalgebras.

  2. (2)

Check that open pathwise-embeddings are preserved by the lifted operation.

Tackling step 1 is the topic of Section 5.1. Step 2 is the subject of the
subsequent Section 5.3.

###  5.1. Lifting operations to coalgebras

Here we focus on the task of lifting a given operation to the level of
coalgebras. By a _lifting_ of a functor
$H:\prod_{i}\mathcal{C}_{i}\rightarrow\mathcal{D}$ we mean a functor
$\widehat{H}:\prod_{i}\mathsf{EM}(\mathbb{C}_{i})\rightarrow\mathsf{EM}(\mathbb{D})$
such that the following diagram commutes up to isomorphism:

${\prod_{i}\mathsf{EM}(\mathbb{C}_{i})}$${\mathsf{EM}(\mathbb{D})}$${\prod_{i}\mathcal{C}_{i}}$${\mathcal{D}}$$\scriptstyle{\widehat{H}}$$\scriptstyle{\prod_{i}F^{\mathbb{C}_{i}}}$$\scriptstyle{H}$$\scriptstyle{F^{\mathbb{D}}}$
(10)

To this end, we generalise a standard technique from monad theory, used for
lifting adjunctions to the Eilenberg–Moore categories [Joh75] or to lifting
monoidal structure to the algebras of commutative monad [Koc71b] (see also
[Jac94, Sea13, JMS22b]). For such a lifting to exist, given a Kleisli law, it
is sufficient that the codomain category of coalgebras has sufficient
equalisers. In our case, it is enough to check that the comonad on the target
category preserves embeddings and the rest is ensured by Linton’s theorem
[Lin69]. In the following paragraphs we review the terminology necessary for
the said theorem.

We say that a pair of classes of morphisms $(\mathcal{E},\mathcal{M})$ is a
_weak factorisation system_ in a category $\mathcal{C}$ if:

  * •

Every morphism $f$ in $\mathcal{C}$ factorises as $f=m\circ e$ for some
$m\in\mathcal{M}$ and $e\in\mathcal{E}$.

  * •

$\mathcal{E}=\\{e\mid\forall m\in\mathcal{M},e\pitchfork m\\}$ and
$\mathcal{M}=\\{m\mid\forall e\in\mathcal{E},e\pitchfork m\\}$. $e\pitchfork
m$ expresses that $e$ is weakly orthogonal to $m$, that is, for any
commutative diagram as shown on the left-hand side below

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

there exists a diagonal morphism $d$ as shown in the diagram on the right-hand
side above, making the diagram commute.

Morphisms of $\mathcal{E}$ are called _quotients_ and are denoted by
$\twoheadrightarrow$ and morphisms of $\mathcal{M}$ are _embeddings_ which we
denote by $\rightarrowtail$. We further say that $(\mathcal{E},\mathcal{M})$
is a _proper factorisation system_ if it is a weak factorisation system such
that $\mathcal{E}$ is a class of epimorphisms and $\mathcal{M}$ is a class of
monomorphisms.

Factorisation systems are omnipresent in category theory. For example, the
category of sets is equipped with the (surjectives, injectives) proper
factorisation system. Similarly, $\mathcal{R}(\sigma)$ and
$\mathcal{R}_{*}(\sigma)$ come equipped with $(\text{epis},\text{strong
monos})$ factorisation system [AR94]. In this case epis are precisely the
surjective homomorphisms of (pointed) $\sigma$-structures and strong monos are
precisely the _embeddings_ , that is, injective homomorphisms $f\colon A\to B$
which reflect relations. In fact, strong monos are the same as regular,
extremal, or effective monos in this $\mathcal{R}(\sigma)$ and
$\mathcal{R}_{*}(\sigma)$.

In the following, we always assume that (pointed) $\sigma$-structures come
equipped with (epi, strong mono) factorisation system.

Finally, for a comonad $\mathbb{C}$ on a category $\mathcal{C}$ with a proper
factorisation system we say that $\mathbb{C}$ _preserves embeddings_ if
$\mathbb{C}(f)$ is an embedding whenever $f$ is. In similar fashion, an
$n$-ary operation $H$ preserves embeddings if $H(f_{1},\dots,f_{n})$ is an
embedding whenever $f_{1},\dots,f_{n}$ are embeddings in their respective
categories.

######  Theorem 10 (Linton [Lin69]).

Given a comonad $\mathbb{C}$ on a category $\mathcal{C}$ equipped with a
proper factorisation system $(\mathcal{E},\mathcal{M})$ if

  1. (1)

$\mathbb{C}$ preserves $\mathcal{M}$-morphisms,

  2. (2)

$\mathcal{C}$ has coproducts and

  3. (3)

$\mathcal{C}$ is _$\mathcal{M}$ -well-powered_, that is, every object $A$ of
$\mathcal{C}$ has up to isomorphism only a set of embeddings $X\rightarrowtail
A$.

then $\mathsf{EM}(\mathbb{C})$ has equalisers.

######  Remark 11.

This is essentially the dual of [Lin69, Proposition 4], up to some small
technical differences. We provide a full proof in the form we require for
completeness.

To prove Linton’s theorem, we first establish some preliminaries. We need a
standard fact that comonads that preserve embeddings lift the factorisation
system from the underlying category to their category of coalgebras. This is
essential not only for the proof of Theorem 10 but also for the definition of
$\equiv_{\mathbb{C}}$ in Section 5.3.

######  Lemma 12.

Given a comonad $\mathbb{C}$ on a category with a proper factorisation system
$(\mathcal{E},\mathcal{M})$. If $\mathbb{C}$ preserves embeddings then
$\mathsf{EM}(\mathbb{C})$ admits a proper factorisation system
$(\overline{\mathcal{E}},\overline{\mathcal{M}})$ where a morphism of
coalgebras $h\colon(A,\alpha)\to(B,\beta)$ is in $\overline{\mathcal{E}}$
(resp. $\overline{\mathcal{M}}$) if the underlying morphism $h\colon A\to B$
is in $\mathcal{E}$ (resp. $\mathcal{M}$).

Next, we prove an intermediate statement from which Linton’s theorem follows.
In the proof of Theorem 10 the category $\mathcal{A}$ will be
$\mathsf{EM}(\mathbb{C})$ for some comonad $\mathbb{C}$.

######  Lemma 13.

If a category $\mathcal{A}$ has a proper factorization system
$(\mathcal{E},\mathcal{M})$, is $\mathcal{M}$-well-powered and has coproducts
then $\mathcal{A}$ has equalisers.

######  Proof 5.1.

Consider parallel pair:

${A}$${B}$$\scriptstyle{f}$$\scriptstyle{g}$

As $\mathcal{A}$ is well-powered and has a factorization system, there is a
set $I$ of isomorphism classes $[m_{i}]$ of embeddings $m_{i}:M_{i}\rightarrow
A$ equalizing $f$ and $g$. As

$f\circ[m_{i}]=[f\circ m_{i}]=[g\circ m_{i}]=g\circ[m_{i}]$

the induced morphism $\widetilde{m}:\coprod_{i}M_{i}\to A$ equalises $f$ and
$g$. As $\mathcal{A}$ has a factorization system, the morphism $\widetilde{m}$
factors as:

${\coprod_{i}M_{i}}$${E}$${A}$$\scriptstyle{e}$$\scriptstyle{m}$

Next, assume $h:C\rightarrow A$ equalises $f$ and $g$. Observe that
$m^{\prime}$ in the $(\mathcal{E},\mathcal{M})$ factorisation $m^{\prime}\circ
e^{\prime}$ of $h$ also equalises $f$ and $g$ since $e^{\prime}$ is an
epimorphism. We might assume that $m^{\prime}=m_{i}$ for some $i$. Let $j$ be
the corresponding coproduct injection. The following commutes:

${\coprod_{i}M_{i}}$${E}$${A}$${B}$${M_{i}}$${C}$$\scriptstyle{e}$$\scriptstyle{m}$$\scriptstyle{f}$$\scriptstyle{g}$$\scriptstyle{j}$$\scriptstyle{e^{\prime}}$$\scriptstyle{h}$

As the factorization system is proper, $m$ is a monomorphism, and so $e\circ
j\circ e^{\prime}$ is the unique morphism $C\to E$ factorising $h$ via $m$.
Consequently, $m$ equalises $f$ and $g$.

We’re now ready to prove Linton’s theorem.

######  Proof 5.2 (Proof of Theorem 10.).

We check that $\mathsf{EM}(\mathbb{C})$ satisfies the conditions of Lemma 13.
By Lemma 12, since $\mathbb{C}$ preserves embeddings the proper factorisation
system $(\mathcal{E},\mathcal{M})$ on $\mathcal{C}$ lifts to a proper
factorisation system $(\overline{\mathcal{E}},\overline{\mathcal{M}})$ on
$\mathsf{EM}(\mathbb{C})$. By the definition of $\overline{\mathcal{M}}$ since
$\mathcal{C}$ is well-powered so is $\mathsf{EM}(\mathbb{C})$. Finally,
$\mathsf{EM}(\mathbb{C})$ has coproducts since the forgetful functor
$\mathsf{EM}(\mathbb{C})\to\mathcal{C}$ reflects them.

All the comonads that we have introduced thus far preserve embeddings and
$\mathcal{R}(\sigma)$ and $\mathcal{R}_{*}(\sigma)$ both have coproducts, in
the case of $\mathcal{R}(\sigma)$ these are disjoint unions of structures and
in the case of $\mathcal{R}_{*}(\sigma)$ we glue the disjoint union by the
distinguished elements. Finally, we see that both categories are also well-
powered because each embedding $X\rightarrowtail A$ is determined by its image
in $A$ and there are only set-many of these.

######  Corollary 14.

If a comonad $\mathbb{C}$ on $\mathcal{R}(\sigma)$ or on
$\mathcal{R}_{*}(\sigma)$ preserves embeddings then $\mathsf{EM}(\mathbb{C})$
has equalisers.

In particular, $\mathsf{EM}({\mathbb{E}_{k}})$,
$\mathsf{EM}({\mathbb{P}_{k}})$ and $\mathsf{EM}({\mathbb{M}_{k}})$ have
equalisers.

Let us come back to the question of lifting functors
$H\colon\prod_{i}\mathcal{C}_{i}\to\mathcal{D}$ to the category of coalgebras,
in sense of (10) above. It might come as a surprise that nothing more than a
Kleisli law and existence of equalisers is needed for the lift to exist.

thmEMLifting If $\kappa$ is a Kleisli law of type $\mathbb{D}\circ
H\Rightarrow H\circ\prod_{i}\mathbb{C}_{i}$ and $\mathsf{EM}(\mathbb{D})$ has
equalisers then the lifting of $H$ to
$\widehat{H}:\prod_{i}\mathsf{EM}(\mathbb{C}_{i})\rightarrow\mathsf{EM}(\mathbb{D})$
exists.

######  Remark 15 (Notation).

In the following we often just write $\alpha$ instead of $(A,\alpha)$ in
expressions that involve a coalgebra $(A,\alpha)\in\mathsf{EM}(\mathbb{C})$.
In particular, the morphism $\iota_{\vv{\alpha_{i}}}$ below is parametrised by
the coalgebras $\\{\,(A_{i},\alpha_{i})\,\\}_{i}$ and the same is true for the
resulting coalgebra $\widehat{H}(\vv{\alpha_{i}})$.

Furthermore, we often omit the subscripts for the components of natural
transformations, if they can be easily inferred from the context. For example,
we shall write $\kappa$ instead of $\kappa_{A_{1},\dots,A_{n}}$ and
$\lambda_{H}$ instead of the more verbose $\lambda_{H(A_{1},\dots,A_{n})}$.

######  Proof 5.3.

Let $(A_{i},\alpha_{i})\in\mathsf{EM}(\mathbb{C}_{i})$ be a collection of
coalgebras, for $i\in I$. By our assumptions, we can form the following
equaliser in $\mathsf{EM}(\mathbb{D})$.

${\widehat{H}(\vv{\alpha_{i}})}$${F^{\mathbb{D}}(H(\vv{A_{i}}\mkern
1.0mu))}$${F^{\mathbb{D}}(H(\vv{\mathbb{C}_{i}(A_{i})}))}$$\scriptstyle{\iota_{\vv{\alpha_{i}}}}$$\scriptstyle{F^{\mathbb{D}}(\kappa)\circ\delta}$$\scriptstyle{F^{\mathbb{D}}(H(\vv{\alpha_{i}}))}$
(11)

Observe that the mapping on objects
$\vv{\alpha_{i}}\mapsto\widehat{H}(\vv{\alpha_{i}})$ extends to a functor.
Given coalgebra morphisms $f_{i}\colon(A_{i},\alpha_{i})\to(B_{i},\beta_{i})$,
for $i\in\\{1,\dots,n\\}$, obtain a diagram of the following form.

${\widehat{H}(\vv{\alpha_{i}})}$${F^{\mathbb{D}}(H(\vv{A_{i}}))}$${\widehat{H}(\vv{\beta_{i}})}$${F^{\mathbb{D}}(H(\vv{B_{i}}))}$${F^{\mathbb{D}}(H(\vv{\mathbb{C}_{i}(B_{i})}))}$$\scriptstyle{\widehat{H}(f_{i})}$$\scriptstyle{\iota_{\vv{\alpha_{i}}}}$$\scriptstyle{F^{\mathbb{D}}(H(\vv{f_{i}}\mkern
1.0mu))}$$\scriptstyle{\iota_{\vv{\beta_{i}}}}$$\scriptstyle{F^{\mathbb{D}}(\kappa)\circ\delta}$$\scriptstyle{F^{\mathbb{D}}(H(\vv{\beta_{i}}))}$
(12)

It follows from the fact that $f_{1},\dots,f_{n}$ are coalgebra morphisms that
$F^{\mathbb{D}}(H(\vv{f_{i}}\mkern 1.0mu))\circ\iota_{\vv{\alpha_{i}}}$
coequalisers the parallel morphisms at the bottom, i.e. that
$F^{\mathbb{D}}(\kappa)\circ\delta\circ F^{\mathbb{D}}(H(\vv{f_{i}}\mkern
1.0mu))\circ\iota_{\vv{\alpha_{i}}}=F^{\mathbb{D}}(H(\vv{\beta_{i}}))\circ
F^{\mathbb{D}}(H(\vv{f_{i}}\mkern 1.0mu))\circ\iota_{\vv{\alpha_{i}}}$. Then,
by the universal property there exists a unique morphism
$\widehat{H}(\vv{\alpha_{i}})\to\widehat{H}(\vv{\beta_{i}})$, which we denote
by $\widehat{H}(f_{i})$, and which makes the square above commute.

Furthermore, one can verify that
$\mathbb{D}(\kappa)\circ\delta:F^{\mathbb{D}}(H(\vv{A_{i}}\mkern 1.0mu))\to
F^{\mathbb{D}}(H(\vv{\mathbb{C}_{i}(A_{i})}))$ equalises the diagram that
defines $\widehat{H}(\vv{F^{\mathbb{C}_{i}}(A_{i})})$, giving us
$\widehat{H}(\vv{F^{\mathbb{C}_{i}}(A_{i})})\cong
F^{\mathbb{D}}(H(\vv{A_{i}}\mkern 1.0mu))$, cf. [JMS22b, Theorem 7.4].

######  Remark 16.

Observe that (11) is a reflexive coequaliser, with $\mathbb{D}H(\varepsilon)$
the mutual post-inverse of the parallel pair. Therefore, the theorem holds in
greater generality with the category $\mathsf{EM}(\mathbb{D})$ only required
to have equalisers of reflexive pairs.

######  Remark 17.

Appendix A of [BK11] contains a statement analogous to our Theorem 14 above.
In fact the authors show that in case of a unary functor
$H\colon\mathcal{C}\to\mathcal{D}$, the lifting
$\widehat{H}\colon\mathsf{EM}(\mathbb{C})\to\mathsf{EM}(\mathbb{D})$ is the
right Kan extension of $K_{\mathbb{D}}\circ H^{\prime}$ along $K_{\mathbb{C}}$
where $H^{\prime}$ is the Kleisli lifting
$\mathsf{Kl}(\mathbb{C})\to\mathsf{Kl}(\mathbb{D})$ from (8) and
$K_{\mathbb{C}}\colon\mathsf{Kl}(\mathbb{C})\to\mathsf{EM}(\mathbb{C})$ is the
comparison functor.

###  5.2. Heteromorphisms

In what follows, we often need to analyse morphisms of the form
$(A,\alpha)\to\widehat{H}(\vv{(B_{i},\beta_{i})})$, for some coalgebras
$(A,\alpha),(B_{1},\beta_{1}),\dots,(B_{n},\beta_{n})$. To aid with this we
restate a direct generalisation of the universal property of bilinear
morphisms or bimorphisms, known from linear algebra and also from the setting
of commutative monads [Koc71a], to our setting.

In this subsection we fix a Kleisli law $\kappa:\mathbb{D}\circ H\Rightarrow
H\circ\prod_{i}\mathbb{C}_{i}$ and its corresponding lifting
$\widehat{H}:\prod_{i}\mathsf{EM}(\mathbb{C}_{i})\rightarrow\mathsf{EM}(\mathbb{D})$
given by Theorem 14. Given a morphism of coalgebras
$f\colon(A,\alpha)\to\widehat{H}(\vv{(B_{i},\beta_{i})})$ we define a
morphisms $f^{\\#}\colon A\to H(\vv{B_{i}}\mkern 1.0mu)$ in $\mathcal{D}$ as

$f^{\\#}\colon
A\xrightarrow{U^{\mathbb{D}}(f)}U^{\mathbb{D}}(\widehat{H}(\vv{B_{i},\beta_{i}}))\xrightarrow{\mathrm{u}_{\vv{\beta_{i}}\mkern
1.0mu}}H(\vv{B_{i}}\mkern 1.0mu)$

where $\mathrm{u}_{\vv{\beta_{i}}\mkern 1.0mu}$ is the composition
$\varepsilon_{H}\circ U^{\mathbb{D}}(\iota_{\vv{\beta_{i}}\mkern 1.0mu})$ of
the underlying morphism of $\iota_{\vv{\beta_{i}}\mkern
1.0mu}\colon\widehat{H}(\vv{\beta_{i}}\mkern 1.0mu)\to
F^{\mathbb{D}}(H(\vv{B_{i}}\mkern 1.0mu))$ with the counit morphism
$\varepsilon_{H}\colon\mathbb{D}(H(\vv{B_{i}}\mkern 1.0mu))\to
H(\vv{B_{i}}\mkern 1.0mu)$.

In the following we observe that $f^{\\#}$ is a _(Kleisli) heteromorphism_
222The name originates in [Ell06] where it was used to talk about morphisms
between objects of different categories. These usually take the form $A\to
F(B)$ where $F$ is a functor. In our case we further require the condition
(13) enforced by the Kleisli law., that is, a morphism $g\colon A\to
H(\vv{B_{i}}\mkern 1.0mu)$, from $(A,\alpha)$ to $\vv{(B_{i},\beta_{i})}$,
written as $g:\alpha\to[\vv{\beta_{i}}\mkern 1.0mu]$, such that the following
diagram commutes.

${A}$${H(\vv{B_{i}})}$${\mathbb{D}(A)}$${\mathbb{D}H(\vv{B_{i}})}$${H(\vv{\mathbb{C}_{i}(B_{i})})}$$\scriptstyle{g}$$\scriptstyle{\alpha}$$\scriptstyle{H(\vv{\beta_{i}})}$$\scriptstyle{\mathbb{D}(g)}$$\scriptstyle{\kappa}$
(13)

In fact, Proposition 5.4 below establishes that the mapping $f\mapsto f^{\\#}$
gives a bijection between coalgebra morphisms and heteromorphisms. First we
observe that heteromorphisms are closed under composition by coalgebra
morphisms from both left and right.

######  Lemma 18.

Given a heteromorphism $f\colon\alpha\to[\vv{\beta_{i}}\mkern 1.0mu]$, a
morphism of $\mathbb{D}$-coalgebras
$h\colon(A^{\prime},\alpha^{\prime})\to(A,\alpha)$ and
$\mathbb{C}_{i}$-coalgebra morphisms
$g_{i}\colon(B_{i},\beta_{i})\to(B^{\prime}_{i},\beta^{\prime}_{i})$, for
$i\in\\{1,\dots,n\\}$, the composite $H(\vv{g_{i}}\mkern 1.0mu)\circ f\circ h$
is a heteromorphism $\alpha^{\prime}\to[\vv{\beta^{\prime}_{i}}\mkern 1.0mu]$.

Crucially we also need that $\mathrm{u}_{\vv{\beta_{i}}\mkern 1.0mu}\colon
U^{\mathbb{D}}(\widehat{H}(\vv{B_{i},\beta_{i}}))\to H(\vv{B_{i}}\mkern
1.0mu)$ from above is a universal heteromorphism, in the following sense.

######  Lemma 19.

The following holds for $\mathrm{u}_{\vv{\beta_{i}}\mkern 1.0mu}$.

  1. (1)

$\mathrm{u}_{\vv{\beta_{i}}\mkern 1.0mu}$ is a heteromorphism
$\widehat{H}(\vv{\beta_{i}}\mkern 1.0mu)\to[\vv{\beta_{i}}\mkern 1.0mu]$.

  2. (2)

For any heteromorphism $f\colon\alpha\to[\vv{\beta_{i}}\mkern 1.0mu]$ there is
a _unique_ $\mathbb{D}$-coalgebra morphism
$f^{+}\colon(A,\alpha)\to\widehat{H}(\vv{\beta_{i}}\mkern 1.0mu)$ such that
$f=\mathrm{u}_{\vv{\beta_{i}}\mkern 1.0mu}\circ f^{+}$ in the underlying
category $\mathcal{D}$.

  3. (3)

The collection of morphisms $\mathrm{u}_{\vv{\beta_{i}}\mkern 1.0mu}$ is
natural in $\vv{\beta_{i}}\mkern 1.0mu$. That is, for any tuple of coalgebra
morphisms $f_{i}\colon\beta_{i}\to\beta_{i}^{\prime}$, for
$i\in\\{1,\dots,n\\}$,

${U^{\mathbb{D}}(\widehat{H}(\vv{B_{i},\beta_{i}}))}$${H(\vv{B_{i}}\mkern
1.0mu)}$${U^{\mathbb{D}}(\widehat{H}(\vv{B^{\prime}_{i},\beta^{\prime}_{i}}))}$${H(\vv{B_{i}}\mkern
1.0mu^{\prime})}$$\scriptstyle{U^{\mathbb{D}}(\widehat{H}(\vv{f_{i}}\mkern
1.0mu))}$$\scriptstyle{\mathrm{u}_{\vv{\beta_{i}}\mkern
1.0mu}}$$\scriptstyle{H(\vv{f_{i}}\mkern
1.0mu)}$$\scriptstyle{\mathrm{u}_{\vv{\beta_{i}}\mkern 1.0mu^{\prime}}}$

######  Proof 5.4.

To simplify the notation we denote the underlying morphism of
$\iota_{\vv{\beta_{i}}\mkern 1.0mu}$ by $\iota_{\vv{\beta_{i}}\mkern 1.0mu}$
and by $(W,\omega)$ we denote the $\mathbb{D}$-coalgebra
$\widehat{H}(\vv{\beta_{i}}\mkern 1.0mu)$, i.e.
$W=U^{\mathbb{D}}(\widehat{H}(\vv{\beta_{i}}\mkern 1.0mu))$ and $\omega\colon
W\to\mathbb{D}(W)$ is such that $\mathbb{D}(\iota_{\vv{\beta_{i}}\mkern
1.0mu})\circ\omega=\delta^{\mathbb{D}}_{H(\vv{B_{i}}\mkern
1.0mu)}\circ\iota_{\vv{\beta_{i}}\mkern 1.0mu}$. Item 1 is a routine
calculation:

$\displaystyle\kappa\circ\mathbb{D}(\varepsilon_{H})\circ\mathbb{D}(\iota_{\vv{\beta_{i}}\mkern
1.0mu})\circ\omega$
$\displaystyle=\kappa\circ\mathbb{D}(\varepsilon_{H})\circ\delta_{H(\vv{B_{i}}\mkern
1.0mu)}\circ\iota_{\vv{\beta_{i}}\mkern 1.0mu}$ $\iota_{\vv{\beta_{i}}\mkern
1.0mu}$ is a coalgebra homomorphism
$\displaystyle=\kappa\circ\varepsilon_{\mathbb{D}H}\circ\delta_{H(\vv{B_{i}}\mkern
1.0mu)}\circ\iota_{\vv{\beta_{i}}\mkern 1.0mu}$ counit axioms
$\displaystyle=\varepsilon_{H\mathbb{C}}\circ\mathbb{D}\kappa\circ\delta_{H(\vv{B_{i}}\mkern
1.0mu)}\circ\iota_{\vv{\beta_{i}}\mkern 1.0mu}$ naturality of $\varepsilon$
$\displaystyle=\varepsilon_{H\mathbb{C}}\circ\mathbb{D}(H(\vv{\beta_{i}}\mkern
1.0mu))\circ\iota_{\vv{\beta_{i}}\mkern 1.0mu}$ $\iota_{\vv{\beta_{i}}\mkern
1.0mu}$ coequalises (11) $\displaystyle=H(\vv{\beta_{i}}\mkern
1.0mu)\circ\varepsilon_{H}\circ\iota_{\vv{\beta_{i}}\mkern 1.0mu}$ naturality
of $\varepsilon$

Item 2 follows the equalizer universal property. First, recall that the
underlying morphism $f\colon\alpha\to[\vv{\beta_{i}}\mkern 1.0mu]$ uniquely
determines the coalgebra morphism $\mathbb{D}(f)\circ\alpha\colon(A,\alpha)\to
F^{\mathbb{D}}(H{\vv{B_{i}}\mkern 1.0mu})$ such that
$f=\varepsilon_{H}\circ\mathbb{D}(f)\circ\alpha$. Furthermore, this coalgebra
morphism equalises (11).

$\displaystyle\mathbb{D}\kappa\circ\delta_{H(\vv{B_{i}}\mkern
1.0mu)}\circ\mathbb{D}(f)\circ\alpha$
$\displaystyle=\mathbb{D}\kappa\circ\mathbb{D}^{2}(f)\circ\delta_{A}\circ\alpha$
naturality of $\delta$
$\displaystyle=\mathbb{D}\kappa\circ\mathbb{D}^{2}(f)\circ\mathbb{D}(\alpha)\circ\alpha$
$\alpha$ is a morphism $(A,\alpha)\to F^{\mathbb{D}}A$
$\displaystyle=\mathbb{D}(H(\vv{\beta_{i}}\mkern
1.0mu))\circ\mathbb{D}(f)\circ\alpha$ heteromorphism assumption (13)

From $\iota_{\vv{\beta_{i}}\mkern 1.0mu}$ being equaliser of (11), there is a
unique $f^{+}\colon(A,\alpha)\to(W,\omega)$ such that
$\iota_{\vv{\beta_{i}}\mkern 1.0mu}\circ f^{+}=\mathbb{D}(f)\circ\alpha$.
Consequently, $\mathrm{u}_{\vv{\beta_{i}}\mkern 1.0mu}\circ
f^{+}=\varepsilon_{H}\circ\mathbb{D}(f)\circ\alpha=f\circ\varepsilon\circ\alpha=f$.

Item 3 follows from the fact that $\varepsilon$ is a natural transformation
and from the definition of $\widehat{H}(\vv{f_{i}}\mkern 1.0mu)$ in terms of
the universal property of equalisers, cf. (12) above.

We are now ready to prove the promised statement. propBimorphisms The mapping
$f\mapsto f^{\\#}$ establishes a one-to-one correspondence between

  * •

coalgebra morphisms $(A,\alpha)\to\widehat{H}(\vv{(B_{i},\beta_{i})})$ and

  * •

heteromorphisms $\alpha\to[\vv{\beta_{i}}\mkern 1.0mu]$.

######  Proof 5.5.

Let $f\colon(A,\alpha)\to\widehat{H}(\vv{(B_{i},\beta_{i})})$ be a coalgebra
morphism. Since $\mathrm{u}_{\vv{\beta_{i}}\mkern 1.0mu}$ is a heteromorphism
(by Lemma 19.1), so is $f^{\\#}$ by Lemma 18. Furthermore, $(f^{\\#})^{+}=f$
by the universal property of $\mathrm{u}_{\vv{\beta_{i}}\mkern 1.0mu}$ (Lemma
19.2). On the other hand, for a heteromorphism
$g\colon\alpha\to[\vv{\beta_{i}}\mkern 1.0mu]$ we clearly have
$(g^{+})^{\\#}=g$, again by the universal property of
$\mathrm{u}_{\vv{\beta_{i}}\mkern 1.0mu}$.

Lastly, we show that the mapping $f\mapsto f^{\\#}$ commutes with compositions
with coalgebra morphisms.

######  Proposition 20.

For a $\mathbb{D}$-coalgebra morphism
$h\colon(A^{\prime},\alpha^{\prime})\to(A,\alpha)$ and
$\mathbb{C}_{i}$-coalgebra morphisms
$g_{i}\colon(B_{i},\beta_{i})\to(B^{\prime}_{i},\beta^{\prime}_{i})$:

$(\widehat{H}(\vv{g_{i}}\mkern 1.0mu)\circ f\circ h)^{\\#}=H(\vv{g_{i}}\mkern
1.0mu)\circ f^{\\#}\circ h.$

######  Proof 5.6.

Let $f\colon(A,\alpha)\to\widehat{H}(\vv{(B_{i},\beta_{i})})$ and
$h\colon(A^{\prime},\alpha^{\prime})\to(A,\alpha)$ be $\mathbb{D}$-coalgebra
morphisms. Then,

$(f\circ h)^{\\#}=\mathrm{u}_{\vv{\beta_{i}}\mkern 1.0mu}\circ f\circ
h=f^{\\#}\circ h.$

Similarly, for coalgebra morphisms
$g_{i}\colon(B_{i},\beta_{i})\to(B^{\prime}_{i},\beta^{\prime}_{i})$, for
$i\in\\{1,\dots,n\\}$, we have

$(\widehat{H}(\vv{g_{i}}\mkern 1.0mu)\circ
f)^{\\#}=\mathrm{u}_{\vv{\beta^{\prime}_{i}}\mkern 1.0mu}\circ
U^{\mathbb{D}}(\widehat{H}({\vv{g_{i}}\mkern 1.0mu}))\circ
f=H(\vv{g_{i}}\mkern 1.0mu)\circ\mathrm{u}_{\vv{\beta_{i}}\mkern 1.0mu}\circ
f=H(\vv{g_{i}}\mkern 1.0mu)\circ f^{\\#}$

where the equality in the middle follows from Lemma 19.3. We see that
$(\widehat{H}(\vv{g_{i}}\mkern 1.0mu)\circ f\circ h)^{\\#}=H(\vv{g_{i}}\mkern
1.0mu)\circ f^{\\#}\circ h$ now follows from these two observations and Lemma
18, which ensures that $f\circ h$ is a heteromorphism.

###  5.3. Open pathwise-embeddings and their preservation

In this section we define open pathwise-embeddings and give sufficient
conditions for the lifted functors of Section 5.1 to preserve them. In fact,
our condition is a combination of two other categorical properties: parametric
adjoints and relative adjoints, which we discuss in Appendix A.

To emphasise the main ingredients of our arguments we restrict to a simplified
setting of _path categories_. These are categories $\mathcal{A}$ equipped with
a proper factorisation system $(\mathcal{E},\mathcal{M})$ and a choice of
_path_ objects $\mathcal{P}\subseteq\mathrm{obj}(\mathcal{A})$.

${P}$${Q}$${X}$${Y}$$\scriptstyle{e}$$\scriptstyle{g}$$\scriptstyle{m}$$\scriptstyle{f}$

In this setting, an embedding $e\colon P\rightarrowtail X$ is a _path
embedding_ if $P$ is a path (i.e. $P\in\mathcal{P}$). Then, $f\colon X\to Y$
is _pathwise-embedding_ if $f\circ e$ is an embedding for every path embedding
$e\colon P\rightarrowtail X$. Finally, $f$ is _open_ if for every commutative
square as shown on the right, where $e,m,g$ are path embeddings, there exists
a morphism $d\colon Q\to X$ such that $e=d\circ g$ and $m=f\circ d$.

Recall from Remark 9 that coalgebras $(A,\alpha)$, for either of our example
comonad
$\mathbb{C}\in\\{{\mathbb{E}_{k}},{\mathbb{P}_{k}},{\mathbb{M}_{k}}\\}$, come
equipped with a forest order $\sqsubseteq_{\alpha}$ on the universe. In the
following, we always assume that path coalgebras
$\mathcal{P}\subseteq\mathsf{EM}(\mathbb{C})$ are the coalgebras $(A,\alpha)$
which are finite linear orders in $\sqsubseteq_{\alpha}$.

Furthermore, since $\mathbb{C}$ typically preserves embeddings of
$\sigma$-structures, $\mathsf{EM}(\mathbb{C})$ admits a proper factorisation
system $(\overline{\mathcal{E}},\overline{\mathcal{M}})$ by lifting the (epi,
strong mono) factorisation system of (pointed) $\sigma$-structures, cf. Lemma
12. Consequently, we view $\mathsf{EM}({\mathbb{E}_{k}})$,
$\mathsf{EM}({\mathbb{P}_{k}})$, and $\mathsf{EM}({\mathbb{M}_{k}})$ as path
categories in the above sense.

In fact, every _arboreal category_ , in sense of [AR21], is an path category.
Note that the notion of path category in [AR21] is different from ours.

######  Remark 21.

With the notion of open pathwise-embedding for $\mathsf{EM}(\mathbb{C})$ with
paths and embeddings specified as above, we recall that
$A\equiv_{\mathbb{C}}B$ iff there exists a pair of open pathwise-embeddings
$F^{\mathbb{C}}(A)\leftarrow Z\rightarrow F^{\mathbb{C}}(B)$, where
$F^{\mathbb{C}}(A)$ is the cofree coalgebra on $A$.

We now come back to our original goal. In order for an $n$-ary operation
$H\colon\prod_{i}\mathcal{C}_{i}\to\mathcal{D}$ to admit an FVM theorem, we
wish to show that its lifting
$\widehat{H}\colon\prod\nolimits_{i}\mathsf{EM}(\mathbb{C}_{i})\to\mathsf{EM}(\mathbb{D})$
described in Theorem 14, sends tuples of open pathwise embeddings to pathwise
embeddings.

In our simplified setting, we have a functor
$\widehat{H}\colon\prod\nolimits_{i}\mathcal{A}_{i}\to\mathcal{B}$ between
path categories. In the remainder of this section show that $\widehat{H}$
preserves open pathwise-embeddings assuming the following two conditions:

  1. (S1)

$\widehat{H}\colon\prod_{i}\mathcal{A}_{i}\to\mathcal{B}$ preserves
embeddings.

  2. (S2)

Any path embedding $e\colon P\rightarrowtail\widehat{H}(\vv{A_{i}}\mkern
1.0mu)$ has a _minimal decomposition_ as $e_{0}\colon
P\to\widehat{H}(\vv{P_{i}}\mkern 1.0mu)$ followed by
$\widehat{H}(\vv{e_{i}}\mkern 1.0mu)\colon\widehat{H}(\vv{P_{i}}\mkern
1.0mu)\to\widehat{H}(\vv{A_{i}}\mkern 1.0mu)$, for some path embeddings
$e_{i}\colon P_{i}\rightarrowtail A_{i}$, for $1\leq i\leq n$.

Minimality in (S2) expresses that for any decomposition of $e$ as $g_{0}\colon
P\to\widehat{H}(\vv{Q_{i}}\mkern 1.0mu)$ followed by
$\widehat{H}(\vv{g_{i}}\mkern 1.0mu)\colon\widehat{H}(\vv{Q_{i}}\mkern
1.0mu)\to\widehat{H}(\vv{A_{i}}\mkern 1.0mu)$, for some path embeddings
$g_{i}\colon Q_{i}\rightarrowtail A_{i}$, there exist necessarily unique
morphisms $h_{i}\colon P_{i}\to Q_{i}$ such that $e_{i}=g_{i}\circ h_{i}$, for
$i=1,\dots,n$.

We are going to need the following standard facts about embeddings of a proper
factorisation system. The dual statement for quotients holds too but we do not
need it here.

######  Lemma 22 (e.g. Section 2 in [FK72]).

For a category with a proper factorisation system $(\mathcal{E},\mathcal{M})$:

  1. (1)

All equalisers are embeddings.

  2. (2)

Embeddings are closed under composition.

  3. (3)

If $g\circ f$ is an embedding then so is $f$.

These basic properties of embeddings listed in Lemma 22 allow us to show the
first half of our desired result, preservation of pathwise-embeddings.

lemPEPreserved If $f_{1},\dots,f_{n}$ are pathwise-embeddings in
$\mathcal{A}_{1}$, …, $\mathcal{A}_{n}$, respectively, then so is
$\widehat{H}(f_{1},\dots,f_{n})$.

######  Proof 5.7.

Assume $e\colon P\rightarrowtail\widehat{H}(\vv{A_{i}}\mkern 1.0mu)$ is a path
embedding where, for each $i$, $A_{i}$ is the domain of $f_{i}$. By (S2), $e$
decomposes as:

${P}$${\widehat{H}(\vv{P_{i}}\mkern 1.0mu)}$${\widehat{H}(\vv{A_{i}}\mkern
1.0mu)}$$\scriptstyle{e_{0}}$$\scriptstyle{\widehat{H}(\vv{e_{i}}\mkern
1.0mu)}$

Observe that, by Lemma 22.3, $e_{0}$ is an embedding because $e$ is. Further,
since $f_{i}$ is a pathwise-embedding, for $i=1,\dots,n$, the morphism
$f_{i}\circ e_{i}$ is an embedding. Therefore, by (S1),
$\widehat{H}(\vv{f_{i}\circ e_{i}})$ is also an embedding. We obtain that the
composite $\widehat{H}(\vv{f_{i}}\mkern 1.0mu)\circ
e=\widehat{H}(\vv{f_{i}\circ e_{i}})\circ e_{0}$ is an embedding because
embeddings are closed under composition, cf. Lemma 22.2.

For the preservation of openness, we need the following technical lemma.

lemLemmaIFour Let $f_{i}\colon A_{i}\to B_{i}$ in $\mathcal{A}_{i}$ be
pathwise-embeddings, for each $i$, and let $e$ and $g$ be path embeddings
making the diagram on the left below commute.

${P}$${\widehat{H}(\vv{A_{i}}\mkern 1.0mu)}$${\widehat{H}(\vv{B_{i}}\mkern
1.0mu)}$$\scriptstyle{e}$$\scriptstyle{g}$$\scriptstyle{\widehat{H}(\vv{f_{i}}\mkern
1.0mu)}$
${P_{i}}$${Q_{i}}$${A_{i}}$${B_{i}}$$\scriptstyle{f^{\prime}_{i}}$$\scriptstyle{e_{i}}$$\scriptstyle{g_{i}}$$\scriptstyle{f_{i}}$

Then, for $i=1,\dots,n$, there exist morphisms

$f^{\prime}_{i}\colon P_{i}\to Q_{i},$

such that the diagram on the right above commutes. Here, the $e_{i}$ and
$g_{i}$ are the minimal embeddings given by (S2) such that $e$ and $g$
decompose through $\widehat{H}(\vv{e_{i}}\mkern 1.0mu)$ and
$\widehat{H}(\vv{g_{i}}\mkern 1.0mu)$, respectively.

######  Proof 5.8.

Let $e_{0}\colon P\rightarrowtail\widehat{H}(\vv{P_{i}}\mkern 1.0mu)$ be the
embedding such that $\widehat{H}(\vv{e_{i}}\mkern 1.0mu)\circ e_{0}$ is the
minimal decomposition of $e$ by (S2). Since

$\widehat{H}(\vv{f_{i}}\mkern 1.0mu)\circ e=\widehat{H}(\vv{f_{i}\circ
e_{i}})\circ e_{0}$

is another decomposition of $g$, there exists morphisms $l_{i}\colon
Q_{i}\rightarrowtail P_{i}$ such that $g_{i}=f_{i}\circ e_{i}\circ l_{i}$, for
$i=1,\dots,n$.

Next, we observe that $e_{0}=\widehat{H}(\vv{l_{i}}\mkern 1.0mu)\circ g_{0}$
where

$g_{0}\colon P\rightarrowtail\widehat{H}(\vv{Q_{i}}\mkern 1.0mu)$

is such that $\widehat{H}(\vv{g_{i}}\mkern 1.0mu)\circ g_{0}$ is the minimal
decomposition of $g$. Observe that

$\displaystyle\widehat{H}(\vv{f_{i}\circ e_{i}})\circ
e_{0}=g=\widehat{H}(\vv{g_{i}}\mkern 1.0mu)\circ
g_{0}=\widehat{H}(\vv{f_{i}\circ e_{i}\circ l_{i}})\circ
g_{0}=\widehat{H}(\vv{f_{i}\circ e_{i}})\circ\widehat{H}(\vv{l_{i}}\mkern
1.0mu)\circ g_{0}.$

Therefore, since by (S1) $\widehat{H}(\vv{f_{i}\circ e_{i}})$ is an embedding,
we obtain that $e_{0}=\widehat{H}(\vv{l_{i}}\mkern 1.0mu)\circ g_{0}$.

Consequently, we obtain another decomposition of $e$, given by
$\widehat{H}(\vv{e_{i}\circ l_{i}})\circ g_{0}$. By minimality
$\vv{e_{i}}\mkern 1.0mu$, there exists

$f^{\prime}_{i}\colon P_{i}\to Q_{i},$

for $i=1,\dots,n$, such that $e_{i}=e_{i}\circ l_{i}\circ f^{\prime}_{i}$.
Therefore, for $i=1,\dots,n$,

$f_{i}\circ e_{i}=f_{i}\circ e_{i}\circ l_{i}\circ f^{\prime}_{i}=g_{i}\circ
f^{\prime}_{i}.$

We are now ready to proof the main theorem of this section.

thmSmoothnessTheorem If $\widehat{H}$ satisfies (S1) and (S2) and
$f_{1},\dots,f_{n}$ are open pathwise-embeddings, then so is
$\widehat{H}(\vv{f_{i}}\mkern 1.0mu)$.

######  Proof 5.9.

Given for $i=1,\dots,n$, open pathwise-embeddings $f_{i}\colon A_{i}\to B_{i}$
in $\mathsf{EM}(\mathbb{C}_{i})$, it is enough to check that
$\widehat{H}(\vv{f_{i}}\mkern 1.0mu)$ is open by Lemma 22. Assume that the
outer square of path embeddings in the diagram below commutes, with the left-
most and right-most morphisms being their minimal decompositions by (S2).

${P}$${Q}$${\widehat{H}(\vv{P_{i}}\mkern
1.0mu)}$${\widehat{H}(\vv{P^{\prime}_{i}}\mkern
1.0mu)}$${\widehat{H}(\vv{Q_{i}}\mkern 1.0mu)}$${\widehat{H}(\vv{A_{i}}\mkern
1.0mu)}$${\widehat{H}(\vv{B_{i}}\mkern
1.0mu)}$$\scriptstyle{h}$$\scriptstyle{e_{0}}$$\scriptstyle{e^{\prime}_{0}}$$\scriptstyle{g_{0}}$$\scriptstyle{\widehat{H}(\vv{e_{i}}\mkern
1.0mu)}$$\scriptstyle{\widehat{H}(\vv{f^{\prime}_{i}})}$$\scriptstyle{\widehat{H}(\vv{e^{\prime}_{i}})}$$\scriptstyle{\widehat{H}(\vv{h_{i}}\mkern
1.0mu)}$$\scriptstyle{\widehat{H}(\vv{g_{i}}\mkern
1.0mu)}$$\scriptstyle{\widehat{H}(\vv{f_{i}}\mkern 1.0mu)}$

The path embedding $\widehat{H}(\vv{f_{i}\circ e_{i}})\circ e_{0}$ has a
minimal decomposition going via $\widehat{H}(\vv{e^{\prime}_{i}})$ as shown
above. Then, by minimality of this decomposition and by Lemma 5.7, for
$i=1,\dots,n$, there exist $f^{\prime}_{i}\colon P_{i}\to P^{\prime}_{i}$ and
$h_{i}\colon P^{\prime}_{i}\to Q_{i}$ such that $f_{i}\circ
e_{i}=e^{\prime}_{i}\circ f^{\prime}_{i}$ and $e^{\prime}_{i}=g_{i}\circ
h_{i}$. Since $f_{i}$ is open and $f_{i}\circ e_{i}=g_{i}\circ h_{i}\circ
f^{\prime}_{i}$, there is a morphism $d_{i}\colon Q_{i}\to A_{i}$ such that
$d_{i}\circ h_{i}\circ f^{\prime}_{i}=e_{i}$ and $g_{i}=d_{i}\circ f_{i}$.
Finally, because the outer rectangle and the bottom rectangle commute and
$\widehat{H}(\vv{g_{i}}\mkern 1.0mu)$ is a monomorphism, the top rectangle
commute as well. Consequently, $\widehat{H}(\vv{d_{i}}\mkern 1.0mu)\circ
g_{0}\colon Q\to\widehat{H}(\vv{A_{i}}\mkern 1.0mu)$ is the required diagonal
filler of the outer square.

###  5.4. Simplifying the axioms for comonads

Axioms (S1) and (S2) give us sufficient conditions for functors between path
categories to preserve open pathwise-embeddings. In our case the path
categories of interests are categories of coalgebras for our game comonads and
the functor in question $\widehat{H}$ is typically a lifted functor $H$ on the
base categories. In this section we describe simpler conditions in terms of
heteromorphisms that imply axioms (S1) and (S2). This way we can establish
their validity easily, without having to analyse the lifted functor
$\widehat{H}$.

In this section we fix a functor between base categories
$H\colon\prod_{i}\mathcal{C}_{i}\to\mathcal{D}$ and assume that it lifts to
$\widehat{H}\colon\prod_{i}\mathsf{EM}(\mathbb{C}_{i})\to\mathsf{EM}(\mathbb{D})$
as in Theorem 14. To begin with, we observe that (S1) is implied by a similar
property of $H$.

propSOnePrime If $H$ preserves embeddings then so does $\widehat{H}$.

######  Proof 5.10.

Let

$e_{1}\colon(A_{1},\alpha_{1})\to(B_{1},\beta_{1}),\ \dots,\
e_{n}\colon(A_{n},\alpha_{n})\to(B_{n},\beta_{n})$

be embeddings in
$\mathsf{EM}(\mathbb{C}_{1}),\dots,\mathsf{EM}(\mathbb{C}_{n})$, respectively.
Recall that $\widehat{H}(e_{1},\dots,e_{n})$ is defined by the universal
property of equalisers. In particular, it makes the following diagram commute.

${\widehat{H}(\vv{\alpha_{i}})}$${F^{\mathbb{D}}(H(\vv{A_{i}}))}$${\widehat{H}(\vv{\alpha^{\prime}_{i}})}$${F^{\mathbb{D}}(H(\vv{A^{\prime}_{i}}))}$$\scriptstyle{\widehat{H}(\vv{e_{i}}\mkern
1.0mu)}$$\scriptstyle{\iota_{\vv{\alpha_{i}}}}$$\scriptstyle{F^{\mathbb{D}}(H(\vv{U(e_{i})}))}$$\scriptstyle{\iota_{\vv{\alpha^{\prime}_{i}}}}$

From $e_{1},\dots,e_{n}$ being embeddings we know that
$F^{\mathbb{D}}(H(\vv{U(e_{i})}))$ is an embedding as well because
$\mathbb{D}$ and $H$ preserve embeddings. Furthermore, by Lemma 22.1,
$\iota_{\vv{\alpha_{i}}}$ is an embedding since it is an equaliser and,
consequently, by Lemma 22.3, $\widehat{H}(\vv{e_{i}}\mkern 1.0mu)$ is an
embedding too.

To proceed we need the following simple lemma about decompositions of
heteromorphisms.

######  Lemma 23.

Assume that both $\mathbb{D}$ and $H$ preserve embeddings. Then, given a
heteromorphism $f\colon\alpha\to[\vv{\beta_{i}}]$ which decomposes as
$f_{0}\colon A\to H(\vv{A_{i}})$ followed by $H\left(\vv{e_{i}}\mkern
1.0mu\right)$, for some coalgebra embeddings
$e_{i}\colon\alpha_{i}\rightarrowtail\beta_{i}$, for $1\leq i\leq n$, the
morphism $f_{0}$ is a heteromorphism $\alpha\to\left[\vv{\alpha_{i}}\right]$.

######  Proof 5.11.

We show that the left oblong in the diagram below commutes.

${A}$${H(\vv{A_{i}})}$${H(\vv{B_{i}})}$${H(\vv{\mathbb{D}(A_{i})})}$${H(\vv{\mathbb{D}(B_{i})})}$${\mathbb{D}(P)}$${\mathbb{D}(H(\vv{A_{i}}))}$${\mathbb{D}(H(\vv{B_{i}}))}$$\scriptstyle{f_{0}}$$\scriptstyle{\alpha}$$\scriptstyle{H(\vv{e_{i}})}$$\scriptstyle{H(\vv{\alpha_{i}})}$$\scriptstyle{H(\vv{\beta_{i}})}$$\scriptstyle{H(\vv{\mathbb{D}(e_{i})})}$$\scriptstyle{\mathbb{D}(f_{0})}$$\scriptstyle{\kappa}$$\scriptstyle{\mathbb{D}(H(\vv{e_{i}}))}$$\scriptstyle{\kappa}$

Since $f$ is a heteromorphism, we know that the outer square commutes.
Further, the two squares on the right commute by naturality of $\kappa$ and
the assumption that $e_{i}$, for $1\leq i\leq n$, is a coalgebra morphism. A
simple diagram chasing implies that

$H(\vv{\mathbb{D}(e_{i})})\circ H(\vv{\alpha_{i}})\circ
f_{0}=H(\vv{\mathbb{D}(e_{i})})\circ\kappa\circ\mathbb{D}(f_{0})\circ\alpha.$

Since $\mathbb{D}$ and $H$ preserve embeddings, $H(\vv{\mathbb{D}(e_{i})})$ is
an embedding and hence a mono, proving that $f_{0}$ is a heteromorphism.

We observe that (S2) is implied by a simple condition which can be stated
entirely in terms of heteromorphisms, that is, typically it is a condition in
the base category of (pointed) relational structures.

propSTwoPrime The axiom (S2) is implied by the following axiom:

  1. (S2’)

For any path $(P,\pi)$ in $\mathsf{EM}(\mathbb{D})$ and coalgebras
$(A_{i},\alpha_{i})$ in $\mathsf{EM}(\mathbb{C}_{i})$ for $1\leq i\leq n$,
every heteromorphism $\pi\to[\vv{\alpha_{i}}\mkern 1.0mu]$ has a minimal
decomposition through

$H(\vv{e_{i}}\mkern 1.0mu)\colon H(\vv{P_{i}})\to H(\vv{A_{i}}),$

for some path embeddings
$e_{i}\colon(P_{i},\pi_{i})\rightarrowtail(A_{i},\alpha_{i})$.

######  Proof 5.12.

Let $e\colon(P,\pi)\rightarrowtail\widehat{H}(\vv{(A,\alpha_{i})})$ be a path
embedding and let $f=e^{\\#}$ be be the corresponding homomorphism of
(pointed) $\sigma$-structures $P\to H(\vv{A_{i}})$, obtained by Proposition
5.4.

By (S2’), $f$ has a minimal decomposition as $H(\vv{e_{i}}\mkern 1.0mu)\circ
f_{0}$ for some $f_{0}\colon P\to H(\vv{P_{i}})$ and path embeddings

$e_{i}\colon(P_{i},\pi_{i})\rightarrowtail(A_{i},\alpha_{i}),$

with $1\leq i\leq n$. It follows by Lemma 23 that $f_{0}$ is a heteromorphism

$\pi\to\left[\vv{\pi_{i}}\right].$

Therefore, by Proposition 5.4, there exists a coalgebra morphism
$e_{0}\colon\pi\to\widehat{H}\left(\vv{\pi_{i}}\right)$ such that
$e_{0}^{\\#}=f_{0}$ and, furthermore, by Proposition 20

$e^{\\#}=f=H\left(\vv{e_{i}}\mkern 1.0mu\right)\circ
f_{0}=H\left(\vv{e_{i}}\mkern 1.0mu\right)\circ
e_{0}^{\\#}=(\widehat{H}\left(\vv{e_{i}}\mkern 1.0mu\right)\circ e_{0})^{\\#}$

which proves that $e=\widehat{H}\left(\vv{e_{i}}\mkern 1.0mu\right)\circ
e_{0}$, since $(-)^{\\#}$ is a bijection between coalgebra morphisms
$(P,\pi)\to\widehat{H}\left(\vv{\alpha_{i}}\right)$ and heteromorphisms
$\pi\to\left[\vv{\alpha_{i}}\right]$.

Lastly, we show the minimality of this decomposition. If $e$ decomposes as
$g_{0}\colon\pi\to\widehat{H}\left(\vv{\rho_{i}}\right)$ followed by
$\widehat{H}\left(\vv{g_{i}}\mkern 1.0mu\right)$, with embeddings
$g_{i}\colon(Q_{i},\rho_{i})\rightarrowtail(A_{i},\alpha_{i})$, for $1\leq
i\leq n$, then by Proposition 20,

$f=e^{\\#}=(\widehat{H}\left(\vv{g_{i}}\mkern 1.0mu\right)\circ
g_{0})^{\\#}=H\left(\vv{g_{i}}\mkern 1.0mu\right)\circ g_{0}^{\\#}$

Therefore, by minimality of the decomposition $f$ as $H\left(\vv{e_{i}}\mkern
1.0mu\right)\circ f_{0}$, there exist coalgebra morphisms
$h_{i}\colon(P_{i},\pi_{i})\to(Q_{i},\rho_{i})$ such that $e_{i}=g_{i}\circ
h_{i}$, for every $i\in\\{1,\dots,n\\}$.

In fact, (S2) is equivalent to the version of (S2’) where we only care about
morphisms $P\to H(\vv{A_{i}})$ which arise from embeddings via the
correspondence in Proposition 5.4. As a corollary, we obtain an FVM theorem
for the full logic which we state with all assumptions.

thmFVMfulllogic Let $H\colon\prod\nolimits_{i}\mathcal{C}_{i}\to\mathcal{D}$
be a functor and let $\mathbb{C}_{1},\dots,\mathbb{C}_{n}$ and $\mathbb{D}$ be
comonads on categories $\mathcal{C}_{1},\dots,\mathcal{C}_{n}$ and
$\mathcal{D}$, respectively, such that each of the arising categories of
coalgebras are path categories and, furthermore, $\mathsf{EM}(\mathbb{D})$ has
equalisers.

If $H$ preserves embeddings and there exists a Kleisli law of type
$\mathbb{D}\circ H\Rightarrow H\circ\prod\nolimits_{i}\mathbb{C}_{i}$
satisfying (S2’), then

$A_{1}\equiv_{\mathbb{C}_{1}}B_{1},\;\ldots,\;A_{n}\equiv_{\mathbb{C}_{n}}B_{n}$

implies

$H(A_{1},\dots,A_{n})\;\equiv_{\mathbb{D}}\;H(B_{1},\dots,B_{n}).$

######  Proof 5.13.

Given a collection of open pathwise-embeddings

$\displaystyle
F^{\mathbb{C}_{1}}(A_{1})\xleftarrow{f_{1}}Z_{1}\xrightarrow{g_{1}}F^{\mathbb{C}_{1}}(B_{1}),\quad\dots\
,\ \
F^{\mathbb{C}_{n}}(A_{n})\xleftarrow{f_{n}}Z_{n}\xrightarrow{g_{n}}F^{\mathbb{C}_{n}}(B_{n})$

in $\mathsf{EM}(\mathbb{C}_{1}),\,\dots,\,\mathsf{EM}(\mathbb{C}_{n})$,
respectively, we wish to construct a pair of open pathwise embeddings

$\displaystyle F^{\mathbb{D}}(H(A_{1},\dots,A_{n}))\leftarrow Z\rightarrow
F^{\mathbb{D}}(H(B_{1},\dots,B_{n}))$ (14)

in $\mathsf{EM}(\mathbb{D})$.

Since there is a Kleisli law $\kappa\colon\mathbb{D}\circ H\Rightarrow
H\circ\prod_{i}\mathbb{C}_{i}$, we know by Theorem 14 that $H$ lifts to
$\widehat{H}\colon\prod_{i}\mathsf{EM}(\mathbb{C}_{i})\to\mathsf{EM}(\mathbb{D})$.
Also, since $H$ preserves embeddings, we know that (S1) holds by Proposition
5.4. Furthermore, (S2) holds too by Proposition 5.11 because we assumed that
$\kappa$ satisfies (S2’). Consequently, by Theorem 5.8, $\widehat{H}$ sends
tuples of open pathwise-embeddings to open pathwise-embeddings.

We obtain a pair of open pathwise-embeddings

${\widehat{H}(\vv{F^{\mathbb{C}_{i}}(A_{i})})}$${\widehat{H}(\vv{Z_{i}}\mkern
1.0mu)}$${\widehat{H}(\vv{F^{\mathbb{C}_{i}}(B_{i})})}$$\scriptstyle{\widehat{H}(\vv{f_{i}}\mkern
1.0mu)}$$\scriptstyle{\widehat{H}(\vv{g_{i}}\mkern 1.0mu)}$

as the morphisms of coalgebras $f_{1},\dots,f_{n}$ and $g_{1},\dots,g_{n}$ are
open pathwise-embeddings too.

Finally, we recall that, by Theorem 14,

$F^{\mathbb{D}}(H(\vv{A_{i}}\mkern
1.0mu))\cong\widehat{H}(\vv{F^{\mathbb{C}_{i}}(A_{i})}))\quad\mbox{and}\quad
F^{\mathbb{D}}(H(\vv{B_{i}}\mkern
1.0mu))\cong\widehat{H}(\vv{F^{\mathbb{C}_{i}}(B_{i})})).$

This gives us that $\widehat{H}(f_{1},\dots,f_{n})$ and
$\widehat{H}(g_{1},\dots,g_{n})$ are of the required type, as in (14).

Recall that the requirement that $\mathsf{EM}(\mathbb{D})$ has equalisers in
Theorem 5.12 holds automatically in our examples, by Corollary 14.

We can apply Theorem 5.12 to show that $\equiv_{{\mathbb{P}_{k}}}$ is
preserved by taking disjoint unions of structures. As the functor $\uplus$
preserves embeddings, we only have to check (S2’) for the Kleisli law
$\kappa_{A_{1},A_{2}}\colon{\mathbb{P}_{k}}(A_{1}\uplus
A_{2})\to{\mathbb{P}_{k}}(A_{1})\uplus{\mathbb{P}_{k}}(A_{2})$ defined in
Example 3.1. For a path $(P,\pi)$ in $\mathsf{EM}({\mathbb{P}_{k}})$, consider
a morphism $f\colon P\rightarrow A_{1}\uplus A_{2}$ , where
$(A_{1},\alpha_{1})$ and $(A_{2},\alpha_{2})$ are
${\mathbb{P}_{k}}$-coalgebras, and $f$ makes the following diagram of (S2’)
commute.

${P}$${A_{1}\uplus
A_{2}}$${{\mathbb{P}_{k}}(P)}$${{\mathbb{P}_{k}}(\alpha_{1}\uplus\alpha_{2})}$${{\mathbb{P}_{k}}(A_{1})\uplus{\mathbb{P}_{k}}(A_{2})}$$\scriptstyle{f}$$\scriptstyle{\pi}$$\scriptstyle{\alpha_{1}\uplus\alpha_{2}}$$\scriptstyle{{\mathbb{P}_{k}}(f)}$$\scriptstyle{\kappa}$

Recall from Remark 9 that the coalgebra map $\pi$ defines a forest order
$\sqsubseteq_{\pi}$ on the universe of $P$, and similarly for coalgebra maps
$\alpha_{1},\alpha_{2}$. Furthermore, since $(P,\pi)$ is a path,
$(P,\sqsubseteq_{\pi})$ is a finite linear order
$x_{1}\sqsubseteq_{\pi}\dots\sqsubseteq_{\pi}x_{n}$.

We may assume without loss of generality that $f(x_{n})$ is in $A_{1}$. Then,
$(\alpha_{1}\uplus\alpha_{2})(f(x_{i}))$ gives a word in
${\mathbb{P}_{k}}(\alpha_{1})$, which forms a finite linear order in the
$\sqsubseteq_{\alpha_{i}}$ order. By commutativity of the above diagram, this
must be the same word as the down-to-right composition
$\kappa({\mathbb{P}_{k}}(f)(\pi(x_{n})))$. But, by definition, the latter is
just the reduction of the word on elements $f(x_{1}),\dots,f(x_{n})$ to the
positions where $f(x_{i})\in A_{1}$.

The same reasoning applies for the largest $j$ such that $f(x_{j})$ is in
$A_{2}$. Each of the two words obtained this way yields a path embedding
$e_{i}\colon(P_{i},\pi_{i})\rightarrowtail(A_{i},\alpha_{i})$ as the embedding
of the induced substructure of $A_{i}$ on given word letters. Define a
morphism $e_{0}\colon P\rightarrow P_{1}\uplus P_{2}$ by sending an element to
its image under $f$. By construction, $(e_{1}\uplus e_{2})\circ e_{0}$ forms a
decomposition of $f$ and minimality of this decomposition is immediate, as any
other decomposition of $f$ would contain $P_{i}$ as a subpath. We obtain the
following FVM theorem for the $k$ variable fragment:

$\displaystyle A_{1}\equiv_{{\mathbb{P}_{k}}}B_{1}\enspace\mbox{and}\enspace
A_{2}\equiv_{{\mathbb{P}_{k}}}B_{2}$ $\displaystyle\mbox{implies}\quad
A_{1}\uplus A_{2}\equiv_{{\mathbb{P}_{k}}}B_{1}\uplus B_{2}$

The same reasoning goes through for ${\mathbb{P}_{k}}$ and ${\mathbb{E}_{k}}$
with coproducts over any index set $I$ and for ${\mathbb{M}_{k}}$ with
$\stackrel{{\scriptstyle R}}{{\vee}}$ from Example 3.1.

##  6\. FVM theorems for existential fragments

In [ALR] it is observed that we can also express preservation of existential
formulas naturally in the setting of game comonads. Recall that _existential
formulas_ are first-order formulas without universal quantifiers and with
negation only in front of atoms. Define

  * •

$A\Rrightarrow_{\exists\mathbb{C}}B$ if there exists a pathwise-embedding
$F^{\mathbb{C}}(A)\to F^{\mathbb{C}}(B)$.

Then, it follows that $A\Rrightarrow_{\exists{\mathbb{E}_{k}}}B$ iff, for
every existential sentence $\varphi$ of quantifier depth at most $k$,
$A\models\varphi$ implies $B\models\varphi$. A similar statement holds for
$A\Rrightarrow_{\exists{\mathbb{P}_{k}}}B$ and the $k$-variable restriction of
the existential fragment [AR23].

It turns out that under the same conditions as in Theorem 5.12 we have a
preservation theorem for $\Rrightarrow_{\exists\mathbb{C}}$. To do so, we
weaken axiom (S2’) to a new axiom which no longer requires the decomposition
to be minimal, that is, we define:

  1. (S2”)

For any path $(P,\pi)$ in $\mathsf{EM}(\mathbb{D})$ and coalgebras
$(A_{i},\alpha_{i})$ in $\mathsf{EM}(\mathbb{C}_{i})$ for $1\leq i\leq n$,
every heteromorphism $\pi\to[\vv{\alpha_{i}}\mkern 1.0mu]$ has _some_
decomposition through

$H(\vv{e_{i}}\mkern 1.0mu)\colon H(\vv{P_{i}})\to H(\vv{A_{i}}),$

for some path embeddings
$e_{i}\colon(P_{i},\pi_{i})\rightarrowtail(A_{i},\alpha_{i})$.

The corresponding FVM theorem for the existential fragments is as follows.
Note that (S2’) implies (S2”) and so any FVM theorem about the full fragment
that we state in this text automatically entails an analogous statement for
the existential fragment.

######  Theorem 24.

Let $H\colon\prod\nolimits_{i}\mathcal{C}_{i}\to\mathcal{D}$,
$\mathbb{C}_{1},\dots,\mathbb{C}_{n}$ and $\mathbb{D}$ be exactly as in
Theorem 5.12, except that instead of (S2’) we only require (S2”) for the
Kleisli law $\mathbb{D}\circ H\Rightarrow
H\circ\prod\nolimits_{i}\mathbb{C}_{i}$. Then

$A_{1}\Rrightarrow_{\exists\mathbb{C}_{1}}B_{1},\;\ldots,\;A_{n}\Rrightarrow_{\exists\mathbb{C}_{n}}B_{n}$

implies

$H(A_{1},\dots,A_{n})\;\Rrightarrow_{\exists\mathbb{D}}\;H(B_{1},\dots,B_{n}).$

######  Proof 6.1.

Observe that in the proof of Lemma 22 the minimality of the decomposition was
not needed. Further observe that the variant of (S2) where minimality is not
required is obtained from (S2”) by the same proof as for Proposition 5.11.
Consequently, we see that the lifting
$\widehat{H}\colon\prod\nolimits_{i}\mathsf{EM}(\mathbb{C}_{i})\to\mathsf{EM}(\mathbb{D})$
of $H$ preserves pathwise-embeddings.

Then, from
$A_{1}\Rrightarrow_{\exists\mathbb{C}_{1}}B_{1},\;\ldots,\;A_{n}\Rrightarrow_{\exists\mathbb{C}_{n}}B_{n}$,
witnessed by pathwise-embeddings

$f_{1}\colon F^{\mathbb{C}_{1}}(A_{1})\to
F^{\mathbb{C}_{2}}(B_{2}),\;\ldots,\;f_{n}\colon F^{\mathbb{C}_{n}}(A_{n})\to
F^{\mathbb{C}_{n}}(B_{n})$

we obtain a pathwise embedding

$\widehat{H}(f_{1},\ldots,f_{n})\colon\widehat{H}(F^{\mathbb{C}_{1}}(A_{1}),\ldots,F^{\mathbb{C}_{n}}(A_{n}))\to\widehat{H}(F^{\mathbb{C}_{1}}(B_{1}),\ldots,F^{\mathbb{C}_{n}}(B_{n})).$

Finally, since $\widehat{H}$ commutes with the cofree functors, i.e.
$\widehat{H}(F^{\mathbb{C}_{1}}(A_{1}),\ldots,F^{\mathbb{C}_{n}}(A_{n}))=F^{\mathbb{D}}(H(A_{1},\dots,A_{n}))$,
we have the required relation
$H(A_{1},\dots,A_{n})\Rrightarrow_{\exists\mathbb{D}}H(B_{1},\dots,B_{n})$.

##  7\. Abstract FVM theorems for products

In this section we show that FVM theorems for the operation of the categorical
product of two structures are automatic, regardless of the chosen comonad.
This shows the power of the categorical approach since the theorem applies to
any situation where logical equivalence admits a comonadic characterisation.

Recall that the (categorical) product $\prod_{i}A_{i}$ in the category
$\mathcal{R}(\sigma)$, indexed by a set $I$, is the $\sigma$-structure with
the universe being the product of the underlying universes $\prod_{i}A_{i}$.
Further, for a relation $R$ in $\sigma$, define its realisation in the product
by

$R^{\prod_{i}A_{i}}(\overline{a}_{1},\dots,\overline{a}_{n})\iff\ (\forall i)\
\ R^{A_{i}}(a_{1,i},\,\dots,\,a_{n,i})$

This operation obeys the usual universal property of categorical products.
Namely, for any object $C$ and morphisms $h_{i}\colon C\to A_{i}$ for each
$i\in I$, there is a _unique_ morphism $\overline{h}\colon C\to\prod_{i}A_{i}$
such that, for every $i\in I$,

${C}$${\prod_{i}A_{i}}$${A_{i}}$$\scriptstyle{\overline{h}}$$\scriptstyle{h_{i}}$$\scriptstyle{\pi_{i}}$

where $\pi_{i}\colon\prod_{i}A_{i}\to A_{i}$ is the $i$th projection. In case
of products of relational structures, $\overline{h}$ sends $c$ to the tuple
$(h_{i}(c))_{i\in I}$. Products in $\mathcal{R}_{*}(\sigma)$ work similarly,
with the distinguished element of $\prod_{i}(A_{i},a_{i})$ being the tuple
$(a_{i})_{i}$.

###  7.1. The positive existential and counting fragments

We fix an arbitrary comonad $\mathbb{C}$ on a category $\mathcal{C}$ with
products. Observe that, for a family of objects $\\{A_{i}\\}_{i}$ of
$\mathcal{C}$, indexed by a set $I$, we have morphisms
$\mathbb{C}(\pi_{i})\colon\mathbb{C}(\prod\nolimits_{i}A_{i})\to\mathbb{C}(A_{i})$
for each $i\in I$ and, by the universal property of products, also the
morphism

$\kappa_{\vv{A_{i}}\mkern
1.0mu}\colon\mathbb{C}(\prod\nolimits_{i}A_{i})\to\prod\nolimits_{i}\mathbb{C}(A_{i}).$

Applying Theorem 3 immediately yields the following FVM theorem for positive
existential fragments.

######  Theorem 25.

Given collections of $\sigma$-structures $\\{A_{i}\\}_{i\in I}$ and
$\\{B_{i}\\}_{i\in I}$, indexed by a common set $I$, and a comonad
$\mathbb{C}$ on a category $\mathcal{C}$ with products. Then,

$\textstyle\left(\forall i\in
I.\;A_{i}\Rrightarrow_{\exists^{+}\mathbb{C}_{i}}B_{i}\right)\quad\mbox{implies}\quad\prod_{i}A_{i}\Rrightarrow_{\exists^{+}\mathbb{C}_{i}}\prod_{i}B_{i}.$

A direct calculation reveals that $\kappa$ is natural in the choice of
$\\{A_{i}\\}_{i}$ and, furthermore, is a Kleisli law.

######  Lemma 26.

$\kappa$ is a Kleisli law.

######  Proof 7.1.

First, observe that by the definition of products and how $\kappa$ is defined,
we have that

$\mathbb{C}(\pi_{i})=\pi_{i}\circ\kappa$ (15)

for every $i$. From this we show commutativity of the following diagram.

${\mathbb{C}\left(\prod_{i}A_{i}\right)}$${\prod_{i}\mathbb{C}(A_{i})}$${\prod_{i}A_{i}}$${\prod_{i}A_{i}}$${A_{i}}$$\scriptstyle{\kappa}$$\scriptstyle{\varepsilon}$$\scriptstyle{\prod_{i}\varepsilon}$$\scriptstyle{\pi_{i}}$$\scriptstyle{\pi_{i}}$

By universality of the products, this implies the counit axiom of Kleisli laws
that is (K1) for the operation $H(\vv{A_{i}}\mkern 1.0mu)=\prod_{i}A_{i}$. To
show commutativity of the pentagon above, compute:

$\displaystyle\pi_{i}\circ\left(\prod\nolimits_{i}\varepsilon\right)\circ\kappa$
$\displaystyle=\varepsilon\circ\pi_{i}\circ\kappa$ products
$\displaystyle=\varepsilon\circ\mathbb{C}(\pi_{i})$
$\displaystyle\eqref{eq:prod-prop}$ $\displaystyle=\pi_{i}\circ\varepsilon$
naturality

Next, to show (K2) for the operation $H(\vv{A_{i}}\mkern
1.0mu)=\prod_{i}A_{i}$, we employ the same strategy. We wish to show
commutativity of the following diagram.

${\mathbb{C}(\prod_{i}A_{i})}$${\prod_{i}\mathbb{C}(A_{i})}$${\mathbb{C}^{2}(\prod_{i}A_{i})}$${\mathbb{C}(\prod_{i}\mathbb{C}(A_{i}))}$${\prod_{i}\mathbb{C}^{2}(A_{i})}$${\prod_{i}\mathbb{C}^{2}(A_{i})}$${\mathbb{C}^{2}(A_{i})}$$\scriptstyle{\kappa}$$\scriptstyle{\delta}$$\scriptstyle{\prod_{i}\delta}$$\scriptstyle{\mathbb{C}(\kappa)}$$\scriptstyle{\kappa}$$\scriptstyle{\pi_{i}}$$\scriptstyle{\pi_{i}}$

To do so, we compute:

$\displaystyle\pi_{i}\circ\left(\prod\nolimits_{i}\delta\right)\circ\kappa$
$\displaystyle=\delta\circ\pi_{i}\circ\kappa$ products
$\displaystyle=\delta\circ\mathbb{C}(\pi_{i})$ $\displaystyle\eqref{eq:prod-
prop}$ $\displaystyle=\mathbb{C}^{2}(\pi_{i})\circ\delta$ naturality
$\displaystyle=\mathbb{C}(\pi_{i})\circ\mathbb{C}(\kappa)\circ\delta$
$\displaystyle\eqref{eq:prod-prop}$
$\displaystyle=\pi_{i}\circ\kappa\circ\mathbb{C}(\kappa)\circ\delta$
$\displaystyle\eqref{eq:prod-prop}$

As a corollary of Lemma 26 and Theorem 4.2, we obtain an abstract FVM for
counting fragments.

######  Theorem 27.

Given the same assumptions as in Theorem 25,

$\textstyle\left(\forall i\in
I.\;A_{i}\equiv_{\\#\mathbb{C}}B_{i}\right)\quad\mbox{implies}\quad\prod_{i}A_{i}\equiv_{\\#\mathbb{C}}\prod_{i}B_{i}.$

###  7.2. The full fragments

We also have an FVM theorem for products and the equivalence
$\equiv_{\mathbb{C}}$. We prove this by checking the assumptions of Theorem
5.12. We first check that products preserve embeddings.

######  Lemma 28.

Let $\mathcal{C}$ be a category with products and a weak factorisation system
$(\mathcal{E},\mathcal{M})$. Then, for any collection of embeddings
$\\{m_{i}\colon C_{i}\rightarrowtail D_{i}\\}_{i}$ the product
$\prod_{i}m_{i}\colon\prod_{i}C_{i}\to\prod_{i}D_{i}$ is an embedding too.

######  Proof 7.2.

From the definition of weak factorisation systems it is enough to show that
$\prod_{i}m_{i}$ is weakly orthogonal to any quotient $e\in\mathcal{E}$, i.e.
$e\pitchfork\prod_{i}m_{i}$. To this end, assume we have the following a
commutative square.

${A}$${B}$${\prod_{i}C_{i}}$${\prod_{i}D_{i}}$$\scriptstyle{e}$$\scriptstyle{f}$$\scriptstyle{g}$$\scriptstyle{\prod_{i}m_{i}}$

Upon fixing $i$, we can compose this square with the naturality square for
product projections.

${\prod_{i}C_{i}}$${\prod_{i}D_{i}}$${C_{i}}$${D_{i}}$$\scriptstyle{\pi_{i}}$$\scriptstyle{\prod_{i}m_{i}}$$\scriptstyle{\pi_{i}}$$\scriptstyle{m_{i}}$

Then, since $e\pitchfork m_{i}$, there is some $d_{i}\colon B\to C_{i}$ such
that $d_{i}\circ e=\pi_{i}\circ f$ and $m_{i}\circ d=\pi_{i}\circ g$.

Set $\langle\vv{d_{i}}\mkern 1.0mu\rangle$ to be the unique morphism
$B\to\prod_{i}C_{i}$ obtained from the cone $\\{d_{i}\colon B\to C_{i}\\}_{i}$
and the universal property of products. Observe that

$\pi_{i}\circ\langle\vv{d_{i}}\mkern 1.0mu\rangle\circ e=d_{i}\circ
q=\pi_{i}\circ f$

which gives $\pi_{i}\circ\langle\vv{d_{i}}\mkern 1.0mu\rangle=f$ and,
similarly,

$\pi_{i}\,\circ\,\prod\nolimits_{i}m_{i}\,\circ\,\langle\vv{d_{i}}\mkern
1.0mu\rangle=m_{i}\circ\pi_{i}\circ\langle\vv{d_{i}}\mkern
1.0mu\rangle=m_{i}\circ d_{i}=\pi_{i}\circ g$

which gives the second required equation, i.e.
$\prod_{i}m_{i}\circ\langle\vv{d_{i}}\mkern 1.0mu\rangle=g$.

Recall that in order to specify $\equiv_{\mathbb{C}}$ we need
$\mathsf{EM}(\mathbb{C})$ to be a path category, that is, it comes equipped
with a proper factorisation system
$(\overline{\mathcal{E}},\overline{\mathcal{M}})$ and a choice of path objects
$\mathcal{P}\subseteq\mathsf{EM}(\mathbb{C})$. As before, we consider the
setting where $(\overline{\mathcal{E}},\overline{\mathcal{M}})$ is obtained as
the lifting of a proper factorisation system $(\mathcal{E},\mathcal{M})$ on
the base category $\mathcal{C}$, as in Lemma 12. In this case, a morphism of
coalgebras $(A,\alpha)\to(B,\beta)$ is a quotient (i.e. is in
$\overline{\mathcal{E}}$) if the underlying morphisms $A\to B$ is quotient
(i.e. is in $\mathcal{E}$).

The crucial requirement of our abstract FVM theorems for products is that
_paths are closed under quotients_ , that is, for any quotient

$X\twoheadrightarrow Y$

if $X$ is a path then so is $Y$. The following lemma shows that this is a
sufficient requirement for our path category $\mathsf{EM}(\mathbb{C})$ to
ensure the second assumption of Theorem 5.12.

######  Lemma 29.

If $\mathbb{C}$ preserves embeddings and paths are closed under quotients in
$\mathsf{EM}(\mathbb{C})$, then $H(\vv{A_{i}}\mkern 1.0mu)=\prod_{i}A_{i}$
satisfies axiom (S2’).

######  Proof 7.3.

We assume that $(Q,\rho)$ is a path in $\mathsf{EM}(\mathbb{C})$ and
$(A_{i},\alpha_{i})$ are arbitrary $\mathbb{C}$-coalgebras. Further, assume
that we are given a morphism $f\colon P\to\prod_{i}A_{i}$ which makes the
following diagram commute.

${Q}$${\prod_{i}A_{i}}$${\mathbb{C}(Q)}$${\mathbb{C}(\prod_{i}A_{i})}$${\prod_{i}\mathbb{C}(A_{i})}$$\scriptstyle{f}$$\scriptstyle{\rho}$$\scriptstyle{\prod_{i}\alpha_{i}}$$\scriptstyle{\mathbb{C}(f)}$$\scriptstyle{\kappa}$

It is an easy observation that the composition $\pi_{i}\circ f$ with the $i$th
projection $\pi_{i}\colon\prod_{i}A_{i}\to A_{i}$ is a coalgebra morphism
$(Q,\rho)\to(A_{i},\alpha_{i})$. Since $\mathbb{C}$ preserves embeddings,
Lemma 12 applies and we can take the factorisation of this morphism in
$\mathsf{EM}(\mathbb{C})$ as

${(Q,\rho)}$${(Q_{i},\rho_{i})}$${(A_{i},\alpha_{i})}$$\scriptstyle{q_{i}}$$\scriptstyle{e_{i}}$

where $q_{i}$ is a quotient and $e_{i}$ is an embedding. Since $(Q,\rho)$ is a
path and $q_{i}$ is a quotient, we see that $(Q_{i},\rho_{i})$ is a path by
our assumptions. Consequently, we have a decomposition of $f$ into

${Q}$${\prod_{i}Q_{i}}$${\prod_{i}A_{i}}$$\scriptstyle{q}$$\scriptstyle{\prod_{i}e_{i}}$
(16)

where $q$ is obtained from the universal property of products, from the
collection of morphisms $\\{q_{i}\\}_{i}$.

To show the minimality of this decomposition, let $f$ also decompose as

${Q}$${\prod_{i}S_{i}}$${\prod_{i}A_{i}}$$\scriptstyle{r}$$\scriptstyle{\prod_{i}m_{i}}$
(17)

where $m_{i}$ are path embeddings
$(S_{i},\omega_{i})\rightarrowtail(A_{i},\alpha_{i})$ in
$\mathsf{EM}(\mathbb{C})$. By post-composing both homomorphisms in (16) and
(17) with the projection $\pi_{i}\colon\prod_{i}A_{i}\to A_{i}$ we obtain a
commutative square:

${Q}$${Q_{i}}$${S_{i}}$${A_{i}}$$\scriptstyle{q_{i}}$$\scriptstyle{\pi_{i}\circ
r}$$\scriptstyle{e_{i}}$$\scriptstyle{m_{i}}$

Now, observe that $q_{i}$ is a quotient and $m_{i}$ is an embedding and so
there is a diagonal morphism $d_{i}\colon Q_{i}\to S_{i}$ such that
$e_{i}=m_{i}\circ d_{i}$. It remains to check is that $d_{i}$ is a morphism of
coalgebras $(Q_{i},\rho_{i})\to(S_{i},\omega_{i})$. This is a consequence of
the fact that $\mathbb{C}(m_{i})$ is an embedding and that the right square
and the surrounding rectangle of the following diagram commute.

${Q_{i}}$${S_{i}}$${A_{i}}$${\mathbb{C}(Q_{i})}$${\mathbb{C}(S_{i})}$${\mathbb{C}(A_{i})}$$\scriptstyle{d_{i}}$$\scriptstyle{\rho_{i}}$$\scriptstyle{m_{i}}$$\scriptstyle{\omega_{i}}$$\scriptstyle{\alpha_{i}}$$\scriptstyle{\mathbb{C}(d_{i})}$$\scriptstyle{\mathbb{C}(m_{i})}$

Indeed, let $x\in Q_{i}$. By chasing the above diagram we obtain

$\displaystyle\mathbb{C}(m_{i})\circ\omega_{i}\circ d_{i}=\alpha_{i}\circ
m_{i}\circ d_{i}=\mathbb{C}(m_{i})\circ\mathbb{C}(d_{i})\circ\rho_{i}$

and since $\mathbb{C}(m_{i})$ is a monomorphism $\omega_{i}\circ
d_{i}=\mathbb{C}(d_{i})\circ\rho_{i}$, as required.

To summarise, we have shown that any category $\mathcal{C}$ with products
admits a Kleisli law for any comonad $\mathbb{C}$ on $\mathcal{C}$ (Lemma 26).
If, furthermore, $\mathsf{EM}(\mathbb{C})$ has equalisers then $\prod_{i}$
automatically satisfies assumptions of Theorem 5.12 by Lemmas 28 and 29.

As a corollary we obtain a general FVM theorem for products, with assumptions
that hold true for all the game comonads studied so far in the literature (cf.
Example 7.2 below).

######  Theorem 30.

Let $\mathbb{C}$ be a comonad on a category $\mathcal{C}$ with products, such
that $\mathsf{EM}(\mathbb{C})$ is a path category. If
$\mathsf{EM}(\mathbb{C})$ has equalisers and paths closed under quotients then

$\textstyle\left(\forall i\in
I.\;A_{i}\equiv_{\mathbb{C}}B_{i}\right)\quad\mbox{implies}\quad\prod_{i}A_{i}\,\equiv_{\mathbb{C}}\,\prod_{i}B_{i}.$

As a consequence of Corollary 14 we obtain the following specialised version
of the above theorem.

######  Corollary 31.

If a comonad $\mathbb{C}$ on $\mathcal{R}(\sigma)$ or
$\mathcal{R}_{*}(\sigma)$ preserves embeddings and if
$\mathsf{EM}(\mathbb{C})$ is a path category with paths closed under
quotients, then

$\textstyle\left(\forall i\in
I.\;A_{i}\equiv_{\mathbb{C}}B_{i}\right)\quad\mbox{implies}\quad\prod_{i}A_{i}\,\equiv_{\mathbb{C}}\,\prod_{i}B_{i}.$

In the case of ${\mathbb{E}_{k}}$, it is immediate that ${\mathbb{E}_{k}}$
preserves embeddings. Furthermore, for a surjective coalgebra morphism
$(P,\pi)\to(A,\alpha)$ in $\mathsf{EM}({\mathbb{E}_{k}})$ such that $(P,\pi)$
is a path, we also have that $(A,\alpha)$ is a path since, in view of Remark
9, we map a finite linear order onto a forest.

The same is true for our example comonads ${\mathbb{P}_{k}}$,
${\mathbb{M}_{k}}$, yielding product FVM theorems for the bounded quantifier
rank, bounded variable and bounded modal depth fragments and their positive
existential and counting variants.

More generally, the assumptions of Theorem 31 hold for any comonad
$\mathbb{C}$ which preserves embeddings and such that the category
$\mathsf{EM}(\mathbb{C})$ is an _arboreal category_ , in sense of [AR21], by
Lemma 3.5 therein.

In particular, all FVM theorems for products from this section hold for
_hybrid logic_ because of the hybrid comonad of [AM22], _guarded logics_
captured by guarded comonads in [AM21], the _bounded conjunction_ and _bounded
quantifier rank_ fragments of the $k$-variable first-order logic captured in
[MS22] and [Pai20], respectively.

##  8\. Adding equality and other enrichments

Recall that the relations $\equiv_{{\mathbb{E}_{k}}}$ and
$\equiv_{{\mathbb{P}_{k}}}$ express logical equivalence with respect to the
logic _without_ equality. The standard way to add equality to the language is
to extend the signature $\sigma$ with an additional binary relation symbol
$I(\cdot,\cdot)$, and provide a _translation_
$\mathfrak{t}^{I}\colon\mathcal{R}(\sigma)\to\mathcal{R}(\sigma\cup\\{I\\})$
which interprets this new relational symbol as equality, i.e.
$\mathfrak{t}^{I}(A)$ is the $\sigma\cup\\{I\\}$-structure extension of $A$ by
setting $I(a,b)$ if and only if $a=b$. Since our game comonads are defined
uniformly for any signature, they are also defined over
$\mathcal{R}(\sigma\cup\\{I\\})$, giving us:

  * •

$\mathfrak{t}^{I}(A)\equiv_{{\mathbb{E}_{k}}}\mathfrak{t}^{I}(B)$ iff $A$ and
$B$ are logically equivalent w.r.t. the fragment of first-order logic
consisting of formulas of quantifier depth ${\leq}\,k$ with equality, and

  * •

$\mathfrak{t}^{I}(A)\equiv_{{\mathbb{P}_{k}}}\mathfrak{t}^{I}(B)$ iff $A$ and
$B$ are logically equivalent w.r.t. the fragment of first-order logic
consisting of formulas in $k$-variables with equality.

Moreover, an operation which commutes with the translation $\mathfrak{t}^{I}$
lifts FVM theorems for fragments without equality to fragments with equality.
For example, disjoint unions satisfy that $\mathfrak{t}^{I}(A\uplus
B)=\mathfrak{t}^{I}(A)\uplus\mathfrak{t}^{I}(B)$ and, therefore, if
$\mathfrak{t}^{I}(A_{1})\equiv_{{\mathbb{E}_{k}}}\mathfrak{t}^{I}(B_{1})$, and
$\mathfrak{t}^{I}(A_{2})\equiv_{{\mathbb{E}_{k}}}\mathfrak{t}^{I}(B_{2})$,
then

$\displaystyle\mathfrak{t}^{I}(A_{1}\uplus A_{2})$
$\displaystyle\enspace=\enspace\mkern
8.0mu\mathfrak{t}^{I}(A_{1})\uplus\mathfrak{t}^{I}(A_{2})$
$\displaystyle\enspace\equiv_{{\mathbb{E}_{k}}}\mathfrak{t}^{I}(B_{1})\uplus\mathfrak{t}^{I}(B_{2})=\mathfrak{t}^{I}(B_{1}\uplus
B_{2})$

which shows that $A_{1}\uplus A_{2}$ and $B_{1}\uplus B_{2}$ are logically
equivalent w.r.t. formulas of quantifier depth ${\leq}\,k$ with equality.

In general, similar translations can be used for other logic extensions. For
example, in [BU22] a translation is used to obtain description logics using
${\mathbb{M}_{k}}$. Nevertheless, the above technique applies verbatim to
varying translations, operations and logics. We arrive at the following simple
but important fact, that greatly increases the applicability of the results in
the previous sections. thmCommutativityWithTranslations For $1\leq i\leq n+1$,
let $\mathcal{L}_{i}$ and $\mathcal{L}^{\prime}_{i}$ be logics and
$\mathfrak{t}_{i}$ a translation such that ${A\equiv_{\mathcal{L}_{i}}B}$ iff
${\mathfrak{t}_{i}(A)\equiv_{\mathcal{L}^{\prime}_{i}}\mathfrak{t}_{i}(B)}$.
Further, let $H^{\prime}$ be an $n$-ary operation satisfying the _FVM theorem
from $\mathcal{L}^{\prime}_{1},\dots,\mathcal{L}^{\prime}_{n}$ to
$\mathcal{L}^{\prime}_{n+1}$_, with respect to translated structures. That is:

$\mathfrak{t}_{1}(A_{1})\equiv_{\mathcal{L}^{\prime}_{1}}\mathfrak{t}_{1}(B_{1}),\;\ldots,\;\mathfrak{t}_{n}(A_{n})\equiv_{\mathcal{L}^{\prime}_{n}}\mathfrak{t}_{n}(B_{n})$

implies

$H^{\prime}(\vv{\mathfrak{t}_{i}(A_{i})})\equiv_{\mathcal{L}^{\prime}_{n+1}}H^{\prime}(\vv{\mathfrak{t}_{i}(B_{i})})$

If $H$ commutes with the translations in the sense that
$H^{\prime}(\vv{\mathfrak{t}_{i}(A_{i})})\cong\mathfrak{t}_{n+1}(H(\vv{A_{i}}\mkern
1.0mu))$, then $H$ satisfies the FVM theorem from
$\mathcal{L}_{1},\dots,\mathcal{L}_{n}$ to $\mathcal{L}_{n+1}$. That is:

$A_{1}\equiv_{\mathcal{L}_{1}}B_{1},\;\ldots,\;A_{n}\equiv_{\mathcal{L}_{n}}B_{n}\quad\mbox{implies}\quad
H(\vv{A_{i}}\mkern 1.0mu)\equiv_{\mathcal{L}_{n+1}}H(\vv{B_{i}}\mkern 1.0mu)$

######  Proof 8.1.

Assume that $A_{i}\equiv_{\mathcal{L}_{i}}B_{i}$, for every $i=1,\dots,n$. By
our assumptions, we obtain that
$\mathfrak{t}_{i}(A_{i})\equiv_{\mathcal{L}^{\prime}_{i}}\mathfrak{t}_{i}(B_{i})$
for every $i=1,\dots,n$ and, therefore,

$H^{\prime}(\mathfrak{t}_{1}(A_{1}),\dots,\mathfrak{t}_{n}(A_{n}))\equiv_{\mathcal{L}^{\prime}_{n+1}}H^{\prime}(\mathfrak{t}_{1}(B_{1}),\dots,\mathfrak{t}_{n}(B_{n}))$

Then, by a straightforward calculation

$\displaystyle\mathfrak{t}_{n+1}(H(\vv{A_{i}}\mkern 1.0mu))\cong
H^{\prime}(\vv{\mathfrak{t}_{i}(A_{i})})\equiv_{\mathcal{L}^{\prime}_{n+1}}H^{\prime}(\vv{\mathfrak{t}_{i}(B_{i})})\cong\mathfrak{t}_{n+1}(H(\vv{B_{i}}\mkern
1.0mu))$

which, by our assumptions, implies that

$H(\vv{A_{i}}\mkern 1.0mu)\equiv_{\mathcal{L}_{n+1}}H(\vv{B_{i}}\mkern
1.0mu).$

Let
$\mathfrak{t}^{\texttt{com}}\colon\mathcal{R}(\sigma)\to\mathcal{R}(\sigma^{\texttt{com}})$
be a translation of $\sigma$-structures into the extension
$\sigma^{\texttt{com}}$ of $\sigma\cup\\{I\\}$ with an extra binary relation
$\texttt{com}(\cdot,\cdot)$. The interpretation of com in
$\mathfrak{t}^{\texttt{com}}(A)$ consists of all pairs $(a,b)$ appearing in
the same component of the Gaifman graph of $A$, that is, pairs $(a,b)$ such
that there is a path $a\leftrightsquigarrow
x_{1}\leftrightsquigarrow\dots\leftrightsquigarrow x_{n}\leftrightsquigarrow
b$ where $x\leftrightsquigarrow y$ holds whenever $x$ and $y$ are in a common
tuple in an $R^{A}$ of some $R\in\sigma$.

It is easy to see that
$\mathfrak{t}^{\texttt{com}}(A)\equiv_{{\mathbb{E}_{k}}}\mathfrak{t}^{\texttt{com}}(B)$
expresses logical equivalence in the bounded quantifier depth fragment
extended with the connectivity predicate, akin to [Boj21, SSV22]. Since
$\mathfrak{t}^{\texttt{com}}(A\uplus
B)\cong\mathfrak{t}^{\texttt{com}}(A)\uplus\mathfrak{t}^{\texttt{com}}(B)$, we
obtain, by Theorem 8 and Example 5.4, an FVM theorem for disjoint unions and
the quantifier rank $k$ fragment of said logic. While still being polynomial-
time computable, the connectivity relation is not definable in bounded
quantifier depth fragments of first-order logic, and so this is a proper
extension.

Continuing from Example 7.2, consider
$\mathfrak{t}\colon\mathcal{R}_{*}(\sigma)\to\mathcal{R}_{*}(\sigma^{G})$
where $\sigma^{G}$ is the extension of the modal signature $\sigma$ with the
_global relation_ $G(a,b)$, true in $\mathfrak{t}(A,a)$ for any pair of
elements. Then, it is immediate that
$\mathfrak{t}((A,a)\times(B,b))\cong\mathfrak{t}(A,a)\times\mathfrak{t}(B,b)$,
giving us by Theorem 8 an FVM theorem for products and modal logic with global
modalities.

As an example of Theorem 8 where the two operations differ, we consider the
notion of weak (bi)simulation where transitions along a distinguished relation
$S\in\sigma$ are considered to occur silently. We can model weak bisimulation
by considering bisimulation between translated structures where
$\mathfrak{t}\colon\mathcal{R}_{*}(\sigma)\to\mathcal{R}_{*}(\sigma)$ replaces
all relations $R$ with their closure under sequences of prior and subsequent
$S$ transitions.

For pointed structures $A_{1}=(A_{1},a_{1})$ and $A_{2}=(A_{2},a_{2})$, there
is an operation $A_{1}\vee A_{2}$ which adds a new initial point $\star$ to
$A_{1}\uplus A_{2}$. We extend the transitions with $R(\star,(i,x))$, for
$R\in\sigma$, whenever $R^{A_{i}}(a_{i},x)$ for some $i\in\\{1,2\\}$ and $x\in
A_{i}$. This construction satisfies $\mathfrak{t}(A_{1}\stackrel{{\scriptstyle
S}}{{\vee}}A_{2})\cong\mathfrak{t}(A_{1})\vee\mathfrak{t}(A_{2})$ by design,
and there is a Kleisli law

$\kappa_{A_{1},A_{2}}\colon{\mathbb{M}_{k}}(A_{1}\vee
A_{2})\rightarrow{\mathbb{M}_{k}}(A_{1})\vee{\mathbb{M}_{k}}(A_{2}),$

via a similar construction to that used in Example 3.1. This yields an FVM
theorem:

$\displaystyle A_{1}\Rrightarrow_{W_{k}}B_{1}\enspace\mbox{and}\enspace
A_{2}\Rrightarrow_{W_{k}}B_{2}$ $\displaystyle\mbox{implies}\quad
A_{1}\stackrel{{\scriptstyle
S}}{{\vee}}A_{2}\Rrightarrow_{W_{k}}B_{1}\stackrel{{\scriptstyle
S}}{{\vee}}B_{2}$

where $A\Rrightarrow_{W_{k}}B$ indicates that $A$ weakly simulates $B$ up to
depth $k$.

##  9\. Conclusion

We presented a categorical approach to the composition methods, and
specifically Feferman–Vaught–Mostowski theorems. We exploit game comonads to
encapsulate the logics and their model comparison games. Surprising
connections to classical constructions in category theory, and especially the
monad theory of bilinear maps emerged from this approach, cf. Section 5.1.

For finite model theorists, our work provides a novel high-level account of
many FVM theorems, abstracting away from individual logics and constructions.
Furthermore, concrete instances of these theorems are verified purely
semantically, by finding a suitable collection homomorphisms forming a Kleisli
law satisfying (S2’), instead of the usual delicate verification that
strategies of model comparison games compose. For game comonads, we provide a
much needed tool that enables us to handle logical relationships between
structures as they are transformed or viewed in terms of different logics.

The FVM results in this paper, combined with judicious use of the techniques
described in Section 8 can be pushed significantly further. FVM theorems and
the compositional method are of particular significance in the setting of
monadic second-order (MSO) logic [Gur85]. Exploiting the results we have
presented for the composition methods, a follow up paper will give a comonadic
semantics for MSO, and develop a semantic account of Courcelle’s algorithmic
meta-theorems [CE12].

The original theorem of Feferman–Vaught [FV59] is very flexible, including
incorporating structure on the indices of families of models to be combined by
an operation, as well as the models themselves. This aspect is currently
outside the scope of our comonadic methods. An ad-hoc adaptation of our
approach also gives a proof of the FVM theorem for free amalgamations, but
this does not follow directly from our theorems. Developing these extensions
is left to future work.

The present work bears some resemblance to Turi and Plotkin’s bialgebraic
semantics [TP97], a categorical model of structural operational semantics
(SOS) [G.D81]. Turi and Plotkin noticed that the SOS rules assigning behaviour
to syntax could be abstracted as a certain distributive law $\lambda$. An
algebra encodes the composition operations of the syntax, and a coalgebra the
behaviour. If this pair is suitably compatible with $\lambda$, forming a so-
called $\lambda$-bialgebra, then crucially bisimulation is a congruence with
respect to the composition operations. Both bialgebraic semantics and our work
presented in this paper give a categorical account of well-behaved composition
operations, with the interaction between composition and observable behaviour
mediated by some form of distributive law. There are also essential
differences: bialgebraic semantics typically focuses on assigning behaviour to
syntax, whereas FVM theorems encompass operations on models. Our FVM theorems
are parametric in a choice of logic or observable behaviour, while the notion
of bisimulation in bialgebraic semantics is fixed by the coalgebra signature
functor. The natural presence of positive existential and counting quantifier
variants of FVM theorems, and the incorporation of resource parameters, do not