Theory of computation Finite Model Theory Theory of computation Design and
analysis of algorithms University of Cambridge,
https://tomas.jakl.onetomas.jakl@cl.cam.ac.ukhttps://orcid.org/0000-0003-1930-4904
University of
Oxforddaniel.marsden@cs.ox.ac.ukhttps://orcid.org/0000-0003-0579-0323
University of
Oxfordnihil.shah@cs.ox.ac.ukhttps://orcid.org/0000-0003-2844-0828 T. Jakl, D.
Marsden and N. Shah Research supported by the EPSRC project EP/T00696X/1
“Resources and Co-Resources: a junction between categorical semantics and
descriptive complexity”.

# A game comonadic account of Courcelle and Feferman–Vaught–Mostowski theorems

Tomáš Jakl  Dan Marsden  Nihil Shah

###### Abstract

Game comonads, introduced by Abramsky, Dawar and Wang, and developed by
Abramsky and Shah, give a categorical semantics for model comparison games. We
present an axiomatic account of Feferman-Vaught-Mostowski (FVM) composition
theorems within the game comonad framework, parameterized by the model
comparison game. In a uniform way, we produce compositionality results for the
logic in question, and its positive existential and counting quantifier
variants.

Secondly, we extend game comonads to the second order setting, specifically in
the case of Monadic Second Order (MSO) logic. We then generalize our FVM
theorems to the second order case. We conclude with an abstract formulation of
Courcelle’s algorithmic meta-theorem, exploiting our earlier developments.
This is instantiated to recover well-known bounded tree-width and bounded
clique-width Courcelle theorems for MSO on graphs.

###### keywords:

game comonads, Courcelle’s theorem, Feferman–Vaught–Mostowski theorems

##  1 Introduction

Model comparison games, such as the Ehrenfeucht–Fraïssé [16, 19], pebbling
[28] and bisimulation games [23], play a key role in finite model theory [30].
Recent work has introduced a novel categorical semantics for these games [1,
4]. In this programme, a comonad is introduced for a chosen model comparison
game. This comonad is typically graded by a resource parameter, such as
quantifier depth or variable count. Winning Duplicator strategies for model
comparison games, bounded by the chosen resource parameter, can then be
uniformly characterized categorically, in terms of the Kleisli [25] and
Eilenberg-Moore [17] categories of the comonad.

This approach has been extended to more complex games, such as those for
guarded logics [2] and generalized quantifiers [9], and applications such as
Lovasz type theorems [14] and Rossman’s homomorphism theorem [38]. The
abstract setting was axiomatized in [3].

Our aim is to give a semantic account of algorithmic meta-theorems,
specifically Courcelle type theorems [12], exploiting the game comonadic
semantics. To do so, firstly we develop an axiomatic formulation of Feferman-
Vaught-Mostowski (FVM) theorems [36, 18], which describe how logical
equivalence is preserved under operations on models.

Pleasingly, the canonical categorical structures associated with the comonadic
approach play a central role. Specifically, we lift model transformations to
the Kleisli and Eilenberg-Moore categories via distributive laws satisfying
natural axioms. These axioms are semantic in nature, and parametric in the
notion of model equivalence. Contrast this with the more tautological, MSO
specific logical condition of MSOL-smoothness used to describe well-behaved
model transformations for the generic Courcelle theorem presented in [32]. Our
results yield FVM results for a given logic, it’s positive existential
fragment, and its extension to counting quantifiers in a uniform way.

Secondly, we identify a suitable comonad capturing the model comparison game
for monadic second order logic. FVM theorems often generalize to MSO [22, 21,
29, 41]. Our abstract approach to FVM theorems is then extended to the second-
order setting.

With these two components in place, we give an abstract Courcelle theorem,
parameterized by the game comonad and model transformations of interest. This
theorem is then instantiated to yield concrete results for bounded tree-width
[10] and bounded clique-width variants [13, 37] of Courcelle’s theorem.

##  2 Preliminaries

We assume the reader is already familiar with basic category theoretic notions
such as functors, natural transformations, adjunctions, and limits (see e.g.
[5] or [6]).

###  2.1 Game 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 a $\mathrm{obj}({\mathcal{C}})$-indexed family of morphisms
$\varepsilon_{A}\colon\mathbb{C}(A)\to A$. Lastly, there is a coextension
operation $(-)^{*}$ mapping 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^{*},$ (1)

It is then standard [33] that $\mathbb{C}$ is a functor such that
$\mathbb{C}(f)=(f\circ\varepsilon_{A})^{*}$, and the counit is a natural
transformation $\mathbb{C}\Rightarrow{Id}$. The morphisms
$\delta_{A}:=\mathrm{id}_{\mathbb{C}(A)}^{*}:\mathbb{C}(A)\rightarrow\mathbb{C}^{2}(A)$
form a _comultiplication_ natural transformation satisfying
$\varepsilon\circ\delta=\mathrm{id}=\mathbb{C}(\varepsilon)\circ\delta$ and
$\delta\circ\delta=\mathbb{C}(\delta)\circ\delta$.

Our comonads of interest shall be on the category of relational structures
over a fixed signature. A  _signature_ $\sigma$ is a set consisting of:

  1. 1.

_Relation symbols_ , each with a specified _arity_ , a strictly positive
natural number. A relation symbol of arity $n$ is referred to as _$n$ -ary_.
$\mathbf{rel}(\sigma)$ shall denote the subset of relation symbols.

  2. 2.

_Constant symbols_. $\mathbf{cs}(\sigma)$ shall denote the subset of constant
symbols.

A  _modal signature_ $\sigma$ has a single constant $c_{0}$ and
$\mathbf{rel}(\sigma)$ consisting of a single binary relation $E$, and
finitely many unary relations.

A $\sigma$-structure $A$ consists of a set $A$, referred to as the
_universe_. For each $R\in\mathbf{rel}(\sigma)$ of arity $n$, an $n$-ary
relation $R^{A}$ on $A$, and for each $c\in\mathbf{cs}(\sigma)$ an element
$c^{A}\in A$. A _morphism of $\sigma$-structures_ $f:A\rightarrow B$ is a
function of type $A\rightarrow B$, preserving relations and constants. That
is, for $n$-ary $R\in\mathbf{rel}(\sigma)$,
$R^{A}(a_{1},\ldots,a_{n})\Rightarrow R^{B}(f(a_{1}),\ldots,f(a_{n}))$, and
for $c\in\mathbf{cs}(\sigma)$, $f(c^{A})=c^{B}$. $\mathcal{R}(\sigma)$ shall
denote the category of $\sigma$-structures and morphisms between them.

We shall require three comonads on $\mathcal{R}(\sigma)$ for the examples in
later sections, parameterized by a positive integer $k$. These are small
generalizations of the key comonads appearing in [4], to handle signatures
with constants in a uniform way.

We shall write $A^{+}$ for the set of non-empty lists over $A$, and $A^{\leq
k}$ for its restriction to lists of at most $k$ elements.

Comonad $\mathbb{E}_{k}$:

The universe of $\mathbb{E}_{k}(A)$ is $A^{\leq k}\uplus\mathbf{cs}(\sigma)$.
For $c\in\mathbf{cs}(\sigma)$, define $c^{\mathbb{E}_{k}(A)}:=c$. The counit
preserves constants, and on lists $\varepsilon[a_{1},\dots,a_{n}]:=a_{n}$. For
$n$-ary $R\in\mathbf{rel}(\sigma)$,
$R^{\mathbb{E}_{k}(A)}(s_{1},\ldots,s_{n})$ iff the
$s_{i}\not\in\mathbf{cs}(\sigma)$ are pairwise comparable in the prefix order,
and $R^{A}(\varepsilon(s_{1}),\ldots,\varepsilon(s_{n}))$. For
$h:\mathbb{E}_{k}(A)\rightarrow B$, the coextension preserves constants, and
acts on lists as
$h^{*}([a_{1},\ldots,a_{n}]):=[h([a_{1}]),\ldots,h([a_{1},\ldots,a_{n}])]$.

Comonad $\mathbb{M}_{k}$:

We restrict to a modal signature. The universe of $\mathbb{M}_{k}(A)$ consists
of $\\{c_{0}\\}$ and the elements of $A^{\leq k}$ of the form
$[a_{1},\ldots,a_{n}]$ such that $E^{A}(c_{0}^{A},a_{1})$ and for $1\leq i<n$,
$E^{A}(a_{i},a_{i+1})$. The counit and coextension act as for
$\mathbb{E}_{k}$. We have $E^{\mathbb{M}_{k}(A)}(s,s^{\prime})$ iff either
$s=c_{0}$ and $s^{\prime}$ is a one element list, or $s$ and $s^{\prime}$ are
lists with $s^{\prime}$ covering $s$ in the prefix order. For unary
$P\in\mathbf{rel}(\sigma)$, $P^{\mathbb{M}_{k}(A)}(s)$ iff
$P^{A}(\varepsilon(s))$.

Comonad $\mathbb{P}_{k}$:

The universe of $\mathbb{P}_{k}(A)$ is $(\\{0,\ldots,k-1\\}\times
A)^{+}\,\uplus\,\mathbf{cs}(\sigma)$. Constant interpretations are defined as
for $\mathbb{E}_{k}$. The counit $\varepsilon$ preserves constants, and on
lists sends $[(p_{1},a_{1}),\dots,(p_{n},a_{n})]$ to $a_{n}$. We refer to the
first element in a pair $(p,a)$ as a  _pebble index_. For $n$-ary
$R\in\mathbf{rel}(\sigma)$, $R^{\mathbb{P}_{k}(A)}(s_{1},\ldots,s_{n})$ iff:

  1. 1.

The $s_{i}\not\in\mathbf{cs}(\sigma)$ are pairwise comparable in the prefix
order.

  2. 2.

For $s_{i},s_{j}\not\in\mathbf{cs}(\sigma)$ with $s_{i}\leq s_{j}$, the pebble
index of the tail of $s_{i}$ does not appear in the suffix of $s_{i}$ in
$s_{j}$.

  3. 3.

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

For $h\colon\mathbb{P}_{k}(A)\rightarrow B$, the coextension $h^{*}$ preserves
constants, and acts on lists 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}]))]$

######  Theorem 2.1.

$\mathbb{E}_{k}$, $\mathbb{M}_{k}$ and $\mathbb{P}_{k}$ are comonads in
Kleisli form (direct adaptation of [1, 4]).

###  2.2 Kleisli and Eilenberg–Moore categories

A comonad $\mathbb{C}$ on a category $\mathcal{C}$ gives rise to two
categories. The first is the _Kleisli category_ $\mathsf{Kl}(\mathbb{C})$
consisting of the same objects as $\mathcal{C}$ has, but morphisms from $A$ to
$B$ are $\mathcal{C}$-morphisms of type $\mathbb{C}(A)\to B$. The composition
of $f\colon\mathbb{C}A\to B$ and $g\colon\mathbb{C}B\to C$ is defined as
$g\circ f^{*}$, with the counits the identity morphisms. The equations (1)
ensure that $\mathsf{Kl}(\mathbb{C})$ is a well-formed category.

The second category induced by $\mathbb{C}$ is the _Eilenberg–Moore category
$\mathsf{EM}(\mathbb{C})$ of $\mathbb{C}$-coalgebras_. Its objects are pairs
$(A,\alpha)$ where $\alpha\colon A\to\mathbb{C}(A)$ is a
$\mathcal{C}$-morphism such that

$\varepsilon_{A}\circ\alpha=\mathrm{id}_{A}\enspace\text{and}\enspace\delta\circ\alpha=\mathbb{C}\alpha\circ\alpha,$
(2)

A _coalgebra morphism_ $h\colon(A,\alpha)\to(B,\beta)$ is a
$\mathcal{C}$-morphism $h\colon A\to B$ such that $\beta\circ
h=\mathbb{C}h\circ\alpha$. We shall simply write $\alpha$ instead of
$(A,\alpha)$ whenever $A$ can be inferred from the context.

${\mathsf{Kl}(\mathbb{C})}$${\mathsf{EM}(\mathbb{C})}$${\mathcal{C}}$$\scriptstyle{U_{\mathbb{C}}}$$\scriptstyle{K^{\mathbb{C}}}$$\scriptstyle{U^{\mathbb{C}}}$$\scriptstyle{F_{\mathbb{C}}}$

$\dashv$

$\scriptstyle{F^{\mathbb{C}}}$

$\dashv$

The two categories induce two adjunctions over the base category and a functor
$K^{\mathbb{C}}$ from $\mathsf{Kl}(\mathbb{C})$ to $\mathsf{EM}(\mathbb{C})$,
as depicted on the right. For our purposes it suffices to know that

  * •

$K^{\mathbb{C}}$ is a fully faithful functor such that $K^{\mathbb{C}}\circ
F_{\mathbb{C}}=F^{\mathbb{C}}$.

  * •

$F_{\mathbb{C}}$ is the identity on objects, and for $\mathcal{C}$-morphism
$f\colon A\to B$, $F_{\mathbb{C}}(f)=f\circ\varepsilon_{A}$.

  * •

$U^{\mathbb{C}}$ is the forgetful functor, sending $(A,\alpha)$ to $A$ and
$F^{\mathbb{C}}$ is the _cofree coalgebra_ functor, sending $A$ in
$\mathcal{C}$ to $(\mathbb{C}A,\delta_{A})$ and $f\colon A\to B$ in
$\mathcal{C}$ to $\mathbb{C}f$.

######  Remark 2.2.

A coalgebra $(A,\alpha)$ of any of the game comonads defined above is endowed
with a preorder $\sqsubseteq_{\alpha}$, where $x\sqsubseteq_{\alpha}y$
whenever the word $\alpha(x)$ is a prefix of $\alpha(y)$. Then, by (2),
$\alpha(y)$, for a non-constant $y$, is the word listing all non-constant $x$
such that $x\sqsubseteq_{\alpha}y$.

In fact, the category $\mathsf{EM}(\mathbb{E}_{k})$ is equivalent to the
category of $\sigma$-structures endowed with a compatible forest order of
depth ${\leq}\,k$, see section 9 in [4] for details.

###  2.3 Factorisation systems

_Strong homomorphisms_ in $\mathcal{R}(\sigma)$ are those homomorphisms
$f\colon A\to B$ that reflect relations, i.e. if $(f(x_{1}),\dots,f(x_{n}))\in
R^{B}$ then $(x_{1},\dots,x_{n})\in R^{A}$. Recall that any homomorphism
$h\colon A\to B$ in $\mathcal{R}(\sigma)$ factors into an onto homomorphism
$q\colon A\twoheadrightarrow h[A]$ followed by a strong injective homomorphism
$m\colon h[A]\rightarrowtail B$. Then, $h[A]$ above is the $\sigma$-structure
on the image $h[A]$ of $h$ so that the inclusion $h[A]\to B$ is a strong
homomorphism. This factorisation is a special case of a general categorical
structure which we review next.

A _factorisation system_ $(\mathcal{E},\mathcal{M})$ consists of a class of
morphisms $\mathcal{E}$ called _quotients_ , denoted by $\twoheadrightarrow$,
and a class of morphisms $\mathcal{M}$ called _embeddings_ , denoted by
$\rightarrowtail$, which are both closed under compositions, contain all
isomorphisms and, furthermore,

  * •

every morphism $f\colon A\to B$ has a factorisation $f=m\circ e$ for some
quotient $e\colon A\twoheadrightarrow C$ and embedding $m\colon
C\rightarrowtail B$, and

  * •

${A}$${B}$${C}$${D}$$\scriptstyle{e}$$\scriptstyle{u}$$\scriptstyle{v}$$\scriptstyle{d}$$\scriptstyle{m}$

every $e\in\mathcal{E}$ is _orthogonal_ to every $m\in\mathcal{M}$, i.e. given
$u,v$ making the diagram on the right commute, there exists a unique morphism
$d$, making the two triangles commute.

If, furthermore, $\mathcal{E}$ is a class of epimorphisms and $\mathcal{M}$ is
a class of monomorphisms, we say that $(\mathcal{E},\mathcal{M})$ is a _proper
factorisation system_.

We make use of the following well-known fact that any comonad $\mathbb{C}$
which _restricts to embeddings_ , i.e. sends $\mathcal{M}$-morphisms to
$\mathcal{M}$-morphisms, lifts $(\mathcal{E},\mathcal{M})$ to the
factorisation system $(\overline{\mathcal{E}},\overline{\mathcal{M}})$ on
$\mathsf{EM}(\mathbb{C})$, where $\overline{\mathcal{E}}$ consists of all
morphisms of coalgebras $h$ such that $U(h)$ is in $\mathcal{E}$ and,
similarly, $\overline{\mathcal{M}}$ consists of morphisms $h$ such that $U(h)$
is in $\mathcal{M}$.

######  Lemma 2.3.

$(\overline{\mathcal{E}},\overline{\mathcal{M}})$ is a factorisation system
and it is proper whenever $(\mathcal{E},\mathcal{M})$ is.

In the following we always assume that categories of relational structures
$\mathcal{R}(\sigma)$ come equipped with the (surjective, strong injective)
factorisation system111Categorically, surjective homomorphisms are epis and
strong injective homomorphisms are regular monos in $\mathcal{R}(\sigma)$.. It
is immediate to see that $\mathbb{E}_{k}$ preserves strong injective
homomorphisms and, hence, by the previous lemma, this factorisation system
lifts to the categories of $\mathbb{E}_{k}$-coalgebras. Moreover, the same is
true for pebbling and modal comonads and their categories of coalgebras.

###  2.4 Game comonads and logical equivalences

An important feature of game comonads is that they semantically characterise
logical equivalences with respect to various fragments and extensions of
first-order logic. Let $\text{FO}_{k}$ be the fragment of first-order logic
over signature $\sigma$ restricted to sentences of quantifier rank $k$, i.e.
when the depth of nesting of quantifiers is at most $k$. Then,
$\exists^{+}_{k}$ is the further refinement of $\text{FO}_{k}$ to positive
existential sentences, i.e. sentences without negation or universal
quantification, and $\\#\text{FO}_{k}$ is the extension of $\text{FO}_{k}$ by
allowing counting quantifiers. These are quantifiers $\exists_{\geq n}$ where
$A\models\exists_{\geq n}x.\varphi(x)$ if there are at least $n$ different
$a\in A$ such that $A\models\varphi(a)$.

As we will see, the Ehrenfeucht–Fraïssé comonad $\mathbb{E}_{k}$ characterises
logical equivalence with respect to all three aforementioned fragments. To
this end, define

  * •

$A\leftrightarrows_{\mathbb{C}}B$ if there exist morphisms $\mathbb{C}(A)\to
B$ and $\mathbb{C}(B)\to A$, and

  * •

$A\cong_{\mathsf{Kl}(\mathbb{C})}B$ if $F_{\mathbb{C}}(A)\cong
F_{\mathbb{C}}(B)$ in $\mathsf{Kl}(\mathbb{C})$.

In fact, these equivalences are all statements about free coalgebras as
$A\cong_{\mathsf{Kl}(\mathbb{C})}B$ is equivalent to $F^{\mathbb{C}}(A)\cong
F^{\mathbb{C}}(B)$ in $\mathsf{EM}(\mathbb{C})$, since $K^{\mathbb{C}}$ is
fully faithful, and similarly, $A\leftrightarrows_{\mathbb{C}}B$ iff some
$F^{\mathbb{C}}(A)\to F^{\mathbb{C}}(B)$ and $F^{\mathbb{C}}(A)\to
F^{\mathbb{C}}(B)$ exist.

Following [1], to capture logics with equality we introduce an extended
signature $\sigma^{I}$ with a fresh binary relation $I$, and a  _translation
functor_
$\mathfrak{t}^{I}\colon\mathcal{R}_{0}(\sigma)\to\mathcal{R}(\sigma^{I})$
sending $A\in\mathcal{R}_{0}(\sigma)$ to $(A,I^{A})$, where $(a,b)\in I^{A}$
iff $a=b$. Here, $\mathcal{R}_{0}(\sigma)$ denotes the discrete subcategory of
$\mathcal{R}(\sigma)$ containing only identity morphisms. Since
$\mathbb{E}_{k}$ was defined for an arbitrary relational signature, there is
an instance of $\mathbb{E}_{k}$ over $\mathcal{R}(\sigma^{I})$, which we don’t
distinguished notationally.

######  Proposition 2.4 (by adapting [1, theorems 13 and 16]).

For $\sigma$-relational structures $A,B$,

  * •

$A\equiv_{\exists^{+}_{k}}B$ iff $A\leftrightarrows_{\mathbb{E}_{k}}B$ iff
$\mathfrak{t}^{I}A\leftrightarrows_{\mathbb{E}_{k}}\mathfrak{t}^{I}B$

  * •

$A\equiv_{\\#\text{FO}_{k}}B$ iff
$\mathfrak{t}^{I}A\cong_{\mathsf{Kl}(\mathbb{E}_{k})}\mathfrak{t}^{I}B$

Capturing $\equiv_{\text{FO}_{k}}$ requires a few more definitions. First, the
category of _paths_ $\mathcal{P}$ is the full subcategory of
$\mathsf{EM}(\mathbb{E}_{k})$ consisting of the coalgebras $(A,\alpha)$ such
that the order $\sqsubseteq_{\alpha}$ (cf. remark 2.2) is a finite linear
order. Recall from section 2.3 that the factorisation system (surjective,
strong injective) on $\mathcal{R}(\sigma)$ lifts to the category of
$\mathbb{E}_{k}$-coalgebras. We call a morphism
$h\colon(A,\alpha)\to(B,\beta)$ in $\mathsf{EM}(\mathbb{E}_{k})$ a _pathwise-
embedding_ , if for any path embedding

${(P,\pi)}$${(Q,\rho)}$${(A,\alpha)}$${(B,\beta)}$$\scriptstyle{h}$

$e\colon(P,\pi)\rightarrowtail(A,\alpha)$ (with $(P,\pi)\in\mathcal{P}$), the
composite $h\circ e$ is also an embedding. Further, we say that $h$ is _open_
if every commutative square as shown on the right, where $(P,\pi)$ and
$(Q,\rho)$ are from $\mathcal{P}$, has a diagonal filler
$d\colon(Q,\rho)\to(A,\alpha)$ making the two triangles commute. Finally,
define

  * •

$A\leftrightarrow_{\mathbb{C}}B$ if there exists a span of open pathwise-
embeddings $F^{\mathbb{C}}(A)\leftarrow R\rightarrow F^{\mathbb{C}}(B)$.

######  Proposition 2.5 (by adapting [4, theorem 10.5]).

$A\equiv_{\text{FO}_{k}}B$ iff
$\mathfrak{t}^{I}A\leftrightarrow_{\mathbb{E}_{k}}\mathfrak{t}^{I}B$.

The pebbling comonad $\mathbb{P}_{k}$ captures the corresponding $k$-variable
fragments (as opposed to quantifier rank fragment) in the same way and,
similarly, $\mathbb{M}_{k}$ captures the fragments of modal logic restricted
to formulas of modal depth ${\leq}\,k$.

######  Remark 2.6.

We always assume that the subcategory of paths is given implicitly. In
particular, for any category $\mathcal{C}$ equipped with a factorisation
system $(\mathcal{E},\mathcal{M})$, we take the full subcategory of paths
$\mathcal{P}\subseteq\mathcal{C}$ to be the objects whose class of non-
isomorphic subobjects (w.r.t $\mathcal{M}$-morphisms) forms a finite chain
under the order induced by $\mathcal{M}$-morphisms. In particular, for the
game comonads we discuss, the subcategory of
$\mathcal{P}\subseteq\mathsf{EM}(\mathbb{C})$ is equivalent to subcategory of
the coalgebras $(A,\alpha)$ where the order $\sqsubseteq_{\alpha}$ is a finite
linear order [3].

##  3 Comonadic FVM Theorems

###  3.1 A Motivating FVM-type Example

In the approach to algorithmic meta-theorems such as Courcelle’s theorem
adopted in later sections, we work with classes of structures built up by a
suitable family of operations. These operations must interact well with
logical equivalence in the sense of Feferman–Vaught–Mostowski. We now outline
a simple motivating example, forming coproducts of structures, and the
relationship to first order logic. We use the Ehrenfeucht–Fraïssé comonad,
highlighting the key themes, and emphasizing connections to game comonads. The
finer technical details are developed in later sections.

Fix a relational signature $\sigma$ without constants. For two structures $A$
and $B$, their coproduct $A+B$ is simply the disjoint union of the two
components, with the induced relational structure. We would like to show that,
if $A_{1}\equiv_{\text{FO}_{k}}B_{1}$ and $A_{2}\equiv_{\text{FO}_{k}}B_{2}$,
then also $A_{1}+A_{2}\equiv_{\text{FO}_{k}}B_{1}+B_{2}$. Equivalently, in
view of proposition 2.5, given spans of open pathwise-embeddings
$F^{\mathbb{E}_{k}}(\mathfrak{t}^{I}(A_{i}))\xleftarrow{f_{i}}R_{i}\xrightarrow{g_{i}}F^{\mathbb{E}_{k}}(\mathfrak{t}^{I}(B_{i}))$
for $i\in\\{1,2\\}$, we would like to construct a span of open pathwise
embeddings of the form

$\displaystyle F^{\mathbb{E}_{k}}(\mathfrak{t}^{I}(A_{1}+A_{2}))\leftarrow
R\rightarrow F^{\mathbb{E}_{k}}(\mathfrak{t}^{I}(B_{1}+B_{2})).$ (3)

Observe that, even though the category of coalgebras has coproducts for
general reasons, a span of the form in (3) cannot be formed using the
coproduct of the two component spans. We would obtain a span of type

$F^{\mathbb{E}_{k}}(\mathfrak{t}^{I}(A_{1}))+F^{\mathbb{E}_{k}}(\mathfrak{t}^{I}(A_{2}))\xleftarrow{f_{1}+f_{2}}R_{1}+R_{2}\xrightarrow{g_{1}+g_{2}}F^{\mathbb{E}_{k}}(\mathfrak{t}^{I}(B_{1}))+F^{\mathbb{E}_{k}}(\mathfrak{t}^{I}(B_{2}))$

In general
$F^{\mathbb{E}_{k}}(\mathfrak{t}^{I}(A_{1}))+F^{\mathbb{E}_{k}}(\mathfrak{t}^{I}(A_{2}))$
and $F^{\mathbb{E}_{k}}(\mathfrak{t}^{I}(A_{1}+A_{2}))$ need not be
isomorphic, so our span is of the wrong type. Conceptually, this approach
fails because the span we require should encode a strategy for play that may
switch back and forth between two components, and forming coproducts keeps all
the data entirely independent.

We observe that if we have a natural transformation
$\kappa\colon\mathbb{E}_{k}(A+B)\to\mathbb{E}_{k}(A)+\mathbb{E}_{k}(B)$ that
satisfies some natural equations with respect to the counit and
comultiplication, then this induces a lifted functor
$\mathbin{\overline{+}}:\mathsf{Kl}(\mathbb{E}_{k})\times\mathsf{Kl}(\mathbb{E}_{k})\rightarrow\mathsf{Kl}(\mathbb{E}_{k})$
such that
$F_{\mathbb{E}_{k}}(A+B)=F_{\mathbb{E}_{k}}(A)\mathbin{\overline{+}}F_{\mathbb{E}_{k}}(B)$.
As $F_{\mathbb{E}_{k}}(A)=A$, the existence of such a natural transformation
yields both:

$\displaystyle A_{1}\equiv_{\exists^{+}_{k}}A_{2}\;\mbox{ and
}\;B_{1}\equiv_{\exists^{+}_{k}}B_{2}\;$
$\displaystyle\Rightarrow\;A_{1}+B_{1}\equiv_{\exists^{+}_{k}}A_{2}+B_{2}$
$\displaystyle A_{1}\equiv_{\\#\text{FO}_{k}}A_{2}\;\mbox{ and
}\;B_{1}\equiv_{\\#\text{FO}_{k}}B_{2}\;$
$\displaystyle\Rightarrow\;A_{1}+B_{1}\equiv_{\\#\text{FO}_{k}}A_{2}+B_{2}$

So we have FVM type results for the positive existential fragment, and FO with
counting quantifiers. For full first-order logic, we require an additional
observation. As $\mathsf{EM}(\mathbb{E}_{k})$ has equalizers, we can lift
coproducts to a functor
$\mathsf{EM}(\mathbb{E}_{k})\times\mathsf{EM}(\mathbb{E}_{k})\rightarrow\mathsf{EM}(\mathbb{E}_{k})$
by forming the equalizer:

${A\mathbin{\widehat{+}}B}$${F^{\mathbb{E}_{k}}(A+B)}$${F^{\mathbb{E}_{k}}(\mathbb{E}_{k}(A)+\mathbb{E}_{k}(B))}$$\scriptstyle{F^{\mathbb{E}_{k}}(\kappa)\circ\delta}$$\scriptstyle{F^{\mathbb{E}_{k}}(\alpha+\beta)}$

Crucially, this functor satisfies $F^{\mathbb{E}_{k}}(A+B)\cong
F^{\mathbb{E}_{k}}(A)\mathbin{\widehat{+}}F^{\mathbb{E}_{k}}(B)$. We can then
verify the following by direct calculation.

######  Lemma 3.1.

Given a pair of open pathwise-embeddings $f,g$ in
$\mathsf{EM}(\mathbb{E}_{k})$, the morphism $f\mathbin{\widehat{+}}g$ is also
an open pathwise-embedding.

We see that the following span

$F^{\mathbb{E}_{k}}(\mathfrak{t}^{I}(A_{1}))\mathbin{\widehat{+}}F^{\mathbb{E}_{k}}(\mathfrak{t}^{I}(A_{2}))\xleftarrow{f_{1}\mathbin{\widehat{+}}f_{2}}R_{1}\mathbin{\widehat{+}}R_{2}\xrightarrow{g_{1}\mathbin{\widehat{+}}g_{2}}F^{\mathbb{E}_{k}}(\mathfrak{t}^{I}(B_{1}))\mathbin{\widehat{+}}F^{\mathbb{E}_{k}}(\mathfrak{t}^{I}(B_{2}))$

is a span of open pathwise-embeddings, by lemma 3.1. Moreover,
$F^{\mathbb{E}_{k}}(\mathfrak{t}^{I}(A_{1}))\mathbin{\widehat{+}}F^{\mathbb{E}_{k}}(\mathfrak{t}^{I}(A_{2}))$
is isomorphic to
$F^{\mathbb{E}_{k}}(\mathfrak{t}^{I}(A_{1})+\mathfrak{t}^{I}(A_{2}))$ and
similarly for $B_{1}$ and $B_{2}$, and
$\mathfrak{t}^{I}(A)+\mathfrak{t}^{I}(B)\cong\mathfrak{t}^{I}(A+B)$, yielding
a span of shape (3), and so $A_{1}+A_{2}\equiv_{\text{FO}_{k}}B_{1}+B_{2}$.

######  Remark 3.2.

The above analysis follows from a well-known theory of commutative (resp. lax
monoidal) monads [26]. They lift the monoidal structure to the Kleisli and
Eilenberg-Moore categories (if sufficiently complete [15, 27]). The liftings
of coproducts in this section is arising from the dual of these results, as
$\mathbb{E}_{k}$ is opmonoidal with respect to coproducts.

Motivated by this example, in the sequel we introduce a general framework for
lifting logical equivalences. The general results deal with operations of
arbitrary finite arity, with unary and binary transformations being of primary
interest in applications. We will also need to deal with varying base
categories and comonads, as signatures, resource parameters or even logics may
vary under model transformations. As was the case in this example, this leads
to FVM theorems for a given logic, its positive existential fragment, and its
extension with counting quantifiers, parametric in the game comonad of
interest. The main technical challenge is giving sufficient conditions for the
analogue of the critical lemma 3.1 to hold.

###  3.2 FVM-Theorems from Kleisli-laws

As we saw in section 3.1, in order to develop FVM-type theorems within the
comonadic framework, it is natural to consider functorial transformations of
models. We consider categories $\mathcal{C}_{1}$, …, $\mathcal{C}_{n}$ and
$\mathcal{D}$, equipped with comonads $\mathbb{C}_{1},\dots,\mathbb{C}_{n}$,
and $\mathbb{D}$, respectively, and a functorial operation
$H\colon\prod_{i}\mathcal{C}_{i}\to\mathcal{D}$.

######  Remark 3.3.

To simplify our notation for objects and morphisms in product categories, we
shall write $\vv{A_{i}}$ and $\vv{f_{i}}$ instead of the longer expressions
$A_{1},\dots,A_{n}$ and $f_{1},\dots,f_{n}$, respectively.

A _Kleisli-law_ is a natural transformation $\kappa\colon\mathbb{D}\circ H\to
H\circ\prod_{i}\mathbb{C}_{i}$ such that:

  1. (F1)

$H(\vv{\varepsilon_{i}})\circ\kappa=\varepsilon_{H}$

  2. (F2)

$H(\vv{\delta_{i}})\circ\kappa=\kappa\circ\mathbb{D}\kappa\circ\delta_{H}$

These laws are direct generalisations of Kleisli-laws lifting of unary functor
to the Kleisli category, see e.g. [34]. The following result is probably
folklore [24]:

######  Proposition 3.4.

There is a bijective correspondence between:

  1. 1.

Kleisli-laws of type $\mathbb{D}\circ H\to H\circ\prod_{i}\mathbb{C}_{i}$.

  2. 2.

Functors
$\overline{H}:\prod_{i}\mathsf{Kl}(\mathbb{C}_{i})\rightarrow\mathsf{Kl}(\mathbb{D})$
such that: $\overline{H}\circ\prod_{i}F_{\mathbb{C}_{i}}=F_{\mathbb{D}}\circ
H$.

It is encouraging for the game comonad approach that this classical theory
immediately yields results for logical equivalences. To this end, let
$\approx_{\mathbb{C}_{i}}$ and $\approx_{\mathbb{D}}$ be binary relations on
$\mathcal{C}_{i}$ and $\mathcal{D}$ objects respective. We shall say that _$H$
preserves $\approx$_ if for all $1\leq i\leq n$,
$A_{i}\mathbin{\approx_{\mathbb{C}_{i}}}B_{i}$, then
$H(A_{1},\ldots,A_{n})\mathbin{\approx_{\mathbb{D}}}H(B_{1},\ldots,B_{n})$.

######  Theorem 3.5.

If $\kappa:\mathbb{D}\circ H\rightarrow H\circ\prod_{i}\mathbb{C}_{i}$t is a
Kleisli-law then $H$ preserves both $\leftrightarrows$ and
$\cong_{\mathsf{Kl}}$.

######  Example 3.6 (Comonad Morphisms).

A _comonad morphism_ $\sigma:\mathbb{C}\Rightarrow\mathbb{D}$ is a natural
transformation such that $\varepsilon\circ\sigma=\varepsilon$ and
$\delta\circ\sigma=\mathbb{D}(\sigma)\circ\sigma\circ\delta$. A comonad
morphism is a special case of a Kleisli-law, of type
$\mathbb{C}\circ{Id}\Rightarrow{Id}\circ\mathbb{D}$, corresponding to liftings
of the identity functor. For example, there is a comonad morphism of type
$\mathbb{M}\rightarrow\mathbb{P}_{2}$, with action preserving constants, and
mapping lists to lists pebbled by the parity of their position:

$[a_{1},a_{2},a_{3}\ldots,a_{n}]\mapsto[(1,a_{1}),(0,a_{2}),(1,a_{3})\ldots,(p_{n},a_{n})]$

where $p_{n}=n\mod 2$. Consequently, utilizing the logical characterizations
analogous to proposition 2.4 in the cases of (full, unbounded depth)
$\mathbb{M}$ and $\mathbb{P}_{2}$ [1, 4], we obtain a semantic translation of
positive $\square$-free modal logic into positive existential two variable
logic and graded modal logic into two variable logic with counting
quantifiers.

###  3.3 Lifting operations to categories of coalgebras

Assuming appropriate equalisers in $\mathsf{EM}(\mathbb{D})$ exist, we can
extend the above lifting to the categories of coalgebras
$\widehat{H}\colon\prod_{i}\mathsf{EM}(\mathbb{C}_{i})\rightarrow\mathsf{EM}(\mathbb{D})$.
We define $\widehat{H}$ pointwise as the equaliser, for coalgebras
$(A_{1},\alpha_{1})\in\mathsf{EM}(\mathbb{C}_{1})$, …,
$(A_{n},\alpha_{n})\in\mathsf{EM}(\mathbb{C}_{n})$,

${\widehat{H}(\vv{\alpha_{i}})}$${F^{\mathbb{D}}(H(\vv{A_{i}}))}$${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}}))}$
(4)

In fact, the two parallel morphisms are a _reflexive pair_. That is, they have
a mutual post-inverse.

######  Proposition 3.7.

If $\kappa$ is a Kleisli-law, and $\mathsf{EM}(\mathbb{D})$ has equalizers of
reflexive pairs, then $\widehat{H}$ is a well-defined functor such that
$F_{\mathbb{D}}\circ H\cong\widehat{H}\circ\prod_{i}F^{\mathbb{C}_{i}}$.

Note that existence of said equalisers is guaranteed for our game comonads.

######  Lemma 3.8.

For a comonad $\mathbb{C}$ over $\mathcal{R}(\sigma)$. If $\mathbb{C}$
preserves embeddings then the category $\mathsf{EM}(\mathbb{C})$ has
equalisers.

The same is true for a comonad $\mathbb{C}$ over any wide222Recall that a
subcategory is _wide_ if it contains the same objects, with only morphisms
restricted. subcategory $\mathcal{C}$ of $\mathcal{R}(\sigma)$ with
coproducts, all embeddings of $\mathcal{R}(\sigma)$ and satisfying that if
$f\circ g\in\mathcal{C}$, for some $f,g\in\mathcal{R}(\sigma)$, then also
$g\in\mathcal{C}$.

###  3.4 Smooth Kleisli laws

In this section we observe that for an operation to preserve $\leftrightarrow$
we require the lifted operation to preserve open pathwise-embeddings. Since
open pathwise-embeddings are defined in terms of embeddings and paths, we
require that the categories $\mathcal{C}_{1},\dots,\mathcal{C}_{n+1}$333It is
notationally convenient to denote the codomain category and comonad
$\mathcal{C}_{n+1}$ and $\mathbb{C}_{n+1}$, rather than $\mathcal{D}$ and
$\mathbb{D}$ is this section. As before, we assume that
$\mathsf{EM}(\mathbb{C}_{n+1})$ has equalisers of reflexive pairs. are
equipped with proper factorisation systems and the comonads preserve
embeddings (cf. lemma 2.3). We then say an operation
$H\colon\prod\mathcal{C}_{i}\to\mathcal{C}_{n+1}$ with a Kleisli law $\kappa$
is _smooth_ 444Mirroring the terminology introduced in [32]. if
$\widehat{H}(f_{1},\dots,f_{n})$ is an open pathwise-embedding for every tuple
of open pathwise-embeddings $f_{1},\dots,f_{n}$. Smoothness immediately
guarantees FVM-type theorem for back-and-forth equivalence.

######  Proposition 3.9.

If $H$ admits a smooth Kleisli law, then $H$ preserves $\leftrightarrow$.

Recall that $\equiv_{\text{FO}_{k}}$ is obtained as the
$\leftrightarrow_{\mathbb{E}_{k}}$ relation preceded by the $\mathfrak{t}^{I}$
translation. The following is one of our main definitions in this paper,
tailored to account for this translation.

######  Definition 3.10.

We say that an ‘operation’ functor
$H\colon\prod_{i=1}^{n}\mathcal{R}_{0}(\sigma_{i})\to\mathcal{R}_{0}(\sigma_{n+1})$
is _$(\mathbb{C}_{1},\dots,\mathbb{C}_{n+1})$ -smooth relative to
$\mathfrak{t}_{1},\dots,\mathfrak{t}_{n+1}$_, where
$\mathfrak{t}_{i}\colon\mathcal{R}_{0}(\sigma_{i})\to\mathcal{C}_{i}$ is a
functor and $\mathbb{C}_{i}$ a comonad on $\mathcal{C}_{i}$, for $1\leq i\leq
n+1$, if there exists a functor
$H^{\mathfrak{t}}\colon\prod_{i=1}^{n}\mathcal{C}_{i}\to\mathcal{C}_{n+1}$ and
natural transformations

$\theta\colon
H^{\mathfrak{t}}\circ\prod\nolimits_{i=1}^{n}\mathfrak{t}_{i}\to\mathfrak{t}_{n+1}\circ
H\quad\text{and}\quad\kappa\colon\mathbb{C}_{n+1}\circ H^{\mathfrak{t}}\to
H^{\mathfrak{t}}\circ\prod\nolimits_{i=1}^{n}\mathbb{C}_{i}$

such that $\kappa$ is a smooth Kleisli law and $F^{\mathbb{C}_{n+1}}(\theta)$
is a collection of open pathwise embeddings.

Lastly, we say that $H$ is _FO-
$(\mathbb{C}_{1},\dots,\mathbb{C}_{n+1})$-smooth_ if it is
$(\mathbb{C}_{1},\dots,\mathbb{C}_{n+1})$-smooth relative to
$\mathfrak{t}_{1},\dots,\mathfrak{t}_{n+1}$ where each
$\mathfrak{t}_{i}\colon\mathcal{R}_{0}(\sigma_{i})\to\mathcal{C}_{i}$ is a
codomain restriction of the usual FO translation functor
$\mathfrak{t}^{I}\colon\mathcal{R}_{0}(\sigma_{i})\to\mathcal{R}^{S}(\sigma^{I}_{i})$.

By convention, call an $n$-ary operation $\mathbb{C}$-smooth if it is
$(\mathbb{C},\dots,\mathbb{C})$-smooth, for the same game comonad $\mathbb{C}$
but possibly $n$ different instances for $n$ different signatures.

######  Corollary 3.11.

FO-$\mathbb{E}_{k}$-smooth operations preserve $\equiv_{\text{FO}_{k}}$.

Similar statements also hold for $\mathbb{P}_{k}$, $\mathbb{M}_{k}$ and their
corresponding logical equivalences.

######  Example 3.12.

In the case of first-order equivalence, and the coproduct operation,
definition 3.10 is instantiated with every comonad $\mathbb{C}_{i}$ as
$\mathbb{E}_{k}$, and $\mathfrak{t}_{i}=\mathfrak{t}^{I}$. The natural
transformation $\kappa$ is as mentioned in section 3.1 and $\theta$ is the
isomorphism
$\mathfrak{t}^{I}(A)+\mathfrak{t}^{I}(B)\cong\mathfrak{t}^{I}(A+B)$.
Therefore, coproducts are FO-$\mathbb{E}_{k}$-smooth and preserves
$\equiv_{\text{FO}_{k}}$.

###  3.5 Practical axioms for smoothness

The notion of smoothness in definition 3.10 is extremely general, but the
required conditions can be cumbersome to verify. We now identify sufficient
conditions for a Kleisli-law to be smooth, that are easier to establish in
practice. We introduce the following axioms:

  1. (S1)

$H\colon\prod_{i}\mathcal{C}_{i}\to\mathcal{D}$ restricts to embeddings.

  2. (S2)

Any path embedding $e\colon\pi\rightarrowtail\widehat{H}(\vv{\alpha_{i}})$ has
a _minimal decomposition_ as $e_{0}\colon\pi\to\widehat{H}(\vv{\pi_{i}})$
followed by
$\widehat{H}(\vv{e_{i}})\colon\widehat{H}(\vv{\pi_{i}})\to\widehat{H}(\vv{\alpha_{i}})$,
for some path embeddings $e_{i}\colon\pi_{i}\rightarrowtail\alpha_{i}$, for
$1\leq i\leq n$.

Minimality in (S2) expresses that for any other decomposition of $e$ as
$g_{0}\colon\pi\to\widehat{H}(\vv{\rho_{i}})$ followed by
$\widehat{H}(\vv{g_{i}})\colon\widehat{H}(\vv{\rho_{i}})\to\widehat{H}(\vv{\alpha_{i}})$,
for some path embeddings $g_{i}\colon\rho_{i}\rightarrowtail\alpha_{i}$, there
exist (necessarily unique) morphisms $h_{i}\colon\pi_{i}\to\rho_{i}$ such that
$e_{i}=g_{i}\circ h_{i}$, for $i=1,\dots,n$.

A necessary step before showing sufficiency of (S1) and (S2), is checking the
following.

######  Proposition 3.13.

If $f_{1},\dots,f_{n}$ are embeddings (or pathwise-embeddings) in
$\mathsf{EM}(\mathbb{C}_{1})$, …, $\mathsf{EM}(\mathbb{C}_{n})$, respectively,
then $\widehat{H}(f_{1},\dots,f_{n})$ is an embedding (or pathwise-embedding).

The main difficulty is in verifying that openness for pathwise-embeddings is
also preserved, which is the case.

######  Theorem 3.14.

A Kleisli law which satisfies (S1) and (S2) is smooth.

###  3.6 Example: edge creation

We apply our comonadic analysis to the investigation of bounded clique-width
structures in section 5.2. An operation important in the construction of
bounded clique-width structures is edge-creation
${\operatorname{join}_{\bar{i}}^{R}}$, for some $r$-ary $R\in\sigma$, where
$\sigma$ is without constants. The operation
${\operatorname{join}_{\bar{i}}^{R}}$, as all the operations for forming a
$\sigma$-structure of clique-width $\leq m$, apply to structures in an
expanded signature555In fact, this is slightly more general. Clique-width is
typically defined for graphs rather than relational structures.
$\sigma_{m}=\sigma\cup\\{P_{1},\dots,P_{m}\\}$ where $P_{i}$ are unary
relations, or ‘colours’. The operation ${\operatorname{join}_{\bar{i}}^{R}}$
takes a list of colours $i=(i_{1},\dots,i_{r})$ with $i_{j}\in\\{1,\dots,m\\}$
and adds all tuples in $P_{i_{1}}\times\dots\times P_{i_{r}}$ to the
interpretation of $R$.

It is clear that
${\operatorname{join}_{\bar{i}}^{R}}\colon\mathcal{R}(\sigma_{m})\to\mathcal{R}(\sigma_{m})$
is a functor. Furthermore, we have a natural transformation
$\kappa\colon\mathbb{E}_{k}\circ{\operatorname{join}_{\bar{i}}^{R}}\to{\operatorname{join}_{\bar{i}}^{R}}\circ\mathbb{E}_{k}$
with components $\kappa_{A}$ that send
$w\in\mathbb{E}_{k}({\operatorname{join}_{\bar{i}}^{R}}(A))$ to the same word
$w$ in ${\operatorname{join}_{\bar{i}}^{R}}(\mathbb{E}_{k}A)$ which satisfies
(F1), (F2), (S1) and (S2).

######  Lemma 3.15.

$\kappa\colon\mathbb{E}_{k}\circ{\operatorname{join}_{\bar{i}}^{R}}\to{\operatorname{join}_{\bar{i}}^{R}}\circ\mathbb{E}_{k}$
is a smooth Kleisli law.

For any signature $\sigma$, ${\operatorname{join}_{\bar{i}}^{R}}$ does not
change the interpretation of any relation in $\sigma\backslash\\{R\\}$, so we
obtain a natural isomorphism
$\theta:{\operatorname{join}_{\bar{i}}^{R}}(\mathfrak{t}^{I})\cong\mathfrak{t}^{I}({\operatorname{join}_{\bar{i}}^{R}})$
with components given by the identity as a set function. Therefore,
${\operatorname{join}_{\bar{i}}^{R}}$ is FO-$\mathbb{E}_{k}$-smooth.

###  3.7 Example: parallel sums

Maybe the most prominent example of a FVM theorem is the one for coproducts.
Here we verify smoothness for a generalisation of coproducts. Let $\sigma$ be
a relational signature without constants and let $\sigma_{1}$, $\sigma_{2}$
and $\sigma_{3}$ be extensions of $\sigma$ with constants such that
$\mathbf{cs}(\sigma_{1})\cup\mathbf{cs}(\sigma_{2})=\mathbf{cs}(\sigma_{3})$.
This operation is slightly more subtle than the previous examples. In order
for our Kleisli law to be natural, we need to restrict the homomorphisms in
our categories of interest. Therefore, we work with the restriction
$\mathcal{R}_{\text{nc}}(\sigma)$ of $\mathcal{R}(\sigma)$ to the morphisms
which send non-constant elements to non-constant elements. Define a binary
operation

$\mathbin{\parallel}\colon\mathcal{R}_{0}(\sigma_{1})\times\mathcal{R}_{0}(\sigma_{2})\to\mathcal{R}_{0}(\sigma_{3})$

sending $A\in\mathcal{R}_{0}(\sigma_{1})$ and
$B\in\mathcal{R}_{0}(\sigma_{2})$ to the quotient $(A+B)/_{\approx}$ where
$A+B$ is the $\sigma$-structure coproduct and $\approx$ the least equivalence
relation identifying pairs $(c^{A},c^{B})$ such that
$c\in\mathbf{cs}(\sigma_{1})\cap\mathbf{cs}(\sigma_{2})$. For a constant
$c\in\mathbf{cs}(\sigma_{1})$ we set
$c^{A\mathbin{\parallel}B}=\mathfrak{i}(c^{A})$ and, similarly, for
$c\in\mathbf{cs}(\sigma_{2})$ set
$c^{A\mathbin{\parallel}B}=\mathfrak{i}(c^{B})$, where $\mathfrak{i}$ is the
quotient map $A+B\to A\mathbin{\parallel}B$. Observe that
$\mathfrak{i}(A)\cap\mathfrak{i}(B)=\\{c^{A\mathbin{\parallel}B}\mid
c\in\mathbf{cs}(\sigma_{1})\cap\mathbf{cs}(\sigma_{2})\\}$.

The operation $\mathbin{\parallel}$ extends to a functor
$\mathcal{R}_{\text{nc}}(\sigma_{1})\times\mathcal{R}_{\text{nc}}(\sigma_{2})\to\mathcal{R}_{\text{nc}}(\sigma_{3})$.
Furthermore, it admits a smooth Kleisli law w.r.t. a comonad
$\mathbb{E}_{k}^{\text{nc}}$ on $\mathcal{R}_{\text{nc}}(\sigma_{i})$ (for
$i=1,2,$ or $3$), which is the restriction of $\mathbb{E}_{k}$ to words that
do not contain any constant letter. Then, the Kleisli law is the following
mapping, for every $A\in\mathcal{R}(\sigma_{1})$ and
$B\in\mathcal{R}(\sigma_{2})$, defined on non-constants by

$\displaystyle\kappa\colon\mathbb{E}_{k}^{\text{nc}}(A\mathbin{\parallel}B)\longrightarrow\mathbb{E}_{k}^{\text{nc}}(A)\mathbin{\parallel}\mathbb{E}_{k}^{\text{nc}}(B),$
$\displaystyle w\in{(A\mathbin{\parallel}B)}^{\leq k}$
$\displaystyle\mapsto\begin{cases}\mathtt{ex}_{1}(w)&\text{if
}\varepsilon(w)\in\mathfrak{i}(A)\\\ \mathtt{ex}_{2}(w)&\text{if
}\varepsilon(w)\in\mathfrak{i}(B)\\\\[5.0pt] \end{cases}$

where $\mathtt{ex}_{1}([x_{1},\dots,x_{n}])$ is the word666We use the Haskell-
style list comprehension notation, for a word $w=[x_{1},\dots,x_{n}]$ the word
$[x_{i}\mid\varphi(i)]$ is the restriction of $w$ to the letters on positions
$i$ such that $\varphi(i)$ holds. $[x_{i}\mid x_{i}\in\mathfrak{i}(A)]$ and,
similarly, $\mathtt{ex}_{2}([x_{1},\dots,x_{n}])$ is $[x_{i}\mid
x_{i}\in\mathfrak{i}(B)]$. One can verify that $\kappa$ satisfies axioms (S1)
and (S2), which gives us:

######  Lemma 3.16.

$\kappa$ is a smooth Kleisli law
$(\mathbb{E}_{k}^{\text{nc}}\circ\mathbin{\parallel})\rightarrow(\mathbin{\parallel}\circ(\mathbb{E}_{k}^{\text{nc}}\times\mathbb{E}_{k}^{\text{nc}}))$.

In fact, $\mathbin{\parallel}$ is FO-$\mathbb{E}_{k}^{\text{nc}}$-smooth as
$\mathfrak{t}^{I}(A)\mathbin{\parallel}^{I}\mathfrak{t}^{I}(B)\cong\mathfrak{t}^{I}(A\mathbin{\parallel}B)$,
where $\mathbin{\parallel}^{I}$ is the $\sigma^{I}$ variant of
$\mathbin{\parallel}$. Further, it also follows that
$\mathfrak{t}^{I}(A)\leftrightarrow_{\mathbb{E}_{k}^{\text{nc}}}\mathfrak{t}^{I}(B)$
iff $A\equiv_{\text{FO}_{k}}B$, giving us the following.

######  Proposition 3.17.

If $A_{i}\equiv_{\text{FO}_{k}}B_{i}$ in
$\mathcal{R}_{\text{nc}}(\sigma_{i})$, for $i=1,2$, then
$A_{1}\mathbin{\parallel}A_{2}\,\equiv_{\text{FO}_{k}}\,B_{1}\mathbin{\parallel}B_{2}$.

###  3.8 Other examples

######  Example 3.18 (Products for FO).

For any comonad, there is a canonical Kleisli law for products, and when the
Eilenberg-Moore category has equalizers, the lifted functor yields products.
By observing that pairs are equal if and only if each component is equal, we
obtain an isomorphism $\mathfrak{t}^{I}(A\times
B)\cong\mathfrak{t}^{I}(A)\times\mathfrak{t}^{I}(B)$. We can confirm that
products of coalgebras preserve open pathwise embeddings, and therefore
products are FO-$\mathbb{E}_{k}$-smooth.

######  Example 3.19 (Comonad Morphisms).

Example 3.6 exhibited a comonad morphism
$\kappa:\mathbb{M}\rightarrow\mathbb{P}_{2}$ yielding a semantic translation
of positive $\square$-free modal logic into two-variable positive existential
logic and graded modal logic into two-varable logic with counting quantifiers.
The intermediate translation from full modal logic into two-variable logic is
witnessed by $\kappa$ being $(\mathbb{M},\mathbb{P}_{2})$-smooth.

##  4 Comonads for MSO

###  4.1 $\mathbb{E}_{k}$ for many-sorted structures

In order to extend our use of $\mathbb{E}_{k}$ to MSO we interpret the syntax
of MSO as a two-sorted first-order logic. We then use a translation functor to
fix the semantics of MSO to coincide with the standard semantics. This
requires us to ‘upgrade’ the $\mathbb{E}_{k}$ comonad to handle two-sorted
structures. For simplicity and generality, we extend our definition of
$\mathbb{E}_{k}$ to accommodate all many-sorted structures for fixed set $S$
of sorts.

A signature $\sigma$ on sorts $S$ contains a set of constant symbols
$\mathbf{cs}(\sigma,s)$ for each $s\in S$ and a set of relation symbols $R$
with an associated arity given by a tuple of sorts ${\langle
s_{1},\dots,s_{r}\rangle\in S^{r}}$. An object $A$ in the category of
$\sigma$-structures $\mathcal{R}^{S}(\sigma)$ has a universe given by an
$S$-indexed family of sets $\\{A_{s}\\}_{s\in S}$ along with interpretations
$c^{A}\in A_{s}$ for every constant symbol $c\in\mathbf{cs}(\sigma,s)$ and
$R^{A}\subseteq A_{s_{1}}\times\dots\times A_{s_{r}}$ for every relation
symbol with arity $\langle s_{1},\dots,s_{r}\rangle$ in $\sigma$. A morphism
$f:A\rightarrow B$ in $\mathcal{R}^{S}(\sigma)$ is a $S$-indexed family of
functions $\\{f_{s}:A_{s}\rightarrow B_{s}\\}$ which preserves all constants
and all relations.

These objects provide the semantics for $S$-sorted first-order logic. Both
syntax and semantics of $S$-sorted first order logic $\text{FO}(S)$ are
similar to the single-sorted case. The key difference is that terms (constants
and variables) always have an associated sort. Consequently, the quantifiers
$\exists x{:}s$, $\forall x{:}s$ range over the set $A_{s}$ when interpreted
in the model $A$. For subset $J\subseteq S$, $\text{FO}_{k}(S,J)$ denotes
$S$-sorted first order logic up to quantifier rank $k$ with equality for terms
with sorts $s\in J$.

We can now describe $\mathbb{E}_{k}$ as a comonad over
$\mathcal{R}^{S}(\sigma)$. The universe of $\mathbb{E}_{k}A$ for object $A$ in
$\mathcal{R}^{S}(\sigma)$ has components $(\mathbb{E}_{k}A)_{s}$ equal to the
disjoint union of $\mathbf{cs}(\sigma,s)$ and the set of words of the form
$[a_{1}{:}s_{1},\dots,a_{n}{:}s_{n}]$ where $n\leq k$ and, for all $i\leq n$,
$s_{i}\in S$, $a_{i}\in A_{s_{i}}$ and $s_{n}=s$. The counit $\varepsilon_{A}$
for $A\in\mathcal{R}^{S}(\sigma)$ and coextension
$f^{*}:\mathbb{E}_{k}A\rightarrow\mathbb{E}_{k}B$ for
$f:\mathbb{E}_{k}A\rightarrow B$ are defined as in the single-sorted case
while respecting the sorts. We can perform a similar upgrade to the single-
sorted $\mathbb{E}_{k}^{\text{nc}}$ comonad to obtain a many-sorted
$\mathbb{E}_{k}^{\text{nc}}$ comonad.

######  Proposition 4.1.

$\mathbb{E}_{k}$ and $\mathbb{E}_{k}^{\text{nc}}$ are comonads over
$\mathcal{R}^{S}(\sigma)$ and $\mathcal{R}^{S}_{\text{nc}}(\sigma)$,
respectively.

Just as with the single-sorted case, to capture equality for the sorts
$J\subseteq S$, we consider an extended signature $\sigma^{J}$ which has
additional relations $I_{s}$ of arity $\langle s,s\rangle$ for every $s\in J$.
Let
$\mathfrak{t}^{J}\colon\mathcal{R}^{S}_{0}(\sigma)\rightarrow\mathcal{R}^{S}(\sigma^{J})$
be the functor that sends $A$ to the same structure where the additional
relations are interpreted as $(a,b)\in I^{A}_{s}$ iff $a=b\in A_{s}$ for $s\in
J$. Let
$\mathfrak{t}^{J}_{\text{nc}}\colon\mathcal{R}^{S}_{0}(\sigma)\rightarrow\mathcal{R}^{S}_{\text{nc}}(\sigma^{J})$
be the codomain restriction of $\mathfrak{t}^{J}$. We then show that a version
of proposition 2.5 still holds for these many-sorted $\mathbb{E}_{k}$ and
$\mathbb{E}_{k}^{\text{nc}}$ comonads.

######  Proposition 4.2.

Given $A,B\in\mathcal{R}^{S}_{0}(\sigma)$,

  * •

$A\equiv_{\text{FO}_{k}(S,J)}B$ iff
$\mathfrak{t}^{J}A\leftrightarrow_{\mathbb{E}_{k}}\mathfrak{t}^{J}B$.

  * •

$A\equiv_{\text{FO}_{k}(S,J)}B$ iff
$\mathfrak{t}^{J}_{\text{nc}}A\leftrightarrow_{\mathbb{E}_{k}^{\text{nc}}}\mathfrak{t}^{J}_{\text{nc}}B$,
if $s\in J$ for every sort $s\in S$ such that
$\mathbf{cs}(\sigma,s)\not=\emptyset$.

###  4.2 The two-sorted translation for MSO

Second-order logic can be treated syntactically as a many-sorted first-order
logic (see e.g. [42, 35]). In particular, we consider $\text{MSO}_{k}$ on
signature $\sigma$ as $\text{FO}_{k}(S,J)$ with
$S=\\{\mathbf{f},\mathbf{m}\\}$ and $J=\\{\mathbf{f}\\}$ on an expanded
signature $\sigma^{e}$ where $\mathbf{f}$ is sort for ordinary first-order
terms, and $\mathbf{m}$ is a sort for monadic second-order set variables. The
expanded $S$-sorted signature $\sigma^{e}$ has constants
$\mathbf{cs}(\sigma^{e},\mathbf{f})=\mathbf{cs}(\sigma)$ and
$\mathbf{cs}(\sigma^{e},\mathbf{m})=\varnothing$; and relations $R$ of arity
$\langle\mathbf{f},\dots,\mathbf{f}\rangle$ ($\mathbf{f}$ repeated $r$ times)
for every $R\in\sigma$ of arity $r$, and also $e$ of arity
$\langle\mathbf{f},\mathbf{m}\rangle$ and $I$ of arity
$\langle\mathbf{f},\mathbf{f}\rangle$.

The additional expressive power of MSO over $\text{FO}(S,J)$ is obtained by
restricting the semantics of MSO to only include the class of ‘standard’
models of MSO rather than all $\sigma^{e}$-structures. We pick out these
standard models using a functor
$\mathfrak{t}^{e}\colon\mathcal{R}_{0}(\sigma)\rightarrow\mathcal{R}^{S}(\sigma^{e})$
where, for a $\sigma$-structure $A$, the two sorts are instantiated as
$\mathfrak{t}^{e}(A)_{\mathbf{f}}=A$ and
$\mathfrak{t}^{e}(A)_{\mathbf{m}}=\mathcal{P}(A)$, the constants
$c^{\mathfrak{t}^{e}A}=c^{A}$ and relations

$R^{\mathfrak{t}^{e}(A)}=R^{A},\text{ for }R\in\sigma,\qquad
e^{\mathfrak{t}^{e}(A)}(a,M)\enspace\text{iff}\enspace a\in M\qquad
I^{\mathfrak{t}^{e}(A)}(a,a^{\prime})\enspace\text{iff}\enspace a=a^{\prime}$

Let
$\mathfrak{t}^{e}_{\text{nc}}\colon\mathcal{R}^{S}_{0}(\sigma^{e})\rightarrow\mathcal{R}^{S}_{\text{nc}}(\sigma^{e})$
be the codomain restriction of $\mathfrak{t}^{e}$. We can adapt the syntactic
translation stated in [42] to translate $\text{MSO}_{k}$ sentences in
signature $\sigma$ (i.e. MSO sentences of quantifier rank ${\leq}\,k$) to
$\text{FO}_{k}(S,J)$ sentences in $\sigma^{e}$. Linking this syntactic
translation to the semantic translation $\mathfrak{t}^{e}$ and utilizing
proposition 4.2, we are able to capture $\equiv_{\text{MSO}_{k}}$ using the
many-sorted $\mathbb{E}_{k}$ and $\mathbb{E}_{k}^{\text{nc}}$:

######  Theorem 4.3.

$A\equiv_{\text{MSO}_{k}}B$ iff
$\mathfrak{t}^{e}A\leftrightarrow_{\mathbb{E}_{k}}\mathfrak{t}^{e}B$ iff
$\mathfrak{t}^{e}A\leftrightarrow_{\mathbb{E}_{k}^{\text{nc}}}\mathfrak{t}^{e}B$

The last equivalence follows from the second item of proposition 4.2 as the
condition is satisfied by $J=\\{\mathbf{f}\\}$ and
$\mathbf{cs}(\sigma^{e},\mathbf{f})=\mathbf{cs}(\sigma)$. Next we also adapt
definition 3.10 to this setting.

######  Definition 4.4.

We say that $H$ is _MSO -$(\mathbb{C}_{1},\dots,\mathbb{C}_{n+1})$-smooth_ if
it is $(\mathbb{C}_{1},\dots,\mathbb{C}_{n+1})$-smooth relative to
$\mathfrak{t}_{1},\dots,\mathfrak{t}_{n+1}$ where each
$\mathfrak{t}_{i}\colon\mathcal{R}_{0}(\sigma_{i})\to\mathcal{C}_{i}$ is a
codomain restriction of the MSO translation functor
$\mathfrak{t}^{e}\colon\mathcal{R}_{0}(\sigma_{i})\to\mathcal{R}^{S}(\sigma^{e}_{i})$.

As before, proposition 3.9 and theorem 4.3 imply that the
MSO-$\mathbb{E}_{k}$-smooth (or MSO-$\mathbb{E}_{k}^{\text{nc}}$-smooth)
functors preserve $\equiv_{\text{MSO}_{k}}$.

###  4.3 Example: edge creation

In this section, we demonstrate the ${\operatorname{join}_{\bar{i}}^{R}}$
operation is MSO-$\mathbb{E}_{k}$-smooth. Since this operation is used in
generating structures of bounded clique-width, this is a step towards
recovering Courcelle’s theorem for bounded clique-width structures using our
comonadic framework.

By definition the functor
${\operatorname{join}_{\bar{i}}^{R}}\colon\mathcal{R}(\sigma_{m})\rightarrow\mathcal{R}(\sigma_{m})$
only changes the interpretation of $R\in\sigma_{m}$. In the two-sorted setting
of $\sigma^{e}$, we define a variant of this functor
${\operatorname{join}_{\bar{i}}^{R,e}}$ of type
$\mathcal{R}^{S}(\sigma^{e}_{m})\rightarrow\mathcal{R}^{S}(\sigma^{e}_{m})$
which only changes interpretation of the corresponding $R\in\sigma^{e}_{m}$
with arity $\langle\mathbf{f},\dots,\mathbf{f}\rangle$. This ensures that
there is an isomorphism
$\theta:{\operatorname{join}_{\bar{i}}^{R,e}}(\mathfrak{t}^{e}(A))\cong\mathfrak{t}^{e}({\operatorname{join}_{\bar{i}}^{R}}(A))$,
for any $\sigma_{m}$-structure $A$. In addition to the existence of $\theta$,
in order for ${\operatorname{join}_{\bar{i}}^{R}}$ to be
MSO-$\mathbb{E}_{k}$-smooth, we need a smooth Kleisli law

$\kappa\colon\mathbb{E}_{k}\circ{\operatorname{join}_{\bar{i}}^{R,e}}\rightarrow{\operatorname{join}_{\bar{i}}^{R,e}}\circ\mathbb{E}_{k}.$

The components of $\kappa_{A}$ are given by $S$-sorted functions where
$\kappa_{A,t}$ sends a word
$w\in(\mathbb{E}_{k}({\operatorname{join}_{\bar{i}}^{R,e}}(A)))_{t}$ to the
same word $w\in({\operatorname{join}_{\bar{i}}^{R,e}}(\mathbb{E}_{k}(A)))_{t}$
for $t\in S=\\{\mathbf{f},\mathbf{m}\\}$. The proof that this $\kappa$
satisfies (S1) and (S2) is a direct adaptation of the single-sorted proof (cf.
section 3.6).

######  Lemma 4.5.

For every $r$-ary relation $R\in\sigma$ and $r$-tuple of labels $\vv{i}$, the
operation ${\operatorname{join}_{\bar{i}}^{R}}$ is
MSO-$\mathbb{E}_{k}$-smooth.

###  4.4 Example: twisted sums

Here we show that
$\mathbin{\parallel}\colon\mathcal{R}_{0}(\sigma_{1})\times\mathcal{R}_{0}(\sigma_{2})\to\mathcal{R}_{0}(\sigma_{3})$,
defined in section 3.7, is MSO-$\mathbb{E}_{k}^{\text{nc}}$-smooth. To this
end, we define a “twisted sum” functor

$\bowtie\colon\mathcal{R}^{S}_{\text{nc}}(\sigma_{1}^{e})\times\mathcal{R}^{S}_{\text{nc}}(\sigma_{2}^{e})\to\mathcal{R}^{S}_{\text{nc}}(\sigma_{3}^{e})$

as the lift of $\mathbin{\parallel}$ along $\mathfrak{t}^{e}$. For
$A\in\mathcal{R}^{S}_{\text{nc}}(\sigma_{1}^{e})$ and
$B\in\mathcal{R}^{S}_{\text{nc}}(\sigma_{2}^{e})$, the
$\sigma^{I}_{3}$-structure reduct of $A\bowtie B$ is precisely
$A^{\prime}\mathbin{\parallel}B^{\prime}$ where $A^{\prime}$ and $B^{\prime}$
are the $\sigma^{I}_{1}$– and $\sigma^{I}_{2}$-reducts of $A$ and $B$,
respectively. As before, we have the map $\mathfrak{i}\colon
A_{\mathbf{f}}+B_{\mathbf{f}}\to(A_{\mathbf{f}}+B_{\mathbf{f}})/_{\approx}$.
What remains to define is the second sort $(A\bowtie B)_{\mathbf{m}}$, which
is just $A_{\mathbf{m}}\times B_{\mathbf{m}}$, and the relation $e^{A\bowtie
B}$, which is the set $\\{(\mathfrak{i}(a),(a^{\prime},b^{\prime}))\mid
e^{A}(a,a^{\prime}),\,b^{\prime}\in
B_{\mathbf{m}}\\}\cup\\{(\mathfrak{i}(b),(a^{\prime},b^{\prime}))\mid
a^{\prime}\in A_{\mathbf{m}},\,e^{B}(b,b^{\prime})\\}$.

We now define the natural transformation
$\theta\colon\mathfrak{t}^{e}(A)\bowtie\mathfrak{t}^{e}(B)\to\mathfrak{t}^{e}(A\mathbin{\parallel}B)$.
In the $\mathbf{f}$-sort it is just the identity function and in the
$\mathbf{m}$-sort we send the pair $(M,N)$ of subsets $M\subseteq A$ and
$N\subseteq B$ to the subset $\mathfrak{i}(M)\cup\mathfrak{i}(N)$ of
$A\mathbin{\parallel}B$. Clearly, $\theta$ is a strong onto homomorphism in
$\mathcal{R}^{S}_{\text{nc}}(\sigma^{e}_{3})$ and, therefore,
$F^{\mathbb{E}_{k}^{\text{nc}}}(\theta)$ is an open pathwise embedding.

Lastly, we need a smooth Kleisli law
$\kappa\colon\mathbb{E}_{k}^{\text{nc}}(A\bowtie
B)\to\mathbb{E}_{k}^{\text{nc}}(A)\bowtie\mathbb{E}_{k}^{\text{nc}}(B)$.
Analogously to section 3.7, define $\mathtt{ex}_{1}$ by sending a word
$w=[x_{1}:s_{1},\dots,x_{n}:s_{n}]$ from $\mathbb{E}_{k}^{\text{nc}}(A\bowtie
B)$ to $\mathtt{ex}_{1}(w)=[y_{i}:s_{i}\mid
x_{i}\in\mathfrak{i}(A_{\mathbf{f}})\text{ or }s_{i}=\mathbf{m}]$, where
$y_{i}=a$ if $x_{i}=\mathfrak{i}(a)$ or $y_{i}=a^{\prime}$ if
$s_{i}=\mathbf{m}$ and $x_{i}=(a^{\prime},b^{\prime})$. Then,
$\mathtt{ex}_{2}$ is defined dually. We define $\kappa(w)$, for a non-constant
$w$, as $\mathtt{ex}_{1}(w)$ if
$\varepsilon(w)\in\mathfrak{i}(A_{\mathbf{f}})$, $\mathtt{ex}_{2}(w)$ if
$\varepsilon(w)\in\mathfrak{i}(B_{\mathbf{f}})$ and as
$(\mathtt{ex}_{1}(w),\mathtt{ex}_{2}(w))$ for $w$ from the $\mathbf{m}$-sort.

######  Proposition 4.6.

$\kappa$ is a smooth Kleisli law and $\mathbin{\parallel}$ is
MSO-$\mathbb{E}_{k}^{\text{nc}}$-smooth.

###  4.5 Extensions of MSO

The generality of definition 3.10 and the many-sorted $\mathbb{E}_{k}$ allows
us to adapt our approach to proving FVM and consequently Courcelle theorems
for fragments and extensions of (monadic) second order logic. We can
accomplish this by choosing the appropriate translation functors
$\mathfrak{t}$. For example, the logic $\text{MSO}2$, which allows
quantification over subsets of tuples in relations, could be captured by
having a sort $\mathbf{s}_{R}$ for each relation $R\in\sigma$ and the
translation functor $\mathfrak{t}$ on a structure $A$ sets
$\mathfrak{t}(A)_{\mathbf{s}_{R}}$ to $\mathcal{P}(R^{A})$. Similar
translations can be tailored for weak MSO, counting MSO, and $n$-adic second-
order logic.

######  Remark 4.7 (Failure of FVM theorems).

Unlike the case of FO in example 3.18, there famously fails to be a FVM
product theorem for MSO (see e.g. [32]). In our framework, the failure of
$\times$ to be MSO-$\mathbb{E}_{k}$-smooth is demonstrated by the non-
existence of a natural transformation
$\theta:\mathfrak{t}^{e}(A)\times\mathfrak{t}^{e}(B)\rightarrow\mathfrak{t}^{e}(A\times
B)$ where the components of $F^{\mathbb{E}_{k}}(\theta)$ are open pathwise
embeddings. Similarly, the non-existence of a suitable $\theta$ or smooth
Kleisli law $\kappa$ could be used to demonstrate the impossibility of a FVM
product theorem for $\text{MSO}2$ and a FVM coproduct theorem for $n$-adic
second-order logic with $n\geq 2$.

##  5 Comonadic Courcelle’s theorems

In the following we state an abstract version of Courcelle’s theorem, for
classes of $\tau$-structures given by a _$\tau$ -presentation
$\left<\mathcal{B},\mathcal{H}\right>$ over $\Sigma$_. This is specified by

  * •

a finite set of signatures $\Sigma$, which are extensions of $\tau$,

  * •

a finite set of generators $\mathcal{B}$, where each $B\in\mathcal{B}$ is an
object of $\mathcal{R}_{0}(\sigma)$, for some $\sigma\in\Sigma$, and

  * •

a finite set of operations $\mathcal{H}$, where each $H\in\Sigma$ is a functor
$\prod_{i=1}^{n}\mathcal{R}_{0}(\sigma_{i})\to\mathcal{R}_{0}(\sigma)$, with
$\sigma\in\Sigma$ and $\sigma_{i}\in\Sigma$, for every $i$.

Intuitively, $\left<\mathcal{B},\mathcal{H}\right>$ is a presentation of the
class $\Gamma\subseteq\mathcal{R}_{0}(\tau)$ where $A\in\Gamma$ if and only if
there is a term $t_{A}$ using objects $B\in\mathcal{B}$ as constants and
functors $H\in\mathcal{H}$ as operations, such that the $\tau$-structure
reduct of $t_{A}$ is isomorphic to $A$. Examples of classes with such
presentations are the classes of structures of tree-width ${\leq}\,k$ or
clique-width ${\leq}\,k$. These are the focus of our attention in the
following sections, once we state our comonadic Courcelle theorem.

To this end, we say that a comonad $\mathbb{C}$ over $\mathcal{B}$ has _finite
$\mathfrak{t}$-type_, for a functor
$\mathfrak{t}\colon\mathcal{A}\to\mathcal{B}$, if the equivalence relation
$\leftrightarrow_{\mathbb{C}}^{\mathfrak{t}}$ has finitely many equivalence
classes, where $A\leftrightarrow_{\mathbb{C}}^{\mathfrak{t}}B$ iff
$\mathfrak{t}A\leftrightarrow_{\mathbb{C}}\mathfrak{t}B$. A standard tree-
automata argument yields the following.

######  Theorem 5.1.

Let $\Delta$ be a class of $\tau$-structures and let
$\left<\mathcal{B},\mathcal{H}\right>$ be a $\tau$-presentation over
$\sigma_{1}$, …, $\sigma_{n}$ and, for $1\leq i\leq n$ let
$\mathfrak{t}_{i}\colon\mathcal{R}_{0}(\sigma_{i})\to\mathcal{C}_{i}$ be a
functor and $\mathbb{C}_{i}$ a comonad over $\mathcal{C}_{i}$. Assume further
that

  1. 1.

$\mathcal{C}_{i}$ is a category with a proper factorisation system,

  2. 2.

$\mathbb{C}_{i}$ has finite $\mathfrak{t}_{i}$-type, preserves embeddings and
$\mathsf{EM}(\mathbb{C}_{i})$ has equalisers of reflexive pairs,

  3. 3.

operations in $\mathcal{H}$ are $(\vv{\mathbb{C}_{i}})$-smooth relative to
$\vv{\mathfrak{t}_{i}}$, and

  4. 4.

for every $1\leq i\leq n$, the class of $\sigma_{i}$-structures with their
$\tau$-structure reduct in $\Delta$ is closed under
$\leftrightarrow_{\mathbb{C}_{i}}^{\mathfrak{t}_{i}}$.

Then there exists an algorithm, which for a given $\tau$-structure $A$ given
as a term $t_{A}$ of $\left<\mathcal{B},\mathcal{H}\right>$, decides
$A\in\Delta$ in linear time, in the size of $t_{A}$.

This theorem directly applies to our setting of
MSO-$\mathbb{E}_{k}^{\text{nc}}$-smooth operations. Indeed, the (surjective,
strong injective) factorisation system of $\mathcal{R}^{S}(\sigma^{e})$
restricts to $\mathcal{R}^{S}_{\text{nc}}(\sigma^{e})$. Further, observe that
$\mathbb{E}_{k}^{\text{nc}}$ preserves embeddings, has finite
$\mathfrak{t}^{e}_{\text{nc}}$-type, because there are only finitely many
$\equiv_{\text{MSO}_{k}}$-equivalence classes (cf. proposition 4.2), and the
category $\mathsf{EM}(\mathbb{E}_{k}^{\text{nc}})$ has equalisers (cf. lemma
3.8). An MSO sentence $\varphi$ of quantifier rank ${\leq}\,k$, in signature
$\tau$, defines the class $\Delta_{\varphi}$ of $\tau$-structures such that
$A\in\Delta_{\varphi}$ iff $A\models\alpha$. Observe that $\Delta_{\varphi}$
automatically satisfies item 4 in theorem 5.1. Indeed, $\varphi$ is a valid
MSO sentence in any signature $\sigma$ extending $\tau$. Consequently, if
$A\leftrightarrow_{\mathbb{E}_{k}}^{e}B$ and the $\tau$-structure reduct of
$A$ is in $\Delta_{\varphi}$ then so is $B$. Therefore:

######  Corollary 5.2.

Let $\left<\mathcal{B},\mathcal{H}\right>$ be a $\tau$-presentation and
$\varphi$ be a MSO sentence in signature $\tau$ of quantifier rank
${\leq}\,k$.

If every $H\in\mathcal{H}$ is MSO-$\mathbb{E}_{k}^{\text{nc}}$-smooth then
there is an algorithm deciding $A\models\varphi$, for an arbitrary $A$ given
as a term $t_{A}$ of $\left<\mathcal{B},\mathcal{H}\right>$, running in linear
time, in the size of $t_{A}$.

###  5.1 Courcelle’s tree-width theorem

Tree-width is an important, well-understood graph parameter, popularised by
the work of Robertson–Seymour on graph minors [39]. It is well-known [11, 12]
that a graph or, more generally a $\sigma$-structure, has tree-width ${<}\,m$
if and only if it belongs to the class presented by
$\left<\mathcal{B}_{tw},\mathcal{H}_{tw}\right>$ over $\Sigma_{tw}$ where

  * •

$\Sigma_{tw}=\\{\sigma_{C}\mid C\subseteq\\{c_{1},\dots,c_{m}\\}\\}$ where
$\sigma_{C}$ the extension of $\sigma$ by constants in $C$,

  * •

$\mathcal{B}_{tw}$ consists of all $\sigma_{C}$-structures on ${\leq}\,m$
vertices, with $C\subseteq\\{c_{1},\dots,c_{m}\\}$, and

  * •

$\mathcal{H}_{tw}$ consists of all parallel sums $\mathbin{\parallel}$ of type
$\mathcal{R}(\sigma_{C})\times\mathcal{R}(\sigma_{D})\to\mathcal{R}(\sigma_{C\cup
D})$, for every $C,D$, and operations
$\operatorname{fg}_{C,D}\colon\mathcal{R}(\sigma_{C})\to\mathcal{R}(\sigma_{D})$,
for $D\subseteq C$, where $\operatorname{fg}_{C,D}(A)$ is the
$\sigma_{D}$-structure reduct of the $\sigma_{C}$-structure $A$.

In proposition 4.6 we have established that the parallel sum operations in
$\mathcal{H}$ are MSO-$\mathbb{E}_{k}^{\text{nc}}$-smooth. Furthermore,
checking smoothness for $\operatorname{fg}_{C,D}$ is also straightforward.
Consequently, corollary 5.2 for
$\left<\mathcal{B}_{tw},\mathcal{H}_{tw}\right>$ entails the classical
Courcelle’s theorem.

######  Theorem 5.3.

Let $\varphi$ be a MSO sentence in signature $\tau$ of quantifier rank
${\leq}\,k$. Then, there exists an algorithm deciding $A\models\varphi$, for
an arbitrary $A$ given by a term $t_{A}$ of
$\left<\mathcal{B}_{tw},\mathcal{H}_{tw}\right>$, running in linear time, in
the size of $t_{A}$.

######  Remark 5.4.

In traditional presentations of Courcelle’s theorem, the algorithm first
computes the term $t_{A}$, given a structure $A$ of tree-width $\leq k$. This
part of the algorithm also runs in linear time in the size of $A$ [7].

###  5.2 Courcelle’s clique-width theorem

In order to recover Courcelle’s theorem for structures of bounded clique-width
as a corollary of theorem 5.1, we note that the class of structures of clique-
width $\leq m$ is given by the $\sigma$-presentation
$\left<\mathcal{B}_{cw},\mathcal{H}_{cw}\right>$ over $\Sigma_{cw}$ where

  * •

$\Sigma_{cw}=\\{\sigma_{m}\\}$, recall that
$\sigma_{m}=\sigma\cup\\{P_{1},\dots,P_{m}\\}$ with each $P_{i}(\cdot)$ unary

  * •

$\mathcal{B}_{cw}$ is the set of $\sigma_{m}$-strutures
$\\{v_{1},\dots,v_{m}\\}$ where $v_{i}$ is the singleton $\\{*\\}$ such that
$P^{v_{i}}_{i}=\\{*\\}$ and $R^{v_{i}}=\varnothing$ for all
$R\in\sigma_{m}\setminus\\{P_{i}\\}$

  * •

$\mathcal{H}_{cw}$ consists of coproducts $\oplus$ of type
$\mathcal{R}_{0}(\sigma_{m})\times\mathcal{R}_{0}(\sigma_{m})\to\mathcal{R}_{0}(\sigma_{m})$,
edge-creation operations ${\operatorname{join}_{\bar{i}}^{R}}$ for all
$R\in\sigma$ of arity $r$ with $\vv{i}\in\\{1,\dots,m\\}^{r}$, and relabeling
operations $\operatorname{relab}_{i,j}$ for all $i,j\in\\{1,\dots,m\\}$. The
relabeling operation $\operatorname{relab}_{i,j}$ ‘recolours’ elements of
colour $i$ with the colour $j$:

$P^{\operatorname{relab}_{i,j}(A)}_{j}=P^{A}_{i}\cup P^{A}_{j}\qquad
P^{\operatorname{relab}_{i,j}(A)}_{i}=\varnothing\qquad
R^{\operatorname{relab}_{i,j}(A)}=R^{A}\text{, for
}R\in\sigma_{m}\setminus\\{P_{i},P_{j}\\}$

The coproduct $\oplus$ of type
$\mathcal{R}_{0}(\sigma_{m})\times\mathcal{R}_{0}(\sigma_{m})\to\mathcal{R}_{0}(\sigma_{m})$
is a special case of the MSO-$\mathbb{E}_{k}$-smooth operation
$\mathbin{\parallel}$ mentioned in proposition 4.6. In lemma 4.5 we
established all the edge-creation operations
${\operatorname{join}_{\bar{i}}^{R}}$ are MSO-$\mathbb{E}_{k}$-smooth.
Verifying that the relabeling operations $\operatorname{relab}_{i,j}$ are
MSO-$\mathbb{E}_{k}$-smooth is straightforward. Consequently, corollary 5.2
for $\left<\mathcal{B}_{cw},\mathcal{H}_{cw}\right>$ entails Courcelle’s
theorem for bounded clique-width structures.

######  Theorem 5.5.

Let $\varphi$ be a MSO sentence in signature $\tau$ of quantifier rank
${\leq}\,k$. Then, there exists an algorithm deciding $A\models\varphi$, for
an arbitrary $A$ given by a term $t_{A}$ of
$\left<\mathcal{B}_{cw},\mathcal{H}_{cw}\right>$, running in linear time, in
the size of $t_{A}$.

##  6 Conclusion

We presented a general semantic framework for FVM-type theorems, based on
distributive laws. By varying the choice of game comonads, our results are
parametric in the logic of interest, and yield FVM-type results for the logic.
Moreover, we proved several new FVM-type results for positive existential and
counting quantifier variants of these logics by applying theorem 3.5 to the
relevant game comonad. We combined this with a game comonadic semantics for
monadic second order model equivalence. Both were illustrated by many
examples, including FVM-type results spanning these different logics, and
detailed expositions of the key operations for constructing graphs of bounded
tree-width and clique-width. Combining our accounts of FVM-type theorems and
monadic second order logic, we presented an abstract Courcelle theorem. This
theorem was then instantiated to recover concrete tree-width and clique-width
Courcelle theorems.

For reasons of exposition we have concentrated on relational structures. In
fact theorem 5.1, and other results, can be stated much more generally. It
would be interesting to explore algorithmic meta-theorems in such broader
settings, for example [8].

The original Feferman-Vaught theorem [18] deals with operations on indexed
families of structures, with the indexing itself carrying structure. We have
not needed this level of generality in the present work, but the extension to
account for this wider class of operations would be a natural next step.

## References

  * [1] Samson Abramsky, Anuj Dawar, and Pengming Wang.  The pebbling comonad in finite model theory.  In 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017, Reykjavik, Iceland, June 20-23, 2017, pages 1–12. IEEE Computer Society, 2017.  doi:10.1109/LICS.2017.8005129.
  * [2] Samson Abramsky and Dan Marsden.  Comonadic semantics for guarded fragments.  In 36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021, Rome, Italy, June 29 - July 2, 2021, pages 1–13. IEEE, 2021.  doi:10.1109/LICS52264.2021.9470594.
  * [3] Samson Abramsky and Luca Reggio.  Arboreal categories and resources.  In Nikhil Bansal, Emanuela Merelli, and James Worrell, editors, 48th International Colloquium on Automata, Languages, and Programming, ICALP 2021, July 12-16, 2021, Glasgow, Scotland (Virtual Conference), volume 198 of LIPIcs, pages 115:1–115:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021.  doi:10.4230/LIPIcs.ICALP.2021.115.
  * [4] Samson Abramsky and Nihil Shah.  Relating structure and power: Comonadic semantics for computational resources.  Journal of Logic and Computation, 31(6):1390–1428, 2021.
  * [5] Samson Abramsky and Nikos Tzevelekos.  Introduction to categories and categorical logic.  In New structures for physics, pages 3–94. Springer, 2010.
  * [6] Steve Awodey.  Category theory.  Oxford University Press, 2010.
  * [7] Hans L. Bodlaender.  Treewidth: Algorithmic techniques and results.  In International Symposium on Mathematical Foundations of Computer Science, pages 19–36. Springer, 1997.
  * [8] Benjamin A. Burton and Rodney G. Downey.  Courcelle’s theorem for triangulations.  J. Comb. Theory, Ser. A, 146:264–294, 2017.  doi:10.1016/j.jcta.2016.10.001.
  * [9] Adam Ó Conghaile and Anuj Dawar.  Game comonads & generalised quantifiers.  In Christel Baier and Jean Goubault-Larrecq, editors, 29th EACSL Annual Conference on Computer Science Logic, CSL 2021, January 25-28, 2021, Ljubljana, Slovenia (Virtual Conference), volume 183 of LIPIcs, pages 16:1–16:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021.  doi:10.4230/LIPIcs.CSL.2021.16.
  * [10] Bruno Courcelle.  The monadic second-order logic of graphs. I. Recognizable sets of finite graphs.  Information and computation, 85(1):12–75, 1990.
  * [11] Bruno Courcelle.  Graph grammars, monadic second-order logic and the theory of graph minors.  Contemporary Mathematics, 147:565–565, 1993.
  * [12] Bruno Courcelle and Joost Engelfriet.  Graph structure and monadic second-order logic: a language-theoretic approach, volume 138.  Cambridge University Press, 2012.
  * [13] Bruno Courcelle, Johann A Makowsky, and Udi Rotics.  Linear time solvable optimization problems on graphs of bounded clique-width.  Theory of Computing Systems, 33(2):125–150, 2000.
  * [14] Anuj Dawar, Tomás Jakl, and Luca Reggio.  Lovász-type theorems and game comonads.  In 36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021, Rome, Italy, June 29 - July 2, 2021, pages 1–13. IEEE, 2021.  doi:10.1109/LICS52264.2021.9470609.
  * [15] Brian Day.  On closed categories of functors.  In Reports of the Midwest Category Seminar IV, pages 1–38. Springer, 1970.
  * [16] Andrzej Ehrenfeucht.  An application of games to the completeness problem for formalized theories.  Fund. Math, 49(129-141):13, 1961.
  * [17] Samuel Eilenberg and John C. Moore.  Adjoint functors and triples.  Illinois Journal of Mathematics, 9(3):381–398, 1965.
  * [18] Solomon Feferman and Robert L. Vaught.  The first order properties of products of algebraic systems.  Journal of Symbolic Logic, 32(2):57–103, 1967.
  * [19] Roland Fraïssé.  Sur quelques classifications des relations, basées sur des isomorphismes restreints.  Publications Scientifiques de l’Université d’Alger. Série A (mathématiques), 2:273–295, 1955.
  * [20] Peter J. Freyd and G. Max Kelly.  Categories of continuous functors, I.  Journal of Pure and Applied Algebra, 2(3):169–191, 1972.
  * [21] Yuri Gurevich.  Modest theory of short chains. I.  The Journal of Symbolic Logic, 44(4):481–490, 1979.
  * [22] Yuri Gurevich.  Monadic second-order theories.  In J. Barwise and S. Feferman, editors, Model-theoretic logics, pages 479–506. Cambridge University Press, 1985.
  * [23] Matthew Hennessy and Robin Milner.  On observing nondeterminism and concurrency.  In International Colloquium on Automata, Languages, and Programming, pages 299–309. Springer, 1980.
  * [24] Bart Jacobs.  Semantics of weakening and contraction.  Annals of Pure and Applied Logic, 69(1):73–106, 1994.
  * [25] Heinrich Kleisli.  Every standard construction is induced by a pair of adjoint functors.  Proceedings of the American Mathematical Society, 16(3):544–546, 1965.
  * [26] Anders Kock.  Monads on symmetric monoidal closed categories.  Archiv der Mathematik, 21(1):1–10, 1970.
  * [27] Anders Kock.  Closed categories generated by commutative monads.  Journal of the Australian Mathematical Society, 12(4):405–424, 1971\.
  * [28] Phokion G Kolaitis and Moshe Y Vardi.  Infinitary logics and 0–1 laws.  Information and computation, 98(2):258–294, 1992.
  * [29] H. Läuchli and J. Leonard.  On the elementary theory of linear order.  Fundamenta Mathematicae, 59(1):109–116, 1966.  URL: http://eudml.org/doc/213884.
  * [30] Leonid Libkin.  Elements of finite model theory, volume 41.  Springer, 2004.
  * [31] Fred E.J. Linton.  Coequalizers in categories of algebras.  In Seminar on triples and categorical homology theory, pages 75–90. Springer, 1969.
  * [32] Johann A Makowsky.  Algorithmic uses of the Feferman–Vaught theorem.  Annals of Pure and Applied Logic, 126(1-3):159–213, 2004.
  * [33] Ernest G. Manes.  Algebraic theories, volume 26.  Springer Science, 2012.
  * [34] Ernie Manes and Philip Mulry.  Monad compositions i: general constructions and recursive distributive laws.  Theory and Applications of Categories, 18(7):172–208, 2007.
  * [35] María Manzano.  Extensions of First Order Logic.  Cambridge University Press, 1996.
  * [36] Andrzej Mostowski.  On direct products of theories.  The Journal of Symbolic Logic, 17(1):1–31, 1952.
  * [37] Sang-il Oum and Paul Seymour.  Approximating clique-width and branch-width.  Journal of Combinatorial Theory, Series B, 96(4):514–528, 2006\.
  * [38] Thomas Paine.  A pebbling comonad for finite rank and variable logic, and an application to the equirank-variable homomorphism preservation theorem.  In Patricia Johann, editor, Proceedings of the 36th Conference on the Mathematical Foundations of Programming Semantics, MFPS 2020, Online, October 1, 2020, volume 352 of Electronic Notes in Theoretical Computer Science, pages 191–209. Elsevier, 2020.  doi:10.1016/j.entcs.2020.09.010.
  * [39] Neil Robertson and Paul D. Seymour.  Graph minors. II. Algorithmic aspects of tree-width.  Journal of algorithms, 7(3):309–322, 1986.
  * [40] Gavin Seal.  Tensors, monads and actions: Dedicated to the memory of Pawet Waszkiewicz.  Theory and Applications of Categories, 28:403–433, 01 2013.
  * [41] Saharon Shelah.  The monadic theory of order.  Annals of Mathematics, 102(3):379–419, 1975.
  * [42] Jouko Väänänen.  Second-order and Higher-order Logic.  In Edward N. Zalta, editor, The Stanford Encyclopedia of Philosophy. Metaphysics Research Lab, Stanford University, Fall 2021 edition, 2021.

##  Appendix A Omitted Proofs

In the following we make use of the following elementary properties of proper
factorisations systems.

######  Lemma A.1 (e.g. Section 2 in [20]).

Given a proper factorisation system $(\mathcal{E},\mathcal{M})$,

  1. 1.

$\mathcal{E}\cap\mathcal{M}=\mathrm{Iso}$,

  2. 2.

if $g\circ f\in\mathcal{E}$ then $g\in\mathcal{E}$ and, dually,
if $g\circ f\in\mathcal{M}$ then $f\in\mathcal{M}$,

  3. 3.

$\mathcal{E}$ contains all coequalisers and $\mathcal{M}$ all equalisers.

We confirm the following generalization to signatures with constants of
results in [4]. See 2.1

######  Proof A.2.

In the following $\mathbb{N}$ denotes the set of natural numbers, _not_ a
comonad. Fix a signature $\sigma$, potentially containing constant symbols. In
[1, 4] a pebbling comonad $\mathbb{P}_{k}$ for signatures without constants is
defined. In the proofs, the bound on the number of pebbles plays no essential
role, so we can equally define a comonad $\mathbb{P}_{\mathbb{N}}$ on
$\mathcal{R}(\mathbf{rel}(\sigma))$, with a pebble for each natural number.

The universe of $\mathbb{P}_{\mathbb{N}}(A)$ is $(\mathbb{N}\times A)^{+}$
with $p\in\mathbb{N}$. The counit extracts the second element of the tail of
its input list. For $R\in\mathbf{rel}(\sigma)$ of arity $n$,
$R^{\mathbb{P}_{\mathbb{N}}(A)}(s_{1},\ldots,s_{n})$ if:

  1. 1.

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

  2. 2.

If $s_{i}<s_{j}$, then the pebble index of the tail of $s_{i}$ does not appear
in the suffix of $s_{i}$ in $s_{j}$.

  3. 3.

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

The coextension of $h:\mathbb{P}_{\mathbb{N}}(A)\rightarrow B$ is given by:

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

Assuming $\mathbf{cs}(\sigma)$ has $m$ elements, with a specified linear
ordering $c_{0},\ldots,c_{m-1}$, we can restrict $\mathbb{P}_{\mathbb{N}}$ to
a comonad $\mathbb{P}_{m+\mathbb{N}}$, on $\mathcal{R}(\mathbf{rel}(\sigma))$,
by restricting to lists:

  1. 1.

With length greater than $m$.

  2. 2.

With the $m$ element prefix of each list being

$[(0,c^{A}_{0}),\ldots,(m-1,c^{A}_{m-1})]$

  3. 3.

The pebble indices in positions $m$ and above are greater than or equal to
$m$.

We then observe that this yields a comonad on $\mathcal{R}(\sigma)$ if we
define for $0\leq i<m$:

$c^{\mathbb{P}_{m+\mathbb{N}}(A)_{i}}:=[(0,c_{0}^{A},\ldots,(i,c_{i}^{A})]$

It is easy to confirm the counit and coextensions preserve the constant
elements.

We then define:

  * •

A comonad $\mathbb{E}$ as the restriction of $\mathbb{P}_{m+\mathbb{N}}$ to
lists of the form:

$[(0,a_{0}),(1,a_{1}),\ldots,(n,a_{n})]$

  * •

A comonad $\mathbb{M}$ as the restriction of $\mathbb{P}_{\mathbb{N}}$ to
lists of the form:

$[(0,a_{0}),(1,a_{1}),(0,a_{2}),\ldots,(\operatorname{parity}(n),a_{n})]$

such that $E^{A}(a_{i},a_{i+1})$ and $a_{0}=c^{A}_{0}$.

  * •

A comonad $\mathbb{P}$ as being $\mathbb{P}_{m+\mathbb{N}}$.

Then, up to isomorphism as comonads:

  * •

The comonad $\mathbb{E}_{k}$ is given by restricting $\mathbb{E}$ to lists of
at most $m+k$ elements.

  * •

The comonad $\mathbb{M}_{k}$ is given by restricting $\mathbb{M}$ to lists of
at most $1+k$ elements.

  * •

The comonad $\mathbb{P}_{k}$ is given by restricting $\mathbb{P}$ to lists
with pebble indices at most $m+k$.

In each case, it is routine to verify that coextensions preserve the
restricted class of lists.

The following is a standard result about lifting factorization systems to
Eilenberg-Moore categories. See 2.3

######  Proof A.3 (Proof sketch.).

It is clear that both $\overline{\mathcal{E}}$ and $\overline{\mathcal{M}}$
contain all isomorphisms and are closed under compositions. The factorisation
of a coalgebra morphism $h\colon(A,\alpha)\to(B,\beta)$ is computed as the
$(\mathcal{E},\mathcal{M})$-factorisation of the underlying morphism into a
quotient $e$ and an embedding $m$ as shown below.

${A}$${C}$${B}$${\mathbb{C}(A)}$${\mathbb{C}(C)}$${\mathbb{C}(B)}$$\scriptstyle{e}$$\scriptstyle{\alpha}$$\scriptstyle{m}$$\scriptstyle{\gamma}$$\scriptstyle{\beta}$$\scriptstyle{\mathbb{C}(e)}$$\scriptstyle{\mathbb{C}(m)}$

Since $\mathbb{C}$ restricts to embeddings, $\mathbb{C}(m)$ is an embedding
and so there exists a diagonal filler $\gamma$. It is immediate to check that
$\gamma$ is a $\mathbb{C}$-coalgebra.

Next, assume we have a commutative square of coalgebra morphisms, with
$e\in\overline{\mathcal{E}}$ and $m\in\overline{\mathcal{M}}$.

${(A,\alpha)}$${(B,\beta)}$${(A^{\prime},\alpha^{\prime})}$${(B^{\prime},\beta^{\prime})}$$\scriptstyle{e}$$\scriptstyle{u}$$\scriptstyle{v}$$\scriptstyle{d}$$\scriptstyle{m}$

By orthogonality of $e$ and $m$, there exists a unique diagonal filler $d$. It
is immediate to show that $d$ is a coalgebra morphism
$(B,\beta)\to(A^{\prime},\alpha^{\prime})$ from the fact that $e$ is
orthogonal to $\mathbb{C}(m)$.

The “furthermore” part follows from the definitions.

###  A.1 Proofs for section 3.1

See 3.1

######  Proof A.4.

Recall from section 9 in [4] that $\mathsf{EM}(\mathbb{E}_{k})$ can be
identified with the category of $\sigma$-structures equipped with forest order
$\sqsubseteq$ of depth ${\leq}\,k$ such that, for any relation symbol
$R\in\sigma$, $R^{A}(x_{1},\dots,x_{n})$ implies $x_{i}\sqsubseteq x_{j}$ or
$x_{j}\sqsubseteq x_{i}$ ($\forall i,j\in\\{1,\dots,n\\}$). The morphisms in
$\mathsf{EM}(\mathbb{E}_{k})$ are then the morphisms of $\sigma$-structures
which preserve the covering relation $\prec$, where $x\prec y$ iff
$x\sqsubseteq y$ and, for every $z$ such that $x\sqsubseteq z\sqsubseteq y$,
either $z=x$ or $z=y$.

It then follows from the definition of $\mathbin{\widehat{+}}$ (in terms of
the equaliser) that
$(A,\sqsubseteq^{A})\mathbin{\widehat{+}}(B,\sqsubseteq^{B})$ consists of
precisely the words $w\in\mathbb{E}_{k}(A+B)$ such that

  * •

the restriction of $w$ to the sub-word consisting of only letters from $A$, is
a path in $(A,\sqsubseteq^{A})$ and

  * •

similarly, the sub-word of $w$ with letters from $B$, is a path in
$(B,\sqsubseteq^{B})$

From this it is easy to see that, given open pathwise embeddings $f$ and $g$,
also $f\mathbin{\widehat{+}}g$ is an open pathwise-embedding, because checking
openness and being a pathwise embeddings for $f\mathbin{\widehat{+}}g$ is
decomposed into the corresponding properties of $f$ and $g$.

###  A.2 Proofs for section 3.2

We shall write $g\bullet f$ for composition in Kleisli categories. The
following result is well known if various forms, although full proofs are hard
to find in the literature. We explicitly confirm the details for the multi-
argument version that we require. See 3.4

######  Proof A.5.

Let $\kappa:\mathbb{D}\circ H\rightarrow H\circ\prod_{i}\mathbb{C}_{i}$ be a
Kleisli-law. For family of morphisms $f_{i}:\mathbb{C}_{i}A_{i}\rightarrow
B_{i}$, define $\overline{H}(\vv{f_{i}})$ as the composite:

${\mathbb{D}(H(\vv{A_{i}}))}$${H(\vv{\mathbb{C}_{i}A_{i}})}$${H(\vv{B_{i}})}$$\scriptstyle{\kappa_{A}}$$\scriptstyle{H(\vv{f_{i}})}$

That identities a preserved is immediate from ((F1)). For composition:

$\displaystyle\overline{H}(\vv{g_{i}\bullet f_{i}})$
$\displaystyle=\overline{H}(\vv{g_{i}\circ\mathbb{C}_{i}(f_{i})\circ\delta})$
$\displaystyle=H(\vv{g_{i}\circ\mathbb{C}_{i}(f_{i})\circ\delta})\circ\kappa$
$\displaystyle=H(\vv{g_{i}})\circ H(\vv{\mathbb{C}_{i}(f_{i})})\circ
H(\delta)\circ\kappa$ $\displaystyle=H(\vv{g_{i}})\circ
H(\vv{\mathbb{C}_{i}(f_{i})})\circ\kappa\mathbb{D}(\kappa)\circ\kappa$
$\displaystyle=H(\vv{g_{i}})\circ\kappa\circ\mathbb{D}(H(\vv{f_{i}}))\circ\mathbb{D}(\kappa)\circ\kappa$
$\displaystyle=\overline{H}(\vv{g_{i}})\bullet\overline{H}(\vv{f_{i}})$

The key step uses ((F2)). To confirm (2):

$\displaystyle\overline{H}(\vv{F_{\mathbb{C}_{i}}(f_{i})})$
$\displaystyle=\overline{H}(\vv{F_{\mathbb{C}_{i}}(f_{i})})$
$\displaystyle=\overline{H}(\vv{f_{i}\circ\varepsilon})$
$\displaystyle=H(\vv{f_{i}\circ\varepsilon})\circ\kappa$
$\displaystyle=H(\vv{f_{i}})\circ H(\vv{\varepsilon})\circ\kappa$
$\displaystyle=H(\vv{f_{i}})\circ\varepsilon$
$\displaystyle=F_{\mathbb{D}}(H(\vv{f_{i}}))$

Now assume we have $H$ and $\overline{H}$ satisfying (2). Note that for
$A_{i}$ a $\mathcal{C}_{i}$-object, $\mathrm{id}_{\mathbb{C}_{i}A_{i}}$ is a
morphism in $\mathsf{Kl}(\mathbb{C}_{i})$. Define:

$\kappa_{A}:=\overline{H}(\vv{\mathrm{id}_{\mathbb{C}_{i}A}})$

Which by (2) must be a $\mathcal{D}$-morphism of type
$\mathbb{D}(H(\vv{A_{i}}))\rightarrow H(\vv{\mathbb{C}_{i}(A_{i})})$. Noting
$\overline{H}(\vv{f_{i}\circ\varepsilon})=H(\vv{f_{i}})\circ\varepsilon$, we
establish naturality as follows:

$\displaystyle\kappa\circ\mathbb{D}H(\vv{f_{i}})$
$\displaystyle=\overline{H}(\vv{\mathrm{id}})\circ\mathbb{D}H(\vv{f_{i}})$
$\displaystyle=\overline{H}(\vv{\mathrm{id}})\circ\mathbb{D}H(\vv{f_{i}})\circ\mathbb{D}(\varepsilon)\circ\delta$
$\displaystyle=\overline{H}(\vv{\mathrm{id}})\circ\mathbb{D}H(\vv{f_{i}\circ\varepsilon})\circ\delta$
$\displaystyle=\overline{H}(\vv{\mathrm{id}})\bullet\overline{H}(\vv{f_{i}\circ\varepsilon})$
$\displaystyle=\overline{H}(\vv{\mathrm{id}\bullet(f_{i}\circ\varepsilon)})$
$\displaystyle=\overline{H}(\vv{\mathrm{id}\circ\mathbb{C}_{i}(f_{i})\circ\mathbb{C}_{i}(\varepsilon)\circ\delta})$
$\displaystyle=\overline{H}(\vv{\mathbb{C}_{i}(f_{i})})$
$\displaystyle=\overline{H}(\vv{\mathbb{C}_{i}(f_{i})\circ\varepsilon\circ\mathbb{C}_{i}(\mathrm{id})\circ\delta})$
$\displaystyle=\overline{H}(\vv{\mathbb{C}_{i}(f_{i})\circ\varepsilon)}\bullet\overline{H}(\mathrm{id})$
$\displaystyle=\overline{H}(\vv{\mathbb{C}_{i}(f_{i})})\circ\varepsilon\bullet\overline{H}(\mathrm{id})$
$\displaystyle=H(\vv{\mathbb{C}_{i}(f_{i})})\circ\varepsilon\circ\mathbb{D}\overline{H}(\mathrm{id})\circ\delta$
$\displaystyle=H(\vv{\mathbb{C}_{i}(f_{i})})\circ\overline{H}(\mathrm{id})\circ\varepsilon\circ\delta$
$\displaystyle=H(\vv{\mathbb{C}_{i}(f_{i})})\circ\kappa$

For axiom ((F1)):

$\displaystyle H(\varepsilon)\circ\kappa$
$\displaystyle=H(\varepsilon)\circ\overline{H}(\vv{\mathrm{id}})$
$\displaystyle=H(\varepsilon)\circ\overline{H}(\vv{\mathrm{id}})\circ\varepsilon\circ\delta$
$\displaystyle=H(\varepsilon)\circ\varepsilon\circ\mathbb{D}\overline{H}(\vv{\mathrm{id}})\circ\delta$
$\displaystyle=\overline{H}(\varepsilon\circ\varepsilon)\circ\mathbb{D}\overline{H}(\vv{\mathrm{id}})\circ\delta$
$\displaystyle=\overline{H}(\varepsilon\circ\varepsilon)\bullet\overline{H}(\vv{\mathrm{id}})$
$\displaystyle=\overline{H}(\vv{\varepsilon\circ\varepsilon\bullet\mathrm{id}})$
$\displaystyle=\overline{H}(\vv{\varepsilon\circ\varepsilon\circ\mathbb{C}_{i}(\mathrm{id})\circ\delta})$
$\displaystyle=\overline{H}(\vv{\varepsilon\circ\varepsilon\circ\delta})$
$\displaystyle=\overline{H}(\vv{\varepsilon})$ $\displaystyle=\varepsilon$

For axiom ((F2)):

$\displaystyle\kappa\circ\mathbb{D}(\kappa)\circ\delta$
$\displaystyle=\overline{H}(\vv{\mathrm{id}})\circ\mathbb{D}\overline{H}(\vv{\mathrm{id}})\circ\delta$
$\displaystyle=\overline{H}(\vv{\mathrm{id}})\bullet\overline{H}(\vv{\mathrm{id}})$
$\displaystyle=\overline{H}(\vv{\mathrm{id}\circ\mathrm{id}})$
$\displaystyle=\overline{H}(\vv{\mathrm{id}\circ\mathbb{C}_{i}(\mathrm{id})\circ\delta})$
$\displaystyle=\overline{H}(\vv{\delta})$
$\displaystyle=\overline{H}(\vv{\delta\circ\varepsilon\circ\mathbb{C}_{i}(\mathrm{id})\circ\delta})$
$\displaystyle=\overline{H}(\vv{\delta\circ\varepsilon\bullet\mathrm{id}})$
$\displaystyle=\overline{H}(\vv{\delta\circ\varepsilon})\bullet\overline{H}(\vv{\mathrm{id}})$
$\displaystyle=\overline{H}(\vv{\delta\circ\varepsilon})\circ\mathbb{D}\overline{H}(\vv{\mathrm{id}})\circ\delta$
$\displaystyle=H(\vv{\delta})\circ\varepsilon\circ\mathbb{D}\overline{H}(\vv{\mathrm{id}})\circ\delta$
$\displaystyle=H(\vv{\delta})\circ\overline{H}(\vv{\mathrm{id}})\circ\varepsilon\circ\delta$
$\displaystyle=H(\vv{\delta})\circ\overline{H}(\vv{\mathrm{id}})$
$\displaystyle=H(\vv{\delta})\circ\kappa$

Finally, we must check the two mappings exhibit a bijection. For
$\overline{H}$ satisfying (2):

$\displaystyle H(\vv{f_{i}})\circ\overline{H}(\vv{\mathrm{id}})$
$\displaystyle=H(\vv{f_{i}})\circ\overline{H}(\vv{\mathrm{id}})\circ\varepsilon\circ\delta$
$\displaystyle=H(\vv{f_{i}})\circ\varepsilon\mathbb{D}\overline{H}(\vv{\mathrm{id}})\circ\delta$
$\displaystyle=\overline{H}(\vv{f_{i}\circ\varepsilon})\circ\mathbb{D}\overline{H}(\vv{\mathrm{id}})\circ\delta$
$\displaystyle=\overline{H}(\vv{f_{i}\circ\varepsilon})\bullet\overline{H}(\vv{\mathrm{id}})$
$\displaystyle=\overline{H}(\vv{(f_{i}\circ\varepsilon)\bullet\mathrm{id}})$
$\displaystyle=\overline{H}(\vv{f_{i}\circ\varepsilon\circ\mathbb{C}_{i}(\mathrm{id})\circ\delta})$
$\displaystyle=\overline{H}(\vv{f_{i}\circ\varepsilon\circ\delta})$
$\displaystyle=\overline{H}(\vv{f_{i}})$

For $\overline{H}$ induced by a Kleisli-law:

$\displaystyle\overline{H}(\vv{\mathrm{id}})$
$\displaystyle=H(\vv{id})\circ\kappa=\kappa$

See 3.5

######  Proof A.6.

For preservation of $\leftrightarrows$, let $\overline{H}$ be the lifted
functor induced by $\kappa$. If for $1\leq i\leq n$,
$A_{i}\leftrightarrows_{\mathbb{C}_{i}}B_{i}$, then equivalently there are
$\mathsf{Kl}(\mathbb{C}_{i})$-morphisms
$f_{i}:F_{\mathbb{C}_{i}}(A_{i})\rightarrow F_{\mathbb{C}_{i}}(B_{i})$ and
$g_{i}:F_{\mathbb{C}_{i}}(B_{i})\rightarrow F_{\mathbb{C}_{i}}(A_{i})$.
Applying $\overline{H}$ yields $\mathsf{Kl}(\mathbb{D})$-morphisms:

$\displaystyle\overline{H}(\vv{F_{\mathbb{C}_{i}}(A_{i})})$
$\displaystyle\xrightarrow{\overline{H}(\vv{f_{i}})}\overline{H}(\vv{F_{\mathbb{C}_{i}}(B_{i})})\quad\mbox{
and}$ $\displaystyle\overline{H}(\vv{F_{\mathbb{C}_{i}}(B_{i})})$
$\displaystyle\xrightarrow{\overline{H}(\vv{f_{i}})}\overline{H}(\vv{F_{\mathbb{C}_{i}}(A_{i})})$

Then we note that
$\overline{H}(\vv{F_{\mathbb{C}_{i}}(A_{i})})=F_{\mathbb{D}}(H(\vv{A_{i}}))$
and similarly for the $B_{i}$’s, therefore
$H(\vv{A_{i}})\leftrightarrows_{\mathbb{D}}H(\vv{B_{i}})$.

The argument for preservation of $\cong_{\mathsf{Kl}}$ is similar, but in this
case we work with isomorphisms, which are preserved by functoriality.

###  A.3 Proofs for section 3.3

The following result appears in various guises in the literature [24, 40],
although with varying assumptions. We provide a full proof at the level of
generality we require. See 3.7

######  Proof A.7.

We note that the parallel pair:

${F^{\mathbb{D}}(H(\vv{A_{i}}))}$${F^{\mathbb{D}}(H(\vv{\mathbb{C}_{i}(A_{i})}))}$$\scriptstyle{F^{\mathbb{D}}(\kappa)\circ\delta}$$\scriptstyle{F^{\mathbb{D}}(H(\vv{\alpha_{i}}))}$

is reflexive, with mutual post-inverse $\mathbb{D}H(\varepsilon)$.

We define the action on morphisms of $\widehat{H}$ by the universal property
of equalizers, as in the following diagram:

${\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{\overline{H}(f_{i})}$$\scriptstyle{\iota_{\vv{\alpha_{i}}}}$$\scriptstyle{F^{\mathbb{D}}(H(\vv{f_{i}}))}$$\scriptstyle{\iota_{\vv{\beta_{i}}}}$$\scriptstyle{F^{\mathbb{D}}(\kappa)\circ\delta}$$\scriptstyle{F^{\mathbb{D}}(H(\vv{\beta_{i}}))}$

The parallel pair is equalized by the following calculation:

$\displaystyle F^{\mathbb{D}}(H(\vv{\beta_{i}}))\circ
F^{\mathbb{D}}(H(\vv{f_{i}}))\circ\iota_{\vv{\alpha_{i}}}$
$\displaystyle=\mathbb{D}H(\vv{\beta_{i}\circ
f_{i}})\circ\iota_{\vv{\alpha_{i}}}$
$\displaystyle=\mathbb{D}H(\vv{\mathbb{C}_{i}(f_{i})\circ\alpha_{i}})\circ\iota_{\vv{\alpha_{i}}}$
$\displaystyle=\mathbb{D}H(\vv{\mathbb{C}_{i}(f_{i})})\circ\mathbb{D}H(\vv{\alpha_{i}})\circ\iota_{\vv{\alpha_{i}}}$
$\displaystyle=\mathbb{D}H(\vv{\mathbb{C}_{i}(f_{i})})\circ\mathbb{D}(\kappa)\circ\delta\circ\iota_{\vv{\alpha_{i}}}$
$\displaystyle=\mathbb{D}(H(\vv{\mathbb{C}_{i}(f_{i})})\circ\kappa)\circ\delta\circ\iota_{\vv{\alpha_{i}}}$
$\displaystyle=\mathbb{D}(\kappa\circ\mathbb{D}H(\vv{f_{i}}))\circ\delta\circ\iota_{\vv{\alpha_{i}}}$
$\displaystyle=\mathbb{D}(\kappa)\circ\mathbb{D}^{2}(H(\vv{f_{i}}))\circ\delta\circ\iota_{\vv{\alpha_{i}}}$
$\displaystyle=\mathbb{D}(\kappa)\circ\delta\circ\mathbb{D}(H(\vv{f_{i}}))\circ\iota_{\vv{\alpha_{i}}}$
$\displaystyle=F^{\mathbb{D}}(\kappa)\circ\delta\circ
F^{\mathbb{D}}(H(\vv{f_{i}}))\circ\circ\iota_{\vv{\alpha_{i}}}$

As $\mathrm{id}_{\widehat{H}(\vv{\alpha_{i}})}$ makes the following commute:

${\widehat{H}(\vv{\alpha_{i}})}$${F^{\mathbb{D}}(H(\vv{A_{i}}))}$${\widehat{H}(\vv{\alpha_{i}})}$${F^{\mathbb{D}}(H(\vv{A_{i}}))}$$\scriptstyle{\iota_{\vv{\alpha_{i}}}}$$\scriptstyle{F^{\mathbb{D}}(H(\vv{\mathrm{id}}))}$$\scriptstyle{\iota_{\vv{\alpha_{i}}}}$

By the equalizer universal property
$\widehat{H}(\vv{\mathrm{id}})=\mathrm{id}$. The following diagram commutes:

${\widehat{H}(\vv{\alpha_{i}})}$${F^{\mathbb{D}}(H(\vv{A_{i}}))}$${\widehat{H}(\vv{\beta_{i}})}$${F^{\mathbb{D}}(H(\vv{B_{i}}))}$${\widehat{H}(\vv{\gamma_{i}})}$${F^{\mathbb{D}}(H(\vv{C_{i}}))}$$\scriptstyle{\widehat{H}(\vv{f_{i}})}$$\scriptstyle{\iota_{\vv{\alpha_{i}}}}$$\scriptstyle{F^{\mathbb{D}}(H(\vv{f_{i}}))}$$\scriptstyle{\widehat{H}(\vv{g_{i}})}$$\scriptstyle{\iota_{\vv{\beta_{i}}}}$$\scriptstyle{F^{\mathbb{D}}(H(\vv{g_{i}}))}$$\scriptstyle{\iota_{\vv{\gamma_{i}}}}$

Therefore by the universal property of equalizers, $\widehat{H}(\vv{g_{i}\circ
f_{i}})=\widehat{H}(\vv{g_{i}})\circ\widehat{H}(\vv{f_{i}})$. Therefore
$\widehat{H}$ is a well-defined functor. Note also that by construction
$\iota$ is natural of type $\widehat{H}\rightarrow F^{\mathbb{D}}\circ
H\circ\prod_{i}U^{\mathbb{C}_{i}}$.

The composite $\mathbb{D}(\kappa)\circ\delta$ is a morphism of type
$F^{\mathbb{D}}(H(\vv{A_{i}}))\rightarrow
F^{\mathbb{D}}(H(\vv{\mathbb{C}_{i}(A_{i})}))$ as:

$\delta\circ\mathbb{D}(\kappa)\circ\delta=\mathbb{D}^{2}(\kappa)\circ\delta\circ\delta=\mathbb{D}^{2}(\kappa)\circ\mathbb{D}(\delta)\circ\delta=\mathbb{D}(\mathbb{D}(\kappa)\circ\delta)\circ\delta$

We also note $\mathbb{D}(\kappa)\circ\delta$ equalizes
$F^{\mathbb{D}}(\kappa)\circ\delta$ and $F^{\mathbb{D}}(H(\vv{\delta}))$ as:

$\displaystyle\mathbb{D}(\kappa)\circ\delta\circ\mathbb{D}(\kappa)\circ\delta$
$\displaystyle=\mathbb{D}(\kappa)\circ\mathbb{D}^{2}(\kappa)\circ\delta\circ\delta$
$\displaystyle=\mathbb{D}(\kappa)\circ\mathbb{D}^{2}(\kappa)\circ\mathbb{D}(\delta)\circ\delta$
$\displaystyle=\mathbb{D}H(\vv{\delta})\circ\mathbb{D}(\kappa)\circ\delta$

Assuming $f$ equalizes $F^{\mathbb{D}}{\kappa}\circ\delta$ and
$F^{\mathbb{D}}(H(\vv{\delta}))$, then:

$\displaystyle\mathbb{D}(\kappa)\circ\delta\circ\mathbb{D}H(\vv{\varepsilon})\circ
f$
$\displaystyle=\mathbb{D}(\kappa)\circ\mathbb{D}^{2}(H(\vv{\varepsilon}))\circ\delta\circ
f$
$\displaystyle=\mathbb{D}(\kappa\circ\mathbb{D}H(\vv{\varepsilon}))\circ\delta\circ
f$
$\displaystyle=\mathbb{D}(H(\mathbb{C}_{i}\varepsilon)\circ\kappa)\circ\delta\circ
f$
$\displaystyle=\mathbb{D}(H(\mathbb{C}_{i}\varepsilon))\circ\mathbb{D}(\kappa)\circ\delta\circ
f$
$\displaystyle=\mathbb{D}(H(\mathbb{C}_{i}\varepsilon))\circ\mathbb{D}(H(\vv{\delta}))\circ
f$ $\displaystyle=f$

$\mathbb{D}(\kappa)\circ\delta$ is split mono as:

$\mathbb{D}H(\vv{\varepsilon}))\circ\mathbb{D}(\kappa)\circ\delta=\mathbb{D}(\varepsilon)\circ\delta=\mathrm{id}$

Therefore the following is an equalizer diagram:

${\widehat{H}(\vv{\delta})}$${F^{\mathbb{D}}(H(\vv{\mathbb{C}_{i}(A_{i})}))}$${F^{\mathbb{D}}(H(\vv{\mathbb{C}^{2}_{i}(A_{i})}))}$$\scriptstyle{\mathbb{D}(\kappa)\circ\delta}$$\scriptstyle{F^{\mathbb{D}}(\kappa)\circ\delta}$$\scriptstyle{F^{\mathbb{D}}(H(\vv{\delta}))}$

with $\mathbb{D}H(\vv{\varepsilon})\circ f$ the unique fill-in for a given
$f$. Therefore there is an induced isomorphism:

$\widehat{H}(\vv{F^{\mathbb{C}}(A_{i})})\xrightarrow{\tilde{\iota_{\vv{\delta}}}}F^{\mathbb{D}}(H(\vv{A_{i}})).$

Then we calculate:

$\displaystyle\mathbb{D}(\kappa)\circ\delta\circ
F^{\mathbb{D}}(H(\vv{f_{i}}))\circ\tilde{\iota}$ $\displaystyle=\delta\circ
F^{\mathbb{D}}(H(\vv{\mathbb{C}_{i}(f_{i})}))\circ\mathbb{D}(\kappa)\circ\delta\circ\tilde{\iota}$
$\displaystyle=\delta\circ
F^{\mathbb{D}}(H(\vv{\mathbb{C}_{i}(f_{i})}))\circ\iota$
$\displaystyle=\iota\circ\widehat{H}(\vv{F^{\mathbb{C}_{i}}(f_{i})})$
$\displaystyle=\mathbb{D}(\kappa)\circ\delta\circ\tilde{\iota}\circ\widehat{H}(\vv{F^{\mathbb{C}_{i}}(f_{i})})$

Therefore $\tilde{\iota}$ is natural of type
$\widehat{H}\circ\prod_{i}\mathbb{C}_{i}\Rightarrow F^{\mathbb{D}}\circ H$.

See 3.8

######  Proof A.8.

We prove the more general statement, when $\mathbb{C}$ is on a wide
subcategory $\mathcal{C}$ of $\mathcal{R}(\sigma)$. Let
$(\mathcal{E},\mathcal{M})$ be the (usual) proper factorisation system on
$\mathcal{R}(\sigma)$.

We first observe that
$(\mathcal{E}\cap\mathcal{C},\mathcal{M}\cap\mathcal{C})=(\mathcal{E}\cap\mathcal{C},\mathcal{M})$
is a factorisation system on $\mathcal{C}$. Let $f\in\mathcal{C}$ and $m\circ
e$ be is its factorisation in $\mathcal{R}(\sigma)$. Because $\mathcal{C}$
contains embeddings, $m\in\mathcal{C}$ and by the last assumption we also have
that $e\in\mathcal{C}$ as $f=m\circ e$ is in $\mathcal{C}$. The diagonality
condition of factorisation systems is immediate. Consequently,
$\mathsf{EM}(\mathcal{C})$ is equipped with the factorisation system
$(\overline{\mathcal{E}\cap\mathcal{C}},\overline{\mathcal{M}})$ by lemma 2.3.

Next, we observe that $\mathcal{C}$ is closed under equalisers and coproducts
in $\mathcal{R}(\sigma)$. For the former, let
$A\xrightarrow{e}B\overset{f,g}{\rightrightarrows}C$ be an equaliser diagram
in $\mathcal{R}(\sigma)$ with $f,g\in\mathcal{C}$. By lemma A.1.3,
$e\in\mathcal{C}$. Furthermore, let
$D\xrightarrow{h}B\overset{f,g}{\rightrightarrows}C$ be a commutative diagram
in $\mathcal{C}$ and $\overline{h}\colon D\to A$ the unique morphism such that
$e\circ\overline{h}=h$. Then, $\overline{h}\in\mathcal{C}$ by our last
assumption, and therefore, $e$ also an equaliser morphism of $f,g$ in
$\mathcal{C}$.

Observe that $\mathsf{EM}(\mathbb{C})$ is $\overline{\mathcal{M}}$-well-
powered because $\mathcal{C}$ is $\mathcal{M}$-well-powered because
$\mathcal{R}(\sigma)$ is as well. The rest follows from proposition A.9 below
and from the fact that $\mathcal{C}$ has coproducts and the forgetful functor
$\mathsf{EM}(\mathbb{C})\to\mathcal{C}$ reflects them.

The following is essentially an abstract form of Linton’s theorem [31],
phrased using factorization systems to fit our needs.

######  Proposition A.9.

If category $\mathcal{C}$:

  1. 1.

Has a proper factorization system $(\mathcal{E},\mathcal{M})$.

  2. 2.

Is $\mathcal{M}$-well-powered.

  3. 3.

Has coproducts.

Then $\mathcal{C}$ has equalizers.

######  Proof A.10.

Consider parallel pair:

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

As $\mathcal{C}$ is well-powered and has a factorization system, there is a
set $I$ of isomorphism classes 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 following commutes:

${\coprod_{i}M_{i}}$${A}$${A}$${B}$$\scriptstyle{[m_{i}]}$$\scriptstyle{[m_{i}]}$$\scriptstyle{g}$$\scriptstyle{f}$

As $\mathcal{C}$ has a factorization system, the morphism $[m_{i}]$ factors
as:

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

Assume $h:C\rightarrow A$ equalizes $f$ and $g$. There must exist $i$ such
that $h$ factors as $m_{i}\circ e^{\prime}$. 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
k\circ e^{\prime}$ is the unique fill in map, and the following is an
equalizer diagram:

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

###  A.4 Proofs for section 3.4

See 3.9

######  Proof A.11.

For $i=1,\dots,n$, the relation $A_{i}\leftrightarrow_{\mathbb{C}_{i}}B_{i}$
is witnessed by a span of open pathwise-embeddings

$F^{\mathbb{C}_{i}}(A_{i})\leftarrow R_{i}\rightarrow
F^{\mathbb{C}_{i}}(B_{i}),$

in $\mathsf{EM}(\mathbb{C}_{i})$. Then, by definition,

$\widehat{H}(\vv{F^{\mathbb{C}_{i}}(A_{i})})\leftarrow\widehat{H}(\vv{R_{i}})\rightarrow\widehat{H}(\vv{F^{\mathbb{C}_{i}}(B_{i})})$

is a span of open pathwise-embeddings. Furthermore, by proposition 3.7, we get
$F^{\mathbb{C}}(H(\vv{A_{i}}))\cong\widehat{H}(\vv{F^{\mathbb{C}_{i}}(A_{i})})$
and, similarly,
$F^{\mathbb{C}}(H(\vv{B_{i}}))\cong\widehat{H}(\vv{F^{\mathbb{C}_{i}}(B_{i})})$.

See 3.11

######  Proof A.12.

By proposition 2.5, $A\equiv_{\text{FO}_{k}}B$ is characterized by the
existence of a span of open pathwise embeddings

$F^{\mathbb{E}_{k}}(\mathfrak{t}^{I}A)\leftarrow R\rightarrow
F^{\mathbb{E}_{k}}(\mathfrak{t}^{I}B)$

Therefore, it suffices to check that given an FO-$\mathbb{E}_{k}$-smooth
operation $H\colon\prod_{i}R(\sigma_{i})\rightarrow R(\tau)$ and spans of open
pathwise embeddings:

$F^{\mathbb{E}_{k}}(\mathfrak{t}^{I}A_{i})\xleftarrow{f_{i}}R_{i}\xrightarrow{g_{i}}F^{\mathbb{E}_{k}}(\mathfrak{t}^{I}B_{i})\quad\text{in
}\mathsf{EM}(\mathbb{E}_{k})\text{ for $\mathbb{E}_{k}$ over
$\mathcal{R}(\sigma_{i})$}$

for all $1\leq i\leq n$, we can produce another span of open pathwise
embeddings:

$F^{\mathbb{E}_{k}}(\mathfrak{t}^{I}(H(\vv{A_{i}}))\leftarrow
R^{\prime}\rightarrow
F^{\mathbb{E}_{k}}(\mathfrak{t}^{I}(H(\vv{B_{i}}))\quad\text{in
}\mathsf{EM}(\mathbb{E}_{k})\text{ for $\mathbb{E}_{k}$ over
$\mathcal{R}(\tau)$}$ (5)

By assumption, $H$ is a FO-$\mathbb{E}_{k}$-smooth operation, so there exists
a natural transformation $\theta\colon
H\circ\mathfrak{t}^{I}\rightarrow\mathfrak{t}^{I}\circ H$ such that the
components of $F^{\mathbb{E}_{k}}(\theta)$ are open pathwise embeddings. This
allows us to compute (5) as the following composition in
$\mathsf{EM}(\mathbb{E}_{k})$ for $\mathbb{E}_{k}$ over $\mathcal{R}(\tau)$:

${\widehat{H}(\vv{R_{i}})}$${\widehat{H}(\vv{F^{\mathbb{E}_{k}}(\mathfrak{t}^{I}(A_{i}))}}$${\widehat{H}(\vv{F^{\mathbb{E}_{k}}(\mathfrak{t}^{I}(A_{i}))}}$${F^{\mathbb{E}_{k}}(H(\mathfrak{t}^{I}(\vv{A_{i}}))}$${F^{\mathbb{E}_{k}}(H(\mathfrak{t}^{I}(\vv{B_{i}}))}$${F^{\mathbb{E}_{k}}(\mathfrak{t}^{I}(H(\vv{A_{i}}))}$${F^{\mathbb{E}_{k}}(\mathfrak{t}^{I}(H(\vv{B_{i}}))}$$\scriptstyle{\widehat{H}(\vv{f_{i}})}$$\scriptstyle{\widehat{H}(\vv{g_{i}})}$$\scriptstyle{\cong}$$\scriptstyle{\cong}$$\scriptstyle{F^{\mathbb{E}_{k}}(\theta)}$$\scriptstyle{F^{\mathbb{E}_{k}}(\theta)}$
(6)

By proposition 3.9, $\widehat{H}(\vv{f_{i}})$ and $\widehat{H}(\vv{g_{i}})$
are open pathwise embeddings. By proposition 3.7, we get that
$\widehat{H}(\vv{F^{\mathbb{E}_{k}}(\mathfrak{t}^{I}(A_{i}))}\cong
F^{\mathbb{E}_{k}}(H(\mathfrak{t}^{I}(\vv{A_{i}}))$ and
$\widehat{H}(\vv{F^{\mathbb{E}_{k}}(\mathfrak{t}^{I}(B_{i}))}\cong
F^{\mathbb{E}_{k}}(H(\mathfrak{t}^{I}(\vv{B_{i}}))$. Moreover,
$F^{\mathbb{E}_{k}}(\theta_{\vv{A_{i}}})$ and
$F^{\mathbb{E}_{k}}(\theta_{\vv{B_{i}}})$ are open pathwise embedding. Since
the composition of open pathwise embeddings is an open pathwise embedding [3],
we conclude that the span in (6) is a span of open pathwise embeddings as
desired.

###  A.5 Proofs for section 3.5

######  Lemma A.13.

If $e_{1},\dots,e_{n}$ are embeddings in $\mathsf{EM}(\mathbb{C}_{1})$, …,
$\mathsf{EM}(\mathbb{C}_{n})$, respectively, then so is
$\widehat{H}(e_{1},\dots,e_{n})$.

######  Proof A.14.

Recall that $\widehat{H}(e_{1},\dots,e_{n})$ is defined by the universal
property of equalisers, while making the following diagram commute.

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

From $e_{1},\dots,e_{n}$ being embeddings we know that
$F^{\mathbb{D}}(\vv{U(e_{i})})$ is an embedding as well. Furthermore, by lemma
A.1(3), $\widehat{H}(\vv{e_{i}})$ is an equaliser and hence an embedding too.
Consequently, $\widehat{H}(e_{1},\dots,e_{n})$ is an embedding by lemma
A.1(2).

See 3.13

######  Proof A.15.

The first part of the statement is proved in lemma A.13 above. For the second
part, assume $e\colon\pi\rightarrowtail\widehat{H}(\vv{\alpha_{i}})$ is a path
embedding where, for $i=1,\dots,n$, $\alpha_{i}$ is the domain of
$f_{i}\colon\alpha_{i}\to\beta_{i}$. By (S2), $e$ decomposes as
$e_{0}\colon\pi\rightarrowtail\widehat{H}(\vv{\pi_{i}})$ followed by
$\widehat{H}(\vv{e_{i}})\colon\widehat{H}(\vv{\pi_{i}})\rightarrowtail\widehat{H}(\vv{\alpha_{i}})$.
Observe that, by lemma A.1(2), $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 lemma A.13,
$\widehat{H}(\vv{f_{i}\circ e_{i}})$ is also an embedding. We obtain that the
composite $\widehat{H}(\vv{f_{i}})\circ e=\widehat{H}(\vv{f_{i}\circ
e_{i}})\circ e_{0}$ is an embedding because embeddings are closed under
composition.

######  Lemma A.16.

Assume $f_{i}\colon\alpha_{i}\to\beta_{i}$ in $\mathsf{EM}(\mathbb{C}_{i})$
are pathwise-embeddings, for $i=1,\dots,n$. Then, for any path embeddings $e$
and $g$ making the diagram on the left below commute

${\pi}$${\widehat{H}(\vv{\alpha_{i}})}$${\widehat{H}(\vv{\beta_{i}})}$$\scriptstyle{e}$$\scriptstyle{g}$$\scriptstyle{\widehat{H}(\vv{f_{i}})}$
${\pi_{i}}$${\rho_{i}}$${\alpha_{i}}$${\beta_{i}}$$\scriptstyle{f^{\prime}_{i}}$$\scriptstyle{e_{i}}$$\scriptstyle{g_{i}}$$\scriptstyle{f_{i}}$

there exist morphisms $f^{\prime}_{i}\colon\pi_{i}\to\rho_{i}$, for
$i=1,\dots,n$, such that the diagram on the right above commutes. Here, the
$e_{i}$ and $g_{i}$ are the minimal embeddings such that $e$ and $g$ decompose
through $\widehat{H}(\vv{e_{i}})$ and $\widehat{H}(\vv{g_{i}})$, respectively.

######  Proof A.17.

Let $e_{0}\colon\pi\rightarrowtail\widehat{H}(\vv{\pi_{i}})$ be the embedding
such that $\widehat{H}(\vv{e_{i}})\circ e_{0}$ is the minimal decomposition of
$e$. Since $\widehat{H}(\vv{f_{i}})\circ e=\widehat{H}(\vv{f_{i}\circ
e_{i}})\circ e_{0}$ is another decomposition of $g$, there exists a morphism
$l_{i}\colon\rho_{i}\rightarrowtail\pi_{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}})\circ g_{0}$ where
$g_{0}\colon\pi\rightarrowtail\widehat{H}(\vv{\rho_{i}})$ is such that
$\widehat{H}(\vv{g_{i}})\circ g_{0}$ is the minimal decomposition of $g$.
Observe that $\widehat{H}(\vv{f_{i}\circ e_{i}})\circ
e_{0}=g=\widehat{H}(\vv{g_{i}})\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}})\circ g_{0}$. Therefore, since
$\widehat{H}(\vv{f_{i}\circ e_{i}})$ is an embedding (by lemma A.13), we
obtain $e_{0}=\widehat{H}(\vv{l_{i}})\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}}$,
there exists $f^{\prime}_{i}\colon\pi_{i}\to\rho_{i}$, for $i=1,\dots,n$, such
that $e_{i}=e_{i}\circ l_{i}\circ f^{\prime}_{i}$. Therefore, $f_{i}\circ
e_{i}=f_{i}\circ e_{i}\circ l_{i}\circ f^{\prime}_{i}=g_{i}\circ
f^{\prime}_{i}$, for $i=1,\dots,n$.

See 3.14

######  Proof A.18.

Given open pathwise-embeddings $f_{i}\colon\alpha_{i}\to\beta_{i}$ in
$\mathsf{EM}(\mathbb{C}_{i})$, for $i=1,\dots,n$, we need to check that
$\widehat{H}(\vv{f_{i}})$ is open as we already know by proposition 3.13 that
it is a pathwise-embedding. Assume that the outer square of path embeddings in
the diagram below commutes, with the left-most and right-most morphisms being
the minimal decompositions of some path embeddings
$\pi\rightarrowtail\widehat{H}(\vv{\alpha_{i}})$ and
$\rho\rightarrowtail\widehat{H}(\vv{\beta_{i}})$, respectively, by (S2).

${\pi}$${\rho}$${\widehat{H}(\vv{\pi_{i}})}$${\widehat{H}(\vv{\pi^{\prime}_{i}})}$${\widehat{H}(\vv{\rho_{i}})}$${\widehat{H}(\vv{\alpha_{i}})}$${\widehat{H}(\vv{\beta_{i}})}$$\scriptstyle{h}$$\scriptstyle{e_{0}}$$\scriptstyle{e^{\prime}_{0}}$$\scriptstyle{g_{0}}$$\scriptstyle{\widehat{H}(\vv{e_{i}})}$$\scriptstyle{\widehat{H}(\vv{f^{\prime}_{i}})}$$\scriptstyle{\widehat{H}(\vv{e^{\prime}_{i}})}$$\scriptstyle{\widehat{H}(\vv{h_{i}})}$$\scriptstyle{\widehat{H}(\vv{g_{i}})}$$\scriptstyle{\widehat{H}(\vv{f_{i}})}$

The path embedding $\widehat{H}(\vv{f_{i}\circ e_{i}})\circ e_{0}$ has a
minimal decomposition via
$\widehat{H}(\vv{e^{\prime}_{i}})\colon\widehat{H}(\vv{\pi^{\prime}_{i}})\rightarrowtail\widehat{H}(\vv{\beta_{i}})$
as shown above. Then, by minimality of this decomposition and by lemma A.16,
for $i=1,\dots,n$, there exist
$f^{\prime}_{i}\colon\pi_{i}\to\pi^{\prime}_{i}$ and
$h_{i}\colon\pi^{\prime}_{i}\to\rho_{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\rho_{i}\to\alpha_{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}})$ is a mono, the top rectangle commute as well.
Consequently, $\widehat{H}(\vv{d_{i}})\circ
g_{0}\colon\rho\to\widehat{H}(\vv{\alpha_{i}})$ is the required diagonal
filler of the outer square.

###  A.6 Multilinear maps

We introduce a class of maps between coalgebras of use when checking (S1) and
(S2) axioms, and establish a connection to functors lifted to Eilenberg-Moore
categories.

For a Kleisli-law $\kappa$, $\mathbb{D}$-coalgebra $(A,\alpha)$, and
$\mathbb{C}_{i}$-coalgebras $(B_{i},\beta_{i})$, we shall say that a
$\mathcal{D}$-morphism $h:A\rightarrow H(\vv{B_{i}})$ is a _multilinear map_
$\alpha\to[\vv{\beta_{i}}]$ if 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{h}$$\scriptstyle{\alpha}$$\scriptstyle{H(\vv{\beta_{i}})}$$\scriptstyle{\mathbb{D}(h)}$$\scriptstyle{\kappa}$

The following result appears in various guises in the literature for the dual
setting of monads [24, 40]. We provide a full proof as similar results often
appear restricted to the binary setting, and in relation to commutative
monads. Our proof clarifies that the additional assumptions of a commutative
(co)monad serve no role in the properties we require. We state the formulation
suitable subsequent developments.

######  Proposition A.19.

For a Kleisli-law $\kappa$, let $\iota$ be the universal equalizer morphism
appearing in the construction of $\widehat{H}$. The natural transformation:

$\mathrm{u}_{\vv{\alpha_{i}}}:=\widehat{H}(\vv{\alpha_{i}})\xrightarrow{\enspace\iota\enspace}\mathbb{D}(H(\vv{A_{i}}))\xrightarrow{\enspace\varepsilon\enspace}H(\vv{A_{i}})$

is a _universal multilinear map_
$\widehat{H}(\vv{\alpha_{i}})\to[\vv{\alpha_{i}}]$. That is, any multilinear
map $f\colon\beta\rightarrow[\vv{\alpha_{i}}]$ factors through $u$ via a
unique $\mathbb{D}$-coalgebra morphism
$\widehat{f}\colon\beta\to\widehat{H}(\vv{\alpha_{i}})$.

######  Proof A.20.

We first establish $\varepsilon\circ\iota$ is multilinear. Let $\omega$ be the
structure map of $\widehat{H}(\vv{\alpha_{i}})$

$\displaystyle\kappa\circ\mathbb{D}(\varepsilon)\circ\mathbb{D}(\iota)\circ\omega$
$\displaystyle=\kappa\circ\mathbb{D}(\varepsilon)\circ\delta\circ\iota$
$\displaystyle=\kappa\circ\varepsilon\circ\delta\circ\iota$
$\displaystyle=\varepsilon\circ\mathbb{D}(\kappa)\circ\delta\circ\iota$
$\displaystyle=\varepsilon\circ\mathbb{D}H(\vv{\alpha_{i}})\circ\iota$
$\displaystyle=H(\vv{\alpha_{i}})\circ\varepsilon\circ\iota$

Let $(B,\beta)$ be a coalgebra, and $f:\beta\rightarrow[\vv{\alpha_{i}}]$ a
multilinear map. Then $\mathbb{D}(f)\circ\beta$ is a coalgebra morphism by:

$\mathbb{D}^{2}(f)\circ\mathbb{D}(\beta)\circ\beta=\mathbb{D}^{2}(f)\circ\delta\circ\beta=\delta\circ\mathbb{D}(f)\circ\beta.$

Further, it equalizes $F^{\mathbb{D}}(H(\vv{\alpha_{i}}))$ and
$F^{\mathbb{D}}(\kappa)\circ\delta$, as:

$\displaystyle\mathbb{D}(H(\vv{\alpha_{i}}))\circ\mathbb{D}(f)\circ\beta$
$\displaystyle=\mathbb{D}(\kappa)\circ\mathbb{D}^{2}(f)\circ\mathbb{D}(\beta)\circ\beta$
$\displaystyle=\mathbb{D}(\kappa)\circ\mathbb{D}^{2}(f)\circ\delta\circ\beta$
$\displaystyle=\mathbb{D}(\kappa)\circ\delta\circ\mathbb{D}(f)\circ\beta$

Let $\tilde{f}$ be the unique coalgebra morphism given by the equalizer
universal property by $\mathbb{D}(f)\circ\beta$. Now if
$g:\beta\rightarrow\widehat{H}(\vv{\alpha_{i}})$, then
$\varepsilon\circ\iota\circ g$ is a multilinear map as:

$\displaystyle H(\vv{\alpha_{i}})\circ\varepsilon\circ\iota\circ g$
$\displaystyle=\kappa\circ\mathbb{D}(\varepsilon\circ\iota)\circ\omega\circ g$
$\displaystyle=\kappa\circ\mathbb{D}(\varepsilon\circ\iota)\circ\mathbb{D}(g)\circ\beta$
$\displaystyle=\kappa\circ\mathbb{D}(\varepsilon\circ\iota\circ g)\circ\beta$

Then combining these two operations in one direction:

$\varepsilon\circ\iota\circ\tilde{f}=\varepsilon\circ\mathbb{D}(f)\circ\beta=f\circ\varepsilon\circ\beta=f$

In the other direction, we claim $\widetilde{\varepsilon\circ\iota\circ f}=f$.
As:

$\displaystyle\mathbb{D}(\varepsilon\circ\iota\circ f)\circ\beta$
$\displaystyle=\mathbb{D}(\varepsilon)\circ\mathbb{D}(\iota)\circ\mathbb{D}(f)\circ\beta$
$\displaystyle=\mathbb{D}(\varepsilon)\circ\mathbb{D}(\iota)\circ\omega\circ
f$ $\displaystyle=\mathbb{D}(\varepsilon)\circ\delta\circ\iota\circ f$
$\displaystyle=\iota\circ f$

The equalizer universal property then establishes the claimed equality. The
two mappings then exhibit the required bijection.

######  Remark A.21.

Our multilinear map terminology is connected to an instance of the dual
construction in monad theory. See for example [24, 40], where the
corresponding binary notion (called “bilinearity”) is phrased in terms of
Kleisli maps.

######  Lemma A.22.

Given a multilinear map $f\colon\alpha\to[\vv{\beta_{i}}]$ which decomposes as
$f_{0}\colon A\to H(\vv{A_{i}})$ followed by $H(\vv{e_{i}})$, for some
coalgebra embeddings $e_{i}\colon\alpha_{i}\rightarrowtail\beta_{i}$, for
$1\leq i\leq n$, the morphism $f_{0}$ is a multilinear map
$\alpha\to[\vv{\alpha_{i}}]$.

######  Proof A.23.

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

By multilinearity of $f$ 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 multilinearity of $f_{0}$.

Next, we translate axiom (S2) in terms of multilinear maps, which makes it
easier to work with.

######  Lemma A.24.

Assuming (S1) holds, then (S2) is equivalent to

  1. (S2’)

Any multilinear map $f\colon\pi\to[\vv{\alpha_{i}}]$, such that $\widehat{f}$
is a path embedding, has a minimal decomposition through $H(\vv{e_{i}})\colon
H(\vv{\pi_{i}})\to H(\vv{\alpha_{i}})$, for some path embeddings
$e_{i}\colon\pi_{i}\rightarrowtail\alpha_{i}$, with $1\leq i\leq n$.

######  Proof A.25.

Let $e\colon\pi\rightarrowtail\widehat{H}(\vv{\alpha_{i}})$ be a path
embedding and let $f\colon\pi\to[\vv{\alpha_{i}}]$ be the corresponding
multilinear map (i.e. $f=\mathrm{u}\circ e$).

Assume $f$ has a minimal decomposition $H(\vv{e_{i}})\circ f_{0}$ for some
$f_{0}\colon P\to H(\vv{\pi_{i}})$ and path embeddings
$e_{i}\colon\pi_{i}\rightarrowtail\alpha_{i}$, with $1\leq i\leq n$. It
follows that $f_{0}$ is a multilinear map $\pi\to[\vv{\pi_{i}}]$ (see lemma
A.22). Therefore, by proposition A.19, there exists a coalgebra morphism
$e_{0}\colon\pi\to\widehat{H}(\vv{\pi_{i}})$ such that $\mathrm{u}\circ
e_{0}=f_{0}$. Then, by naturality of $\mathrm{u}$, $f=H(\vv{e_{i}})\circ
f_{0}=H(\vv{e_{i}})\circ\mathrm{u}\circ
e_{0}=\mathrm{u}\circ\widehat{H}(\vv{e_{i}})\circ e_{0}$ which, by
universality of $\mathrm{u}$, yields that $\widehat{H}(\vv{e_{i}})\circ
e_{0}=e$ (and whereby $e_{0}$ is an embedding by lemma A.1). Further, if $e$
decomposes as $g_{0}\colon\pi\to\widehat{H}(\vv{\rho_{i}})$ followed by
$\widehat{H}(\vv{g_{i}})$, with embeddings
$g_{i}\colon\rho_{i}\rightarrowtail\alpha_{i}$, for $1\leq i\leq n$, then by
naturality of $\mathrm{u}$, $f$ decomposes as
$H(\vv{g_{i}})\circ\mathrm{u}\circ g_{0}$. Then, by minimality of
$H(\vv{e_{i}})\circ f_{0}$, there exists
$g^{\prime}_{i}\colon\pi_{i}\to\rho_{i}$ such that $e_{i}=g_{i}\circ
g^{\prime}_{i}$, for $1\leq i\leq n$.

Conversely, assuming $e$ has a minimal decomposition
$\widehat{H}(\vv{e_{i}})\circ e_{0}$ for some
$e_{0}\colon\pi\rightarrowtail\widehat{H}(\vv{\pi_{i}})$ and path embeddings
$e_{i}\colon\pi_{i}\rightarrowtail\alpha_{i}$, with $1\leq i\leq n$. By
naturality of $\mathrm{u}$, we obtain a decomposition of $f$ as

$f=\mathrm{u}\circ\widehat{H}(\vv{e_{i}})\circ e_{0}=H(\vv{e_{i}})\circ f_{0}$

where $f_{0}=\mathrm{u}\circ e_{0}\colon P\to H(\vv{P_{i}})$. If there is
another decomposition of $f$ as $g_{0}\circ H(\vv{Q_{i}})$ followed by
$H(\vv{g_{i}})$, for embeddings $g_{i}\colon\rho_{i}\to\alpha_{i}$ (where
$1\leq i\leq n$), then by lemma A.22, $g_{0}$ is multilinear and by
proposition A.19 there exists $h\colon\pi\to\widehat{H}(\vv{\rho_{i}})$ such
that $g_{0}=\mathrm{u}\circ h$. As before we see that
$e=\widehat{H}(\vv{g_{i}})\circ h$, yielding
$g^{\prime}_{i}\colon\pi_{i}\to\rho_{i}$ such that $e_{i}=g_{i}\circ
g^{\prime}_{i}$, for $1\leq i\leq n$

###  A.7 Proofs for section 3.6

See 3.15

######  Proof A.26.

Axioms (F1) and (F2) follow automatically because the underlying function of
$\kappa$ is the identity function.

Next, we check that $\kappa$ satisfies the smoothness axioms (S1) and (S2’)
from lemma A.24. For (S1), we see that ${\operatorname{join}_{\bar{i}}^{R}}$
preserves embeddings $e:A\rightarrow B$, as it follows that
$R^{{\operatorname{join}_{\bar{i}}^{R}}(A)}(a_{1},\dots,a_{r})$ if and only if
$R^{{\operatorname{join}_{\bar{i}}^{R}}(B)}({\operatorname{join}_{\bar{i}}^{R}}(e)(a_{1}),\dots,{\operatorname{join}_{\bar{i}}^{R}}(e)(a_{r}))$
from $R^{A}(a_{1},\dots,a_{r})\Leftrightarrow R^{B}(e(a_{1}),\dots,e(a_{r}))$
and also $P^{A}_{i_{z}}(a_{z})\Leftrightarrow P^{B}_{i_{z}}(e(a_{z}))$ for all
$z\leq r$.

For (S2’), suppose $\pi\colon P\to\mathbb{E}_{k}P$ is a path
$r_{1}\sqsubset_{\pi}r_{2}\sqsubset_{\pi}\dots\sqsubset_{\pi}r_{n}$ and
$f\colon\pi\to[\alpha]$ is a multilinear map. Because $\kappa$ is just the
identity function, multilinearity of $f$ translates as

$\displaystyle\alpha(f(r_{i}))=\kappa([f(r_{1}),\dots,f(r_{n})])=[f(r_{1}),\dots,f(r_{n})],$
(7)

for every $i=1,\dots,n$. In other words, $f(r_{1}),\dots,f(r_{n})$ is a path
in $\sqsubseteq_{\alpha}$ (recall remark 2.2). Therefore, the inclusion
$j\colon P^{\prime}\to A$ of the induced substructure on
$\\{f(r_{1}),\dots,f(r_{n})\\}$ into $A$, is a path embedding
$\pi^{\prime}\to\alpha$ where $\pi^{\prime}$ is the restriction of $\alpha$ to
$P$. Further, the mapping $f$ factors as
${\operatorname{join}_{\bar{i}}^{R}}(j)\circ f_{0}$ where $f_{0}$ is a
homomorphism because $f$ is and $j$ is an embedding. Minimality is immediate
from the fact that the image of $P$ under $f$ is onto $P^{\prime}$.

###  A.8 Proofs for section 3.7

We first justify that $\mathbb{E}_{k}^{\text{nc}}$ is a comonad. Viewing
$\mathbb{E}_{k}^{\text{nc}}(A)$ as an induced substructure of
$\mathbb{E}_{k}(A)$, we see that the restriction of
$\varepsilon\colon\mathbb{E}_{k}(A)\to A$ to $\mathbb{E}_{k}^{\text{nc}}(A)$
is a morphism in $\mathcal{R}_{\text{nc}}(\sigma)$. Further, defining
coextensions $(-)^{*}$ as for $\mathbb{E}_{k}$ we see that, for any morphism
$f\colon\mathbb{E}_{k}^{\text{nc}}(A)\to B$ in
$\mathcal{R}_{\text{nc}}(\sigma)$, the coextension $f^{*}$ is also a morphism
in $\mathcal{R}_{\text{nc}}(\sigma)$. The axioms (1) hold for
$(\mathbb{E}_{k}^{\text{nc}},\varepsilon,(-)^{*})$ because they already hold
for $\mathbb{E}_{k}$.

Observe that $\mathsf{EM}(\mathbb{E}_{k}^{\text{nc}})$ has equalisers of
reflexive pairs. This follows from lemma 3.8, it is easy to see that its
assumptions are satisfied for $\mathbb{C}=\mathbb{E}_{k}^{\text{nc}}$ and
$\mathcal{C}=\mathcal{R}_{\text{nc}}(\sigma_{3})$. Therefore, if $\kappa$ is a
Kleisli law, the functor $\mathbin{\parallel}$ lifts to a functor
$\mathbin{\widehat{\mathbin{\parallel}}}\colon\mathsf{EM}(\mathbb{E}_{k}^{\text{nc}})\times\mathsf{EM}(\mathbb{E}_{k}^{\text{nc}})\to\mathsf{EM}(\mathbb{E}_{k}^{\text{nc}})$.
The following shows that this is the case and that the lifted functor
preserves open pathwise embeddings.

See 3.16

######  Proof A.27.

We check that $\kappa$ is a well-defined natural transformation. First, to see
that each component of $\kappa$ is a well-defined $\sigma$-structure
homomorphism, assume that $(x_{1},\dots,x_{n})\in
R^{\mathbb{E}_{k}^{\text{nc}}(A\mathbin{\parallel}B)}$ holds for some $R$ in
$\sigma$ and $x_{1},\dots,x_{n}$ in
$\mathbb{E}_{k}^{\text{nc}}(A\mathbin{\parallel}B)$. By definition of
$\mathbb{E}_{k}^{\text{nc}}(A\mathbin{\parallel}B)$,
$\varepsilon(x_{i})=\iota(y_{i})$, for some $(y_{1},\dots,y_{n})\in R^{A}$ or
$(y_{1},\dots,y_{n})\in R^{B}$. W.l.o.g. assume that the former is the case.
By definition of $\kappa$, each $\kappa(x_{i})$ is either
$\mathtt{ex}_{1}(x_{i})\in\mathbb{E}_{k}^{\text{nc}}(A)$ or a constant
$c_{i}$. Therefore, $\kappa(x_{i})=\mathfrak{i}(z_{i})$ for some
$z_{i}\in\mathbb{E}_{k}^{\text{nc}}(A)$ and, moreover,
$\varepsilon(z_{i})=y_{i}$, for $1\leq i\leq n$. Finally, we see that non-
constant $x_{i}$ are comparable in the prefix order in
$\mathbb{E}_{k}^{\text{nc}}(A\mathbin{\parallel}B)$ and this property is
preserved by $\mathtt{ex}_{1}(-)$. Therefore,
$(\kappa(x_{1}),\dots,\kappa(x_{n}))\in
R^{\mathbb{E}_{k}^{\text{nc}}(A)\mathbin{\parallel}\mathbb{E}_{k}^{\text{nc}}(B)}$.

Naturality of $\kappa$ is immediate from the fact that morphisms in
$\mathcal{R}_{\text{nc}}(\sigma_{1})$ and
$\mathcal{R}_{\text{nc}}(\sigma_{1})$ send constant elements to constant
elements and non-constant elements to non-constant elements.

Next, we check the smoothness axioms. Observe that (F1) and (S1) hold by
definitions. Further, (F2) follows by an easy case analysis. For (S2’) from
lemma A.24, let $f\colon\pi\to[\alpha,\beta]$ be a multilinear map from a path
$\pi$ in $\mathsf{EM}(\mathbb{E}_{k}^{\text{nc}})$ and let
$r_{1}\sqsubset_{\pi}r_{2}\sqsubset_{\pi}\dots\sqsubset_{\pi}r_{n}$ be the
chain of non-constant elements in $\pi$. Multilinearity of $f$ implies

$\kappa([f(r_{1}),\dots,f(r_{i})])=(\alpha\mathbin{\parallel}\beta)(f(r_{i})),\quad\text{for
$i=1,\dots,n$.}$ (8)

In fact, this expresses precisely that if $f(r_{i})\in\mathfrak{i}(A)$ then
$\mathtt{ex}_{1}([f(r_{1}),\dots,f(r_{i})])$ is a path in
$\sqsubseteq_{\alpha}$ and, dually, $f(r_{i})\in\mathfrak{i}(B)$ implies that
$\mathtt{ex}_{2}([f(r_{1}),\dots,f(r_{i})])$ is a path in
$\sqsubseteq_{\beta}$. From this it immediately follows that $f$ factors
through the embedding

$e_{1}\mathbin{\parallel}e_{2}\colon P\mathbin{\parallel}Q\rightarrowtail
A\mathbin{\parallel}B$

where $e_{1}$ and $e_{2}$ are the path embeddings corresponding to the paths
$\mathtt{ex}_{1}([f(r_{1}),\dots,f(r_{n})])$ and
$\mathtt{ex}_{2}([f(r_{1}),\dots,f(r_{n})])$, respectively. Minimality of $P$
and $Q$ is immediate.

We remark that $\kappa$ is smooth by the above discussion, theorem 3.14 and
lemma A.24.

######  Lemma A.28.

For $\sigma$-structures $A,B$,
$\mathfrak{t}^{I}(A)\leftrightarrow_{\mathbb{E}_{k}^{\text{nc}}}\mathfrak{t}^{I}(B)$
iff $A\equiv_{\text{FO}_{k}}B$

######  Proof A.29.

The proof of proposition 2.5 can be adapted to this statement. Moreover, we
prove a general version for multi-sorted first order logic in proposition 4.2.

See 3.17

######  Proof A.30.

We need to show that $\mathbin{\parallel}$, viewed as an operation
$\mathcal{R}_{0}(\sigma_{1})\times\mathcal{R}_{0}(\sigma_{2})\to\mathcal{R}_{0}(\sigma_{3})$
is FO-$\mathbb{E}_{k}^{\text{nc}}$-smooth. We defined
$\mathbb{E}_{k}^{\text{nc}}$ as a comonad on
$\mathcal{R}_{\text{nc}}(\sigma)$, for any $\sigma$, i.e. including
$\sigma=\sigma^{I}_{1},\sigma^{I}_{2}$, or $\sigma^{I}_{3}$. Also, the usual
$\mathfrak{t}^{I}\colon\mathcal{R}_{0}(\sigma)\to\mathcal{R}(\sigma^{I})$
factors as $\mathcal{R}_{0}(\sigma)\to\mathcal{R}_{\text{nc}}(\sigma^{I})$
followed by the inclusion
$\mathcal{R}_{\text{nc}}(\sigma^{I})\subseteq\mathcal{R}(\sigma^{I})$. We need
two natural transformations $\kappa$ and $\theta$ shown below.

${\mathcal{R}_{0}(\sigma_{1})\times\mathcal{R}_{0}(\sigma_{1})}$${\mathcal{R}_{\text{nc}}(\sigma^{I}_{1})\times\mathcal{R}_{\text{nc}}(\sigma^{I}_{2})}$${\mathcal{R}_{\text{nc}}(\sigma^{I}_{1})\times\mathcal{R}_{\text{nc}}(\sigma^{I}_{2})}$${\mathcal{R}_{0}(\sigma_{3})}$${\mathcal{R}_{\text{nc}}(\sigma^{I}_{3})}$${\mathcal{R}_{\text{nc}}(\sigma^{I}_{3})}$$\scriptstyle{\mathfrak{t}_{1}\times\mathfrak{t}_{2}}$$\scriptstyle{\mathbin{\parallel}}$$\scriptstyle{\mathbin{\parallel}^{I}}$$\scriptstyle{\theta}$$\scriptstyle{\mathbb{E}_{k}^{\text{nc}}\times\mathbb{E}_{k}^{\text{nc}}}$$\scriptstyle{\mathbin{\parallel}^{I}}$$\scriptstyle{\kappa}$$\scriptstyle{\mathfrak{t}_{3}}$$\scriptstyle{\mathbb{E}_{k}^{\text{nc}}}$
(9)

Where $\mathbin{\parallel}^{I}$ is the $I$ version of $\mathbin{\parallel}$.
It is easy to observe that
$\mathfrak{t}^{I}(A)\mathbin{\mathbin{\parallel}^{I}}\mathfrak{t}^{I}(B)\cong\mathfrak{t}^{I}(A\mathbin{\parallel}B)$
and so $\theta$ is just this isomorphism, componentwise. Further, the
$I$-version of $\kappa$ is smooth by lemma 3.16. Therefore, by proposition
3.9, if
$\mathfrak{t}^{I}(A_{i})\leftrightarrow_{\mathbb{E}_{k}^{\text{nc}}}\mathfrak{t}^{I}(B_{i})$,
for $i=1,2$, then also

$\mathfrak{t}^{I}(A_{1}\mathbin{\parallel}A_{2})\cong\mathfrak{t}^{I}(A_{1})\mathbin{\parallel}^{I}\mathfrak{t}^{I}(A_{2})\leftrightarrow_{\mathbb{E}_{k}^{\text{nc}}}\mathfrak{t}^{I}(B_{1})\mathbin{\parallel}^{I}\mathfrak{t}^{I}(B_{2})\cong\mathfrak{t}^{I}(B_{1}\mathbin{\parallel}B_{2}).$

This proves the statement as
$\mathfrak{t}^{I}(A)\leftrightarrow_{\mathbb{E}_{k}^{\text{nc}}}\mathfrak{t}^{I}(B)$
is equivalent to $A\equiv_{\text{FO}_{k}}B$, by lemma A.28.

###  A.9 Proofs for section 4.1

See 4.1

######  Proof A.31.

For $A\in\mathcal{R}^{S}(\sigma)$, the morphism
$\varepsilon_{A}\colon\mathbb{E}_{k}A\rightarrow A$ is defined component-wise:

$(\varepsilon_{A})_{s}(c^{\mathbb{E}_{k}A})=c^{A}\text{ for
}c\in\mathbf{cs}(\sigma,s)\quad(\varepsilon_{A})_{s}([a_{1}{:}s_{1},\dots,a_{n}{:}s_{n}])=a_{n}\text{
with }s=s_{n}$

For a $\sigma$-morphism $f\colon\mathbb{E}_{k}A\rightarrow B$, the morphism
$f^{*}\colon\mathbb{E}_{k}A\rightarrow\mathbb{E}_{k}B$ is defined component-
wise:

$(f^{*})_{s}(c^{\mathbb{E}_{k}A})=c^{\mathbb{E}_{k}B}\text{ for
}c\in\mathbf{cs}(\sigma,s)\quad(f^{*})_{s}([a_{1}{:}s_{1},\dots,a_{n}{:}s_{n}])=[b_{1}{:}s_{1},\dots,b_{n}{:}s_{n}]$

where $b_{i}=f_{s_{i}}([a_{1}{:}s_{1},\dots,a_{i}{:}s_{i}])]$ for $1\leq i\leq
n$ and $s=s_{n}$. Verifying that $\varepsilon_{A}$ and $f^{*}$ are
$\sigma$-morphisms is straightforward application of the definitions.
Moreover, verifying the axioms (1) is also routine.

In order to show $\mathbb{E}_{k}^{\text{nc}}$ is comonad, we note that for all
$A\in\mathcal{R}^{S}_{\text{nc}}(\sigma)$, $\varepsilon_{A}$ is a morphism in
$\mathcal{R}^{S}_{\text{nc}}(\sigma)$ and that $f^{*}$ is a morphism in
$\mathcal{R}^{S}_{\text{nc}}(\sigma)$ whenever $f$ is a morphism in
$\mathcal{R}^{S}_{\text{nc}}(\sigma)$.

See 4.2

We prove that bisimulation for the $\mathfrak{t}^{J}$-lifting $S$-sorted
$\mathbb{E}_{k}$ captures equivalence in $\text{FO}_{k}(S,J)$, by first
introducing the corresponding Ehrenfeucht–Fraïssé game