# Composing Codensity Bisimulations

Mayuko Kori  National Institute of Informatics  The Graduate University for
Advanced Studies, SOKENDAI  Kazuki Watanabe  National Institute of Informatics
The Graduate University for Advanced Studies, SOKENDAI
Jurriaan Rot  Radboud University  Shin-ya Katsumata  Kyoto Sangyo University

###### Abstract

Proving compositionality of behavioral equivalence on state-based systems with
respect to algebraic operations is a classical and widely studied problem. We
study a categorical formulation of this problem, where operations on state-
based systems modeled as coalgebras can be elegantly captured through
distributive laws between functors. To prove compositionality, it then
suffices to show that this distributive law lifts from sets to relations,
giving an explanation of how behavioral equivalence on smaller systems can be
combined to obtain behavioral equivalence on the composed system.

In this paper, we refine this approach by focusing on so-called codensity
lifting of functors, which gives a very generic presentation of various
notions of (bi)similarity as well as quantitative notions such as behavioral
metrics on probabilistic systems. The key idea is to use codensity liftings
both at the level of algebras and coalgebras, using a new generalization of
the codensity lifting. The problem of lifting distributive laws then reduces
to the abstract problem of constructing distributive laws between codensity
liftings, for which we propose a simplified sufficient condition. Our
sufficient condition instantiates to concrete proof methods for
compositionality of algebraic operations on various types of state-based
systems. We instantiate our results to prove compositionality of qualitative
and quantitative properties of deterministic automata. We also explore the
limits of our approach by including an example of probabilistic systems, where
it is unclear whether the sufficient condition holds, and instead we use our
setting to give a direct proof of compositionality.

In addition, we propose a compositional variant of Komorida et al.’s codensity
games for bisimilarities. A novel feature of this variant is that it can also
compose game invariants, which are subsets of winning positions. Under our
sufficient condition of the liftability of distributive laws, composed games
give an alternative proof of the preservation of bisimilarities under the
composition.

##  1 Introduction

Bisimilarity and its many variants are fundamental notions of behavioral
equivalence on state-based systems. A classical question is whether a given
notion of equivalence is _compositional_ w.r.t. algebraic operations on these
systems, such as parallel composition of concurrent systems, product
constructions on automata, or other language constructs. The problem can
become particularly challenging when moving from bisimilarity to quantitative
notions such as behavioral metrics on probabilistic systems, where it is
already non-trivial to even define what the right notion of compositionality
is (see, e.g. [26, 12]).

To formulate and address the problem of compositionality of algebraic
operations on state-based systems at a high level of generality, a natural
formalism is that of _coalgebra_ [20], which is parametric in the type of
system, as modeled by a “behavior” endofunctor $F$. A key idea, originating in
the seminal work of Turi and Plotkin [31], is that composition operations and
in fact whole languages specifying state-based systems arise as _distributive
laws_ between $F$ and a functor (or monad) $T$ which models the syntax of a
bigger programming language. In fact, Turi and Plotkin’s _abstract GSOS laws_
are forms of such distributive laws which guarantee compositionality of strong
bisimilarity, generalizing the analogous result for specifications in the
_GSOS format_ for labeled transition systems [4]. Distributive laws here
precisely capture algebra-coalgebra interaction needed for compositionality.

The results of Turi and Plotkin specifically apply to strong bisimilarity, and
not directly to other notions such as similarity or behavioral metrics. To
prove compositionality in these cases, the key observation is that the task is
to define the composition operation at hand not only on state-based systems
but also on relations (or, e.g., pseudometrics). This idea has been formalized
in the theory of coalgebras by requiring a _lifting_ of the distributive law
that models the composition operator to a category of relations. The lifting
of the behavior functor $F$ then specifies the notion of bisimilarity at hand,
and the lifting of the syntax functor $T$ specifies the way that relations on
components can be combined into bisimulations on the composite system. It has
been shown in [6] at a high level of generality that the existence of such
liftings, referred to in this paper as _liftability_ , ensures
compositionality. The generality there is offered by the use of liftings of
the behavior functor in fibrations which goes back to [17], and which allows
us to study not only relations but also, for instance, coinductively defined
metrics or unary predicates (e.g., [23, 29, 16, 5]). But the main challenge
here is to _prove liftability_ ; this is what we address in the current paper
(Question 3.11.2).

We focus on the _codensity lifting_ of behavior functors [29], which allows to
model a wide variety of coinductive relations and predicates including
(bi)similarity but also, for instance, behavioral metrics; these are commonly
referred to as _codensity bisimilarity_. In fact, the codensity lifting
directly generalizes the celebrated Kantorovich distance between probability
distributions used to define, for instance, metrics between probabilistic
systems [8]. The codensity lifting is parametric in a collection of modal
operators, which makes it on the one hand very flexible and on the other hand
much more structured than arbitrary liftings. Moreover, the codensity lifting
allows to characterize _codensity games_ [23], a generalization of classical
bisimilarity games [30, 9] from transition systems to coalgebras, and from
strong bisimilarity to a wide variety of coinductively defined relations,
metrics and even topologies.

In this paper we study _compositionality of codensity bisimulations_ with
respect to composition operators on the underlying state-based systems,
modeled as coalgebras. We model these composition operators as distributive
laws between an $n$-ary product functor and the behavior functor $F$, referred
to as _one-step composition operators_. We mainly tackle two problems
(Question 3.11) in this paper: 1) How do we lift the $n$-ary product functor
in order to capture non-trivial combination of relations, pseudometrics etc?
2) When is a one-step composition operator liftable?

A key idea for the first problem is to use codensity liftings not only to lift
the behavior functor $F$ and get our desired notion of equivalence, but to use
another codensity lifting of the product functor, to explain syntactically how
relations (or pseudometrics, etc) should be combined from components to the
composite system. This combination can be a simple product between relations,
but in many cases, such as for behavioral metrics, it needs to be more
sophisticated; the flexibility offered by the codensity lifting helps to
define the appropriate constructions on relations.

The second problem about liftability then becomes that of proving the
existence of a _distributive law between codensity liftings_. To this end, we
exhibit a sufficient condition that ensure the existence of this distributive
laws, defined in terms of two properties: 1) commutation between the
underlying modalities that define codensity liftings, and 2) an
_approximation_ property, which resembles the one used to prove expressiveness
of modal logics in [24]. Underlying our approach is a combination of a new
generalization of the codensity lifting beyond endofunctors, to allow to lift
product functors, and the adjunction-based decomposition of codensity liftings
proposed in [3]. The adjunction-based approach precisely allows us to arrive
at our sufficient condition.

We instantiate our approach to pseudometrics on deterministic automata. We
also revisit the compositionality of parallel composition w.r.t. behavioral
metrics studied in [12]. In this case it is not clear whether our sufficient
condition holds; but the framework nevertheless helps to prove liftability and
thereby compositionality.

We further study a compositional variant of codensity games. A key observation
is that our _composite codensity games_ consist of positions that are tuples
of positions of codensity games for component systems. This design of the
composite game directly leads to the compositionality of game invariants,
which characterize winning positions. Assuming our sufficient condition for
the liftability of distributive laws, we present an alternative proof of the
preservation of bisimilarities along compositions (the inequality in Corollary
3.10).

In summary, the contributions of this paper are

  * •

a generalization of the codensity lifting beyond endofunctors (Section 4),
which can be used in a special case to lift products in various ways (Section
5);

  * •

a sufficient condition for proving the existence of a distributive law between
codensity liftings (Section 6), with several detailed examples (Section 7);

  * •

a composition of codensity games, which also composes game invariants, and an
alternative proof of the preservation of codensity bisimilarities under our
sufficient condition (Section 8);

After the preliminaries (Section 2), we start the paper with a more detailed
overview of our approach (Section 3).

##### Related work

There is a wide range of results in the process algebra literature on proving
compositionality and on rule formats that guarantee it, usually focused on
transition systems (see, e.g., [27] for an overview). A full account is beyond
the scope of this paper. We focus instead on generality in the type of models
and the type of coinductive predicate. Concerning general coalgebraic
frameworks for compositionality, we have already mentioned Turi and Plotkin’s
abstract GSOS format; the main innovation in the current paper is that we go
beyond bisimilarity by employing the codensity lifting.

In [6], it is shown that liftings of distributive laws to fibrations yield so-
called _compatibility_ , a property that ensures soundness of up-to
techniques, and which implies compositionality. On the one hand, if one uses
the so-called canonical relation lifting then all distributive laws lift, but
this only concerns strong bisimilarity; on the other hand, in [6] examples
beyond bisimilarity are studied but liftability there is proven on an ad-hoc
basis. In the current paper we identify the codensity lifting as a sweet spot
between the (restricted) canonical relation lifting and abstract, unrestricted
lifting of functors, and focus instead on conditions that allow to prove
liftability.

Many bisimilarity notions are known to be characterized by winning positions
of certain safety games, including bisimilarity on Kripke frames [30],
probabilistic bisimulation [10, 9], and bisimulation metric [25]. There are
several coalgebraic frameworks [25, 11] that captures such a relationship
between games and bisimilarities. In this paper, we focus on codensity games
[23] that are naturally obtained by codensity liftings and coalgebras.

Codensity liftings are first introduced to lift monads across fibrations [21].
They subsume the Kantorivich metric on the Giry monad. In [28], they are
extended to lift endofunctors across ${\mathbf{CLat}_{\sqcap}}$-fibrations
over $\mathbf{Set}$, and are shown to be a generalization of Baldan et al.’s
Kantorovich lifting [1]. Prior to these papers, the monadic property of the
Kantorovich metric is studied in an unpublished manuscript by van Breugel
[34]. Codensity liftings for endofunctors can be done in other base categories
(such as $\mathbf{Meas}$ and $\mathbf{Vect}$) without modification; see [23].
In [13], the Kantorovich liftings are studied in the context of Lawvere metric
space, and are related with other notions of liftings, such as lax extensions
and (monotone) predicate liftings.

##  2 Preliminaries

For a mathematical entity $x$ equipped with the notion of product $(\times)$,
by $x^{N}$ we mean the $(\times)$-product of $N$-many copies of $x$. For
instance, when $\mathbb{C}$ is a category, $\mathbb{C}^{N}$ denotes the
product category of $N$-many copies of $\mathbb{C}$. By abuse of notation, we
use the same letter $N$ for the set $\\{1,\dots,N\\}$ and write $i\in N$ for
$i\in\\{1,\dots,N\\}$.

For two natural transformations $\alpha\colon F\to G,\beta\colon G\to H$,
their vertical composition is denoted by $\beta\mathbin{\bullet}\alpha$, which
is the componentwise composition of $\beta$ and $\alpha$. For a functor
$p\colon\mathbb{E}\to\mathbb{B}$ and an object $X\in\mathbb{B}$, the fiber
category over $X$, denoted by $\mathbb{E}_{X}$, is the category whose objects
are $P\in\mathbb{E}$ such that $pP=X$, and whose morphisms are $f$ such that
$pf=id_{X}$.

###  2.1 ${\mathbf{CLat}_{\sqcap}}$-fibration

A _${\mathbf{CLat}_{\sqcap}}$ -fibration_ is a posetal fibration
$p\colon\mathbb{E}\to\mathbb{B}$ such that each fiber $\mathbb{E}_{X}$ is a
complete lattice and each pullback
$f^{*}\colon\mathbb{E}_{Y}\rightarrow\mathbb{E}_{X}$ preserves all meets. The
order relation of a fiber $\mathbb{E}_{X}$ is denoted by $\sqsubseteq$, the
meet and the join by $\bigsqcap,\bigsqcup$, and the empty meet and join by
$\top,\bot$. We remark that ${\mathbf{CLat}_{\sqcap}}$-fibrations are a
special case of topological functors [18], where each fiber is a small partial
order.

Examples of ${\mathbf{CLat}_{\sqcap}}$-fibrations are forgetful functors from
the following categories into $\mathbf{Set}$: 1) $\mathbf{Pre}$, the category
of preorders and monotone functions, 2) $\mathbf{EqRel}$, the category of
equivalence relations and relation-respecting functions, 3) $\mathbf{Top}$,
the category of topological spaces and continuous functions, 4)
$\mathbf{PMet}$, the category of pseudometric spaces and non-expansive
functions, 5) $\mathbf{ERel}$, the category of sets with endorelations and
relation-respecting functions. The forgetful functors are denoted by
$U_{\mathbf{Pre}}$ etc.

Every ${\mathbf{CLat}_{\sqcap}}$-fibration $p\colon\mathbb{E}\to\mathbb{B}$ is
faithful, i.e., for any $\mathbb{E}$-object $P,Q$ and $\mathbb{B}$-morphism
$f\colon pP\to pQ$, there is at most one $\mathbb{E}$-morphism $\dot{f}$ such
that $p\dot{f}=f$. When such an $\mathbb{E}$-morphism exists, we write
$f\colon P\mathbin{\dot{\to}}Q$. For instance, when $p$ is the forgetful
functor from $\mathbf{Top}$, the notation
$f\colon(X,O_{X})\mathbin{\dot{\to}}(Y,O_{Y})$ for a function $f\colon X\to Y$
is equivalent to the statement: “$f$ is continuous with respect to topologies
$O_{X},O_{Y}$”. From the fiberedness, $f\colon P\mathbin{\dot{\to}}Q$ is
equivalent to the inequality $P\sqsubseteq f^{*}Q$.

###  2.2 Liftings

We extensively use the concept of lifting of various categorical structures in
this paper. Let $p\colon\mathbb{E}\to\mathbb{B}$ and
$q\colon\mathbb{F}\to\mathbb{C}$ be functors. A lifting of a functor
$F\colon\mathbb{B}\to\mathbb{C}$ along $p,q$ (or simply $p$ when $p=q$) is a
functor ${\dot{F}}\colon\mathbb{E}\to\mathbb{F}$ such that
$q\circ{\dot{F}}=F\circ p$. Similarly, for liftings $\dot{F},\dot{G}$ of
$F,G\colon\mathbb{B}\to\mathbb{C}$ along $p,q$ and a natural transformation
$\alpha\colon F\Rightarrow G$, a lifting of $\alpha$ with respect to
$\dot{F},\dot{G}$ is a natural transformation
$\dot{\alpha}\colon\dot{F}\Rightarrow\dot{G}$ such that
$q\circ\dot{\alpha}=\alpha\circ p$.

To extend the concept of lifting to other categorical structures, it is
convenient to set-up the arrow 2-category $\mathbf{CAT}^{\to}$ given by the
following data: a 0-cell is a functor $p\colon\mathbb{E}\to\mathbb{B}$, a
1-cell from $p\colon\mathbb{E}\to\mathbb{B}$ to
$q\colon\mathbb{F}\to\mathbb{C}$ is a pair
$(F\colon\mathbb{B}\to\mathbb{C},\dot{F}\colon\mathbb{E}\to\mathbb{F})$ of
functors such that $\dot{F}$ is a lifting of $F$ along $p,q$, and a 2-cell
from $(F,\dot{F})\colon p\to q$ to $(G,\dot{G})$ is a pair of natural
transformations $(\alpha,\dot{\alpha})$ such that $\dot{\alpha}$ is a lifting
of $\alpha$ with respect to $\dot{F},\dot{G}$. This 2-category
$\mathbf{CAT}^{\to}$ has 2-products: the terminal 0-cell is $id_{1}$, and the
binary product of $p_{1},p_{2}$ is the product functor $p_{1}\times p_{2}$ (we
only use finite ones in this paper). The evident forgetful 2-functor is
denoted by $\mathrm{cod}\colon\mathbf{CAT}^{\to}\to\mathbf{CAT}$. Any
categorical structure expressible within this 2-category corresponds to a pair
of the categorical structure and its lifting along functors (and vice versa).
For instance, a monad on $p\colon\mathbb{E}\to\mathbb{B}$ in
$\mathbf{CAT}^{\to}$ is a pair of a monad on $\mathbb{B}$ together with its
lifting along $p$ (as a monad).

For the theory of coalgebraic bisimulation in Section 3.3, we often focus on
the full-sub 2-category $\mathbf{CAT}^{{\mathbf{CLat}_{\sqcap}}}$ of
$\mathbf{CAT}^{\to}$ obtained by restricting 0-cells to
${\mathbf{CLat}_{\sqcap}}$-fibrations. We say that a 1-cell
$(F,{\dot{F}})\colon p\to q$ in $\mathbf{CAT}^{\mathbf{CLat}_{\sqcap}}$ is
fibered if ${\dot{F}}$ preserves Cartesian morphisms, or equivalently
$(Ff)^{*}({\dot{F}}P)={\dot{F}}(f^{*}P)$ holds for any $f,P$.

The action of this 2-functor on hom-categories is denoted by the functor
$\mathrm{cod}_{p,q}\colon\mathbf{CAT}^{\to}(p,q)\to\mathbf{CAT}(\mathrm{cod}(p),\mathrm{cod}(q))$.
This is a ${\mathbf{CLat}_{\sqcap}}$-fibration, hence faithful. Thus, for a
natural transformation $\alpha\colon F\Rightarrow G$ and liftings
${\dot{F}},{\dot{G}}$ of $F,G$ respectively, there is at most one lifting
$\dot{\alpha}\colon{\dot{F}}\Rightarrow{\dot{G}}$ of $\alpha$. When it exists,
we say that $\alpha$ is liftable with respect to ${\dot{F}},{\dot{G}}$.

$\displaystyle\mathbf{CAT}^{\mathbf{CLat}_{\sqcap}}(p,q)((F,{\dot{F}}),(G,{\dot{G}}))$
$\displaystyle\cong\\{\alpha\colon F\Rightarrow G~{}|~{}\forall
P\in\mathrm{dom}(p)~{}.~{}\alpha_{pP}\colon{\dot{F}}P\mathbin{\dot{\to}}{\dot{G}}P\\}.$

If $\alpha_{pP}\colon{\dot{F}}P\mathbin{\dot{\to}}{\dot{G}}P$ holds for $P$ in
a subclass $C$ of objects in $\mathbb{E}$, we say that $\alpha$ is liftable on
$C$.

##  3 Overview

The theory of coalgebras provides a categorical framework for expressing
various transition systems in a unified manner. Let $\mathbb{C}$ be a category
and $F\colon\mathbb{C}\to\mathbb{C}$ be an endofunctor (called behavior
functor). An $F$-coalgebra is a pair of an object $X$ (called carrier) and a
morphism $c\colon X\to F(X)$. A morphism from $c\colon X\to F(X)$ to $d\colon
Y\to F(Y)$ is a morphism $h\colon X\to Y$ such that $Fh\circ c=d\circ h$.

######  Example 3.1.

We write ${\mathcal{P}}$ for the covariant powerset functor on $\mathbf{Set}$.
A ${\mathcal{P}}$-coalgebra $c\colon X\to{\mathcal{P}}(X)$ bijectively
corresponds to a binary relation on $X$, that is, a Kripke frame.

######  Example 3.2.

Fix an alphabet $\Sigma$. We define the endofunctor ${F_{\mathrm{da}}}$ on
$\mathbf{Set}$ by ${F_{\mathrm{da}}}\coloneq 2\times(-)^{\Sigma}$. An
${F_{\mathrm{da}}}$-coalgebra $c\colon X\to{F_{\mathrm{da}}}(X)$ bijectively
corresponds to a deterministic automata over alphabet $\Sigma$.

The category of $F$-coalgebras and morphisms between them is denoted by
$\mathbf{Coalg}(F)$, and the evident forgetful functor to $\mathbb{C}$ is
denoted by $U_{F}$. We note that
$(\mathbf{Coalg}(F))^{N}\cong\mathbf{Coalg}(F^{N})$. When $(F,{\dot{F}})\colon
p\to p$ is a 1-cell in $\mathbf{CAT}^{\to}$, the application of $p$ to
${\dot{F}}$-coalgebras extends to a functor
$\mathbf{Coalg}(p)\colon\mathbf{Coalg}({\dot{F}})\to\mathbf{Coalg}(F)$.

###  3.1 Coalgebraic Bisimulation

One of the important concepts in state transition systems is the
identification of two states that behave in the same way. A classical notion
of behavioral equivalence is bisimilarity, which has been extensively studied
in process algebra, coalgebra theory and modal logic. Recently, the concept of
coalgebraic bisimulation, initially formulated as a binary relation, is
expressed using other spatial structures, such as pseudometrics [2] and
topologies [28]. A uniform treatment of these spatial representations of
bisimulation have been developed using the framework of
${\mathbf{CLat}_{\sqcap}}$-fibrations [28]. We employ the formulation of
bisimulation as coalgebras in suitable fibrations. This formulation goes back
to the seminal work by Hermida and Jacobs [17], and the key ingredient is the
lifting of behavior functors along fibrations. We recall their theory here.

Let $p\colon\mathbb{E}\to\mathbb{B}$ be a ${\mathbf{CLat}_{\sqcap}}$-fibration
and $c\colon X\to F(X)$ be an $F$-coalgebra. Hermida and Jacobs’ theory first
chooses a lifting ${\dot{F}}$ of $F$ along $p$; the main body of the
definition of bisimulation is packed into it. Then we formulate an
${\dot{F}}$-bisimulation on a coalgebra $c\colon X\to F(X)$ to be a
${\dot{F}}$-coalgebra $\dot{c}\colon P\to{\dot{F}}(P)$ such that
$p(\dot{c})=c$ (hence $p(P)=X$). The morphism $\dot{c}$ witnesses that $P$ is
respected by the underlying transition system $p(c)$. An
${\dot{F}}$-bisimulation bijectively corresponds to $P\in\mathbb{E}_{X}$
satisfying $P\sqsubseteq c^{*}\circ{\dot{F}}(P)$. We thus define the set of
bisimulations on $c$ by

$\displaystyle\mathbf{Bisim}({\dot{F}},c)$
$\displaystyle\coloneq\\{P\in\mathbb{E}_{X}~{}|~{}P\sqsubseteq
c^{*}\circ{\dot{F}}(P)\\},$

and impose a partial order on it by restricting the one on $\mathbb{E}_{X}$.
Since $\mathbb{E}_{X}$ is a complete lattice, it contains the greatest
postfixpoint $\nu(c^{*}\circ{\dot{F}})$ corresponding to bisimilarity.

######  Example 3.3.

We express the definition of bisimulation for ${\mathcal{P}}$-coalgebras. We
take the ${\mathbf{CLat}_{\sqcap}}$-fibration $U_{\mathbf{EqRel}}$ and take
the following lifting $\dot{\mathcal{P}}$ of ${\mathcal{P}}$ along
$U_{\mathbf{EqRel}}$:

$\displaystyle\dot{\mathcal{P}}(X,P)\coloneq({\mathcal{P}}(X),\\{(U,V)~{}|~{}$
$\displaystyle\forall x\in U~{}.~{}\exists y\in V~{}.~{}(x,y)\in P\wedge$
$\displaystyle\forall x\in V~{}.~{}\exists y\in U~{}.~{}(x,y)\in P\\}).$

Then $P$ is a $\dot{\mathcal{P}}$-bisimulation on $c\colon
X\to{\mathcal{P}}(X)$ if and only if it satisfies the standard bisimulation
condition:

$\displaystyle\forall(x,y)\in P~{}.~{}$ $\displaystyle\forall x^{\prime}\in
c(x)~{}.~{}\exists y^{\prime}\in c(y)~{}.~{}(x^{\prime},y^{\prime})\in
P\wedge$ $\displaystyle\forall y^{\prime}\in c(y)~{}.~{}\exists x^{\prime}\in
c(x)~{}.~{}(x^{\prime},y^{\prime})\in P.$

######  Example 3.4.

We represent language-equivalent states in deterministic automata by the
${\mathbf{CLat}_{\sqcap}}$-fibration $U_{\mathbf{EqRel}}$ and the following
lifting ${\dot{F}_{\mathrm{da}}}$ of ${F_{\mathrm{da}}}$ along $p$:

${\dot{F}_{\mathrm{da}}}(P)\coloneq\\{((t_{1},\rho_{1}),(t_{2},\rho_{2}))\mid
t_{1}=t_{2}\wedge\forall a\in\Sigma~{}.~{}(\rho_{1}(a),\rho_{2}(a))\in P\\}.$

Let $P$ be an ${\dot{F}_{\mathrm{da}}}$-bisimulation on $c\colon
X\to{F_{\mathrm{da}}}(X)$. Then any pair of states $(x,y)\in P$ are language
equivalent, that is, the set of words accepted from $x$ coincides with that of
$y$. Moreover, ${\dot{F}_{\mathrm{da}}}$-bisimilarity coincides with the set
of all language-equivalent state pairs.

###  3.2 Composing $F$-Coalgebras

Let $F\colon\mathbb{C}\to\mathbb{C}$ be an endofunctor over a category
$\mathbb{C}$. We model an $N$-ary composition operation for $F$-coalgebras by
a pair of

  1. 1.

a functor $T\colon\mathbb{C}^{N}\to\mathbb{C}$ (called structure functor)
describing how the operation transforms coalgebra carriers, and

  2. 2.

a natural transformation $\lambda\colon T\circ F^{N}\Rightarrow F\circ T$,
describing the composition of a transition system by merging one-step
transition of its arguments.

The second component induces the lifting
${T}_{\lambda}\colon(\mathbf{Coalg}(F))^{N}\to\mathbf{Coalg}(F)$ of $T$ along
$(U_{F})^{N},U_{F}$ given by

${T}_{\lambda}\coloneq\lambda\circ T(c_{1},\cdots,c_{N}).$

We call the pair $(T,\lambda)$ an $N$-ary one-step composition operation for
$F$-coalgebras.

######  Example 3.5.

We introduce a binary one-step composition operation $(\times,\lambda)$ on
${\mathcal{P}}$-coalgebras. It takes the binary product of coalgebra carriers.
The distributive law
$\lambda^{{\mathcal{P}}}_{X,Y}\colon{\mathcal{P}}X\times{\mathcal{P}}Y\to{\mathcal{P}}(X\times
Y)$ is given by $\lambda^{{\mathcal{P}}}_{X,Y}(A,B)\coloneq A\times B$.

######  Example 3.6.

We introduce a binary one-step composition operation
$(\times,\lambda^{\mathrm{da}})$ on ${F_{\mathrm{da}}}$-coalgebras. It takes
the binary product of coalgebra carriers. The distributive law
$\lambda^{\mathrm{da}}_{X,Y}\colon{F_{\mathrm{da}}}X\times{F_{\mathrm{da}}}Y\to{F_{\mathrm{da}}}(X\times
Y)$ is given by

$\lambda^{\mathrm{da}}_{X,Y}((t_{1},\rho_{1}),(t_{2},\rho_{2}))\coloneq(t_{1}\land
t_{2},~{}\lambda a~{}.~{}(\rho_{1}(a),\rho_{2}(a))).$

###  3.3 Composing Coalgebraic Bismulations

The central theme of this paper is to deepen the understanding of the
interaction between composition operations on coalgebras and the concept of
bisimulation. The question we address is:

######  Question 3.7.

Let $(T,\lambda)$ be an $N$-ary one-step composition operation for
$F$-coalgebras. How can we compose bisimulations $P_{1},\cdots,P_{N}$ on
$F$-coalgebras $c_{1},\cdots,c_{N}$ into a bisimulation on the composed
$F$-coalgebra ${T}_{\lambda}(c_{1},\cdots,c_{N})$?

In other words, the problem is about extending the composition operation on
$F$-coalgebras to bisimulations. Using Hermida and Jacobs’ coalgebraic
formulation of bisimulation, we rephrase Question 3.7 as follows:

######  Question 3.8.

Let $(F,\dot{F})\colon p\to p$ be a 1-cell in
$\mathbf{CAT}^{\mathbf{CLat}_{\sqcap}}$. How can we lift ${T}_{\lambda}$ along
$(\mathbf{Coalg}(p))^{N},\mathbf{Coalg}(p)$?
$\textstyle{(\mathbf{Coalg}({\dot{F}}))^{N}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{(\mathbf{Coalg}(p))^{N}}$$\scriptstyle{?}$$\textstyle{\mathbf{Coalg}({\dot{F}})\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\mathbf{Coalg}(p)}$$\textstyle{(\mathbf{Coalg}(F))^{N}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{{T}_{\lambda}}$$\textstyle{\mathbf{Coalg}(F)}$
(1)

Thanks to the coalgebraic formulation of bisimulation, we notice that a
lifting of the distributive law with respect to liftings of relevant functors
yields the operation (1) on ${\dot{F}}$-bisimulations that is compatible with
the operation on $F$-coalgebras. We formally state this principle that guides
this research as follows. This itself is not new, and a limited version is
seen as [6, Proposition 6.3].

######  Theorem 3.9 (composition of bisimulations).

Let $(F,{\dot{F}})\colon p\to p$ and $(T,{\dot{T}})\colon p^{N}\to p$ be
1-cells in $\mathbf{CAT}^{\mathbf{CLat}_{\sqcap}}$ and
$(\lambda,\dot{\lambda})\colon(T,{\dot{T}})\circ(F^{N},{\dot{F}}^{N})\to(F,{\dot{F}})\circ(T,{\dot{T}})$
be a 2-cell. Then
$(T_{\lambda},\dot{T}_{\dot{\lambda}})\colon(\mathbf{Coalg}(p))^{N}\to\mathbf{Coalg}(p)$
is a 1-cell in $\mathbf{CAT}^{\to}$.∎

A restricted version of this theorem is also available. Let $C$ be a subclass
of objects in $\mathbb{E}$. If $\lambda$ is liftable on $C^{N}$, then we
obtain a 1-cell
$(T_{\lambda},\dot{T}_{\dot{\lambda}})\colon(\mathbf{Coalg}(p)|_{C})^{N}\to\mathbf{Coalg}(p)$;
here $\mathbf{Coalg}(p)|_{C}$ is the restriction of $\mathbf{Coalg}(p)$ to the
category of ${\dot{F}}$-coalgebras over objects in $C$. This restriction will
be used after Proposition 7.3.

######  Corollary 3.10 (preservation of bisimilarities).

In the setting of Theorem 3.9, for any $F$-coalgebra $c_{i}\colon X_{i}\to
F(X_{i})$ ($i=1\cdots N$),

${\dot{T}}(\nu(c_{1}^{*}\circ{\dot{F}}),\cdots,\nu(c_{N}^{*}\circ{\dot{F}}))\sqsubseteq\nu(T_{\lambda}(c_{1},\cdots,c_{N})^{*}\circ{\dot{F}}).\qed$

The preservation holds because $\nu(c^{*}\circ{\dot{F}})$ is the domain of the
terminal object of $\mathbf{Coalg}({\dot{F}})_{c}$ for each $F$-coalgebra $c$,
and $\dot{T}_{\dot{\lambda}}$ maps coalgebras in
$\mathbf{Coalg}({\dot{F}})_{c_{i}}$ ($i\in N$) to a coalgebra in
$\mathbf{Coalg}({\dot{F}})_{T_{\lambda}(c_{1},\cdots,c_{N})}$.

This theorem merely says that when all ingredients $F,\cdots,\dot{\lambda}$
are available, the lifting ${\dot{T}}_{\dot{\lambda}}$ is available. In
practice, the data $F,{\dot{F}},T,\lambda$ are given by hand when designing
transition systems and bisimulations on them, while a problematic part is
defining a lifting of the structure ${\dot{T}}$, and make the distributive law
$\lambda$ liftable with respect to ${\dot{T}}\circ({\dot{F}})^{N}$ and
${\dot{F}}\circ{\dot{T}}$.

Regarding lifting the behavior functor $F$, recently a systematic method
called the codensity lifting has been introduced [29]. This is a
generalization of Kantorovich lifting [2], a classical notion of distance
between distributions, to general ${\mathbf{CLat}_{\sqcap}}$-fibrations. The
advantage of the codensity lifting is its flexibility; it has some parameters
and by varying it we obtain various liftings. Yet, it provides more structure
than assuming arbitrary liftings of $F$ and $T$. Another important point is
that codensity bisimulations, where ${\dot{F}}$ is a codensity lifting, have
an interesting game-theoretic characterization. This flexibility and relevance
to bisimulation games is attractive, so we address the problem of having the
codensity liftings and the liftable $\lambda$. This involves two specific
questions. One is about extending the codensity lifting technique to lift not
only behavior functors, but also structure functors $T$.

######  Question 3.11.

Let $(T,\lambda)$ be an $N$-ary one-step composition operation for
$F$-coalgebras. 1. How do we non-trivially lift structure functors (such as
$N$-ary product functors) in order to capture composition operators at the
level of relations? 2. When is $\lambda$ liftable as a distributive law
between codensity liftings of $F$ and $T$?

To answer to these questions, we employ Beohar et al.’s recent decomposition
result of codensity liftings [3]. Their decomposition separates fibration-
specific parts in the codensity lifting from a central part that does the
actual lifting task. Upon their decomposition, in Section 5, we first address
(1) by generalizing the codensity lifting to arbitrary functors. Then in
Section 6, we address (2) by providing a sufficient condition to lift
$\lambda$ to a distributive law between codensity liftings. The proof of the
sufficiency takes advantage of the decomposition and a 2-categorical nature of
the central part in the decomposition.

##  4 Generalizing the Codensity Lifting

We recall the multiple parameter codensity lifting in [29]. It lifts an
endofunctor $F\colon\mathbb{B}\to\mathbb{B}$ along a
${\mathbf{CLat}_{\sqcap}}$-fibration $p\colon\mathbb{E}\to\mathbb{B}$ using
three parameters $\Omega,\mathbf{\Omega},\tau$. We pack
$(p,\Omega,\mathbf{\Omega})$ into the following data.

######  Definition 4.1.

Let $A$ be a discrete category. A ${\mathbf{CLat}_{\sqcap}}$-fibration with
truth values is a tuple $(p\colon\mathbb{E}\to\mathbb{B},\Omega\colon
A\to\mathbb{B},\mathbf{\Omega}\colon A\to\mathbb{E})$ of functors such that
$\Omega=p\circ\mathbf{\Omega}$ and $p$ is a
${\mathbf{CLat}_{\sqcap}}$-fibration. The notation for a
${\mathbf{CLat}_{\sqcap}}$-fibration with truth values is
$(\Omega,\mathbf{\Omega})\colon Id_{A}\to(p\colon\mathbb{E}\to\mathbb{B})$.

Let $(\Omega,\mathbf{\Omega})\colon Id_{A}\to(p\colon\mathbb{E}\to\mathbb{B})$
be a ${\mathbf{CLat}_{\sqcap}}$-fibration with truth values. The codensity
lifting of a functor $F\colon\mathbb{B}\to\mathbb{B}$ takes as argument a
natural transformation $\tau\colon F\circ\Omega\to\Omega$. The components
$\tau_{a}\colon F\circ\Omega(a)\to\Omega(a)$ are referred to in coalgebraic
modal logic as _modalities_ ; $\tau$ is just an indexed collection of these,
and below we will often refer to $\tau$ itself as a modality. The codensity
lifting of $F\colon\mathbb{B}\to\mathbb{B}$ with $\tau$ along $p$ is given by

$\textstyle[F,\tau]^{\mathbf{\Omega}}X\coloneq\bigsqcap_{a\in
A,k\in\mathbb{E}(X,\mathbf{\Omega}(a))}(\tau_{a}\circ
F(pk))^{*}(\mathbf{\Omega}(a)).$

It is an endofunctor over $\mathbb{E}$, and is a lifting of $F$ along $p$.
When $A=1$, it is called the single-parameter codensity lifting.
${\dot{F}}$-bisimulations (resp. ${\dot{F}}$-bisimilarities) where ${\dot{F}}$
is a codensity lifting are called codensity bisimulations (resp. codensity
bisimilarities).

######  Example 4.2.

We write $2$ for the two-point set $\\{\mathrm{false},\mathrm{true}\\}$ and
$\mathrm{Eq}_{2}$ for the object $(2,\\{(x,x)~{}|~{}x\in 2\\})$ in
$\mathbf{EqRel}$. We identify it as a functor of type $1\to\mathbf{EqRel}$,
and form a ${\mathbf{CLat}_{\sqcap}}$-fibration with truth values
$(2,\mathrm{Eq}_{2})\colon Id_{1}\to U_{\mathbf{EqRel}}$. The codensity
lifting of ${\mathcal{P}}$ with the modality
$\diamond\colon{\mathcal{P}}(2)\to 2$ given by $\diamond(U)=true\iff true\in
U$ coincides with the lifting $\dot{\mathcal{P}}$ in Example 3.3 [23].
Therefore the standard bisimulations on ${\mathcal{P}}$-coalgebras are
expressible as codensity bisimulations.

######  Example 4.3.

We adopt the following ${\mathbf{CLat}_{\sqcap}}$-fibration with truth values
$(\Omega,\mathbf{\Omega})\colon Id_{\Sigma\uplus\\{\epsilon\\}}\to
U_{\mathbf{EqRel}}$ where $\Omega$ and $\mathbf{\Omega}$ are functors
constantly returning $2$ and $\mathrm{Eq}_{2}$, respectively. We define the
modality for ${F_{\mathrm{da}}}$ by

$\tau_{a}(t,\rho)=\left\\{\begin{array}[]{ll}t&(a=\epsilon)\\\
\rho(a)&(a\in\Sigma).\end{array}\right.$

Then the codensity lifting $[{F_{\mathrm{da}}},\tau]^{\mathbf{\Omega}}$ maps
$(X,P)\in\mathbf{EqRel}$ to the set ${F_{\mathrm{da}}}(X)=2\times X^{\Sigma}$
paired with the following equivalence relation:

$\\{((t_{1},\rho_{1}),(t_{2},\rho_{2}))\mid t_{1}=t_{2}\wedge\forall
a\in\Sigma~{}.~{}(\rho_{1}(a),\rho_{2}(a))\in P\\}.$

The $[{F_{\mathrm{da}}},\tau]^{\mathbf{\Omega}}$-bisimilarity on $c$
identifies the states that accepts the same language.

To organize the discussion, we package all the ingredients into the following
data. It specifies both abstract transition systems and a notion of
bisimulation on them.

######  Definition 4.4.

Codensity bisimulation data consists of a ${\mathbf{CLat}_{\sqcap}}$-fibration
with truth values $(\Omega,\mathbf{\Omega})\colon
Id_{A}\to(p\colon\mathbb{E}\to\mathbb{B})$, a functor
$F\colon\mathbb{B}\rightarrow\mathbb{B}$, and a natural transformation
$\tau\colon F\circ\Omega\to\Omega$.

###  4.1 Decomposition of Codensity Lifting

Let $((\Omega,\mathbf{\Omega})\colon
Id_{A}\to(p\colon\mathbb{E}\to\mathbb{B}),F,\tau)$ be codensity bisimulation
data. Recently, Beohar et al. [3] introduced a decomposition of the codensity
lifting as a “sandwich” of a monotone function within Galois connections. We
adopt their decomposition as it is useful for analyzing the interaction
between codensity liftings. In this paper, we describe their decomposition in
fibered category theory. The decomposition is given as

$[F,\tau]^{\mathbf{\Omega}}=R^{p,\mathbf{\Omega}}\circ\mathrm{Sp}^{A}(F,\tau)\circ
L^{p,\mathbf{\Omega}},\quad(L^{p,\mathbf{\Omega}}\dashv
R^{p,\mathbf{\Omega}})$ (2)

where $\mathrm{Sp}^{A}(F,\tau)$ is an endofunctor over a suitable category
that we introduce below. The corresponding equation in Beohar et al. is in [3,
Section 4.4]. Their presentation is based on indexed lattices, and left and
right adjoints are swapped.111 Our choice of left and right adjoint is
consistent with the codensity lifting of monads (using Eilenberg-Moore
algebra) [22].

The description of the components of (2) is in order. First, we observe that
the product
$[A,U_{\mathbf{Pred}}^{op}]\colon[A,\mathbf{Pred}^{op}]\to[A,\mathbf{Set}^{op}]$
of $A$-fold copies of the opposite of the subobject fibration
$U_{\mathbf{Pred}}\colon\mathbf{Pred}\to\mathbf{Set}$ is a
${\mathbf{CLat}_{\sqcap}}$-fibration. Now the adjunction
$L^{p,\mathbf{\Omega}}\dashv R^{p,\mathbf{\Omega}}$ in (2) is given between
$\mathbb{E}$ and the category obtained by the change-of-base of the fibration
$[A,U_{\mathbf{Pred}}^{op}]$ along the functor
$H(b)\coloneq(\mathbb{B}(b,\Omega(-)))^{op}$:

$\textstyle{\mathbb{E}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{L^{p,\mathbf{\Omega}}}$
$\bot$
---
$\scriptstyle{R^{p,\mathbf{\Omega}}}$$\scriptstyle{p}$$\textstyle{\mathrm{Sp}^{A}(\mathbb{B},\Omega)\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\overline{H}}$$\scriptstyle{r^{A}_{\mathbb{B},\Omega}}$$\textstyle{[A,\mathbf{Pred}^{op}]\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{[A,U_{\mathbf{Pred}}^{op}]}$$\textstyle{\mathbb{B}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{H}$$\textstyle{[A,\mathbf{Set}^{op}]}$

Concretely, an object of $\mathrm{Sp}^{A}(\mathbb{B},\Omega)$ is a pair of an
object $X\in\mathbb{B}$ and a mapping $S\colon A\to\mathbf{Set}$ such that for
any $a\in A$, $S(a)\subseteq\mathbb{B}(X,\Omega(a))$. A morphism from $(X,S)$
to $(Y,T)$ is a morphism $f\colon X\to Y$ such that for any $a\in A$ and $k\in
T(a)$, $k\circ f\in S(a)$.222This category is similar to the one of
topological spaces. Put $A=1$. The mapping $S$ specifies a subset of
$\mathbb{B}(X,\Omega)$, which may be seen as a topology on $X$. An element in
$S$ corresponds to an open subset, and the condition on morphism corresponds
to the backword preservation of open subsets. For this reason we name this
category Sp. The evident projection functor
$r^{A}_{\mathbb{B},\Omega}\colon\mathrm{Sp}^{A}(\mathbb{B},\Omega)\to\mathbb{B}$
is a ${\mathbf{CLat}_{\sqcap}}$-fibration, because $s$ is so.

Beohar et al. showed that the following assignments form a left adjoint
functor [3, Theorem 7]:

$\displaystyle L^{p,\mathbf{\Omega}}(P)$ $\displaystyle\coloneq(p(P),\lambda
a~{}.~{}p(\mathbb{E}(P,\mathbf{\Omega}(a)))),$ $\displaystyle
L^{p,\mathbf{\Omega}}(f)\coloneq f,$

and the object part of its right adjoint satisfies

$\textstyle R^{p,\mathbf{\Omega}}(X,S)=\bigsqcap_{a\in A,k\in
S(a)}k^{*}(\mathbf{\Omega}(a)).$

The middle part $\mathrm{Sp}^{A}(\mathbb{B},\Omega)$ in (2) is defined as a
lifting of an endofunctor $F\colon\mathbb{B}\to\mathbb{B}$ along
$r^{A}_{\mathbb{B},\Omega}$ using a modality $\tau\colon
F\circ\Omega\to\Omega$. It is an extension of the predicate lifting $(P\colon
X\to\Omega)\mapsto(\tau\circ F(P)\colon F(X)\to\Omega)$, which is commonly
used in the theory of coalgebras, to sets of morphisms into $\Omega$.

$\displaystyle\mathrm{Sp}^{A}(F,\tau)(X,S)$ $\displaystyle\coloneq(FX,\lambda
a~{}.~{}\\{\tau_{a}\circ Fk~{}|~{}k\in S(a)\\})$ (3)
$\displaystyle\mathrm{Sp}^{A}(F,\tau)(f)$ $\displaystyle\coloneq Ff.$ (4)

By composing the above concrete characterizations of
$L^{p,\mathbf{\Omega}}(P)$, $R^{p,\mathbf{\Omega}}(X,S)$ and
$\mathrm{Sp}^{A}(F,\tau)$, it is immediate that the codensity lifting
satisfies the equation (2).

###  4.2 Generalizing Codensity Liftings

From Beohar et al.’s decomposition, we notice that the actual lifting job of
$F$ is done by $\mathrm{Sp}^{A}(F,\tau)$. We speculate that an extension of
$\mathrm{Sp}$ to natural transformations would also help lifting distributive
laws with respect to codensity liftings. We therefore exhibit a 2-functorial
nature of the $\mathrm{Sp}$ construction. Its domain is the lax coslice
2-category ${A}/\\!/{\mathbf{CAT}}$ under a discrete category $A$, which is
defined as follows:

  * •

A 0-cell is a pair of a category $\mathbb{C}$ with a functor $\Omega\colon
A\to\mathbb{C}$.

  * •

A 1-cell from $(\mathbb{C},\Omega)$ to $(\mathbb{D},\Pi)$ is a pair of a
functor $F\colon\mathbb{C}\to\mathbb{D}$ and a natural transformation
$\tau\colon F\circ\Omega\to\Pi$.

  * •

A 2-cell from $(F,\tau)\colon(\mathbb{C},\Omega)\to(\mathbb{D},\Pi)$ to
$(G,\upsilon)$ is a natural transformation $\alpha\colon F\to G$ such that

Observe that an endo-1-cell on $(\mathbb{C},\Omega)$ bijectively corresponds
to a pair of an endofunctor $F$ on $\mathbb{C}$ and a modality $\tau\colon
F\circ\Omega\to\Omega$.

######  Theorem 4.5.

The following assignments $\mathbf{Sp}^{A}$ form a 2-functor of type
${A}/\\!/{\mathbf{CAT}}\to\mathbf{CAT}^{{\mathbf{CLat}_{\sqcap}}}$.

$\displaystyle\mathbf{Sp}^{A}(\mathbb{C},\Omega)$
$\displaystyle=r^{A}_{\mathbb{C},\Omega}$
$\displaystyle\mathbf{Sp}^{A}(F,\tau)$
$\displaystyle=(F,\mathrm{Sp}^{A}(F,\tau))$
$\displaystyle\mathbf{Sp}^{A}(\alpha)$ $\displaystyle=\alpha$

Here, the functor $\mathrm{Sp}^{A}(F,\tau)$ is the extension of (3) to
arbitrary 1-cell $(F,\tau)\colon(\mathbb{C},\Omega)\to(\mathbb{D},\Pi)$ by the
same formulas (3),(4). Moreover, $\mathrm{Sp}^{A}(F,\tau)$ preserves Cartesian
morphisms and all meets. ∎

This construction suggests that a categorical structure in
${A}/\\!/{\mathbf{CAT}}$ is transferred to
${\mathbf{CLat}_{\sqcap}}$-fibrations equipped with the same categorical
structure and its lifting. We employ this property to transfer distributive
laws in ${A}/\\!/{\mathbf{CAT}}$ to $\mathbf{CAT}^{\mathbf{CLat}_{\sqcap}}$ in
Theorem 6.2.

As the construction of $\mathrm{Sp}^{A}(F,\tau)$ is extended to arbitrary
1-cells $(\mathbb{C},\Omega)\to(\mathbb{D},\Pi)$, it is natural to put
different adjoints in the decomposition (2). This leads us to the following
generalization:

######  Definition 4.6.

Let $(\Omega,\mathbf{\Omega})\colon Id_{A}\to(p\colon\mathbb{E}\to\mathbb{B})$
and $(\Pi,\mathbf{\Pi})\colon Id_{A}\to(q\colon\mathbb{F}\to\mathbb{C})$ be
${\mathbf{CLat}_{\sqcap}}$-fibrations with truth values. The codensity lifting
of $F\colon\mathbb{B}\to\mathbb{C}$ along $p,q$ with a natural transformation
$\tau\colon F\circ\Omega\to\Pi$, denoted by
$[F,\tau]^{\mathbf{\Omega},\mathbf{\Pi}}$, is defined by

$\displaystyle[F,\tau]^{\mathbf{\Omega},\mathbf{\Pi}}$ $\displaystyle\coloneq
R^{q,\mathbf{\Pi}}\circ\mathrm{Sp}^{A}(F,\tau)\circ L^{p,\mathbf{\Omega}}$ (5)
$\displaystyle\textstyle=\bigsqcap_{a\in
A,k\in\mathbb{E}(-,\mathbf{\Omega}(a))}(\tau_{a}\circ
F(pk))^{*}(\mathbf{\Pi}(a)).$

We show some properties of this generalized codensity lifting. The following
shows that it is the largest lifting that makes $\tau$ liftable with respect
to $\dot{F}\circ\mathbf{\Omega}$ and $\mathbf{\Pi}$. Here, two liftings
${\dot{F}},\ddot{F}$ of $F$ are compared by: ${\dot{F}}\sqsubseteq\ddot{F}$ if
${\dot{F}}(P)\sqsubseteq\ddot{F}(P)$ for any $P$.

######  Theorem 4.7.

For any $(F,\dot{F})\in\mathbf{CAT}^{\mathbf{CLat}_{\sqcap}}(p,q)$,
$\dot{F}\sqsubseteq[F,\tau]^{\mathbf{\Omega},\mathbf{\Pi}}$ if and only if
$\tau\colon\dot{F}\circ\mathbf{\Omega}\mathbin{\dot{\to}}\mathbf{\Pi}$ in the
fibration $\mathrm{cod}_{\mathrm{Id}_{A},q}$ (§2.2). ∎

This is the generalization of the universal property possessed by codensity
liftings [29, Theorem 5.14].

When the indexing set $A$ is one-point $1$, the codensity lifting
$[F,\tau]^{\mathbf{\Omega},\mathbf{\Pi}}$ is determined by the object
$[F,\tau]^{\mathbf{\Omega},\mathbf{\Pi}}\mathbf{\Omega}$. We can utilize it
for general cases $(A\neq 1)$ because a codensity lifting is a meet
$\sqcap_{a\in A}[F,\tau_{a}]^{\mathbf{\Omega}(a),\mathbf{\Pi}(a)}$ of $A$, and
we have that $[F,\tau]^{\mathbf{\Omega},\mathbf{\Pi}}$ is determined by
objects $[F,\tau_{a}]^{\mathbf{\Omega}(a),\mathbf{\Pi}(a)}\mathbf{\Omega}(a)$.

######  Proposition 4.8.

Assume $A=1$ in the setting of Definition 4.6. Then
$[F,\tau]^{\mathbf{\Omega},\mathbf{\Pi}}=R^{q,[F,\tau]^{\mathbf{\Omega},\mathbf{\Pi}}\mathbf{\Omega}}\circ\mathrm{Sp}^{1}(F,\mathrm{id})\circ
L^{p,\mathbf{\Omega}}$. ∎

######  Proposition 4.9.

Assume $A=1$ in the setting of Definition 4.6. Let $(F,{\dot{F}})\colon p\to
q$ be a fibered one-cell. If $R^{p,\mathbf{\Omega}}\circ
L^{p,\mathbf{\Omega}}=\mathrm{id}$ and $\dot{F}$ preserves fibered meets, the
following statements hold.

  1. 1.

$\dot{F}=R^{q,\dot{F}\mathbf{\Omega}}\circ\mathrm{Sp}^{1}(F,\mathrm{id})\circ
L^{p,\mathbf{\Omega}}$.

  2. 2.

$[F,\tau]^{\mathbf{\Omega},\mathbf{\Pi}}=\dot{F}$ if and only if
$[F,\tau]^{\mathbf{\Omega},\mathbf{\Pi}}\mathbf{\Omega}=\dot{F}\mathbf{\Omega}$.
∎

The assumption $R^{p,\mathbf{\Omega}}\circ L^{p,\mathbf{\Omega}}=\mathrm{id}$
is mild enough for all examples of ${\mathbf{CLat}_{\sqcap}}$-fibrations in
this paper. The first statement means $\dot{F}$ has the same property as
$[F,\tau]^{\mathbf{\Omega},\mathbf{\Pi}}$ written in Proposition 4.8, and it
immediately yields the second statement. This proposition will be used to get
a criterion for analysing
$[F,\tau]^{\mathbf{\Omega},\mathbf{\Pi}}=\times\colon\mathbb{E}^{2}\to\mathbb{E}$
(Corollary 5.1).

##  5 Codensity Liftings of structure Functors

We use the generalized codensity lifting to lift the structure functor. Let
$(\Omega,\mathbf{\Omega})\colon Id_{A}\to(p\colon\mathbb{E}\to\mathbb{B})$ be
a ${\mathbf{CLat}_{\sqcap}}$-fibration with truth values. Its $N$-fold tupling
$(\langle\Omega\rangle_{N},\langle\mathbf{\Omega}\rangle_{N})\colon
Id_{A}\to(p^{N}\colon\mathbb{E}^{N}\to\mathbb{B}^{N})$ is again a
${\mathbf{CLat}_{\sqcap}}$-fibration with truth values; here
$\langle\Omega\rangle_{N}$ denotes the tupling
$\langle\Omega,\cdots,\Omega\rangle\colon A\to\mathbb{B}^{N}$ of $N$-fold
copies of $\Omega$ (and the same for $\langle\mathbf{\Omega}\rangle_{N}$). We
call the codensity lifting of a structure functor
$T\colon\mathbb{B}^{N}\to\mathbb{B}$ with $\sigma\colon
T\circ\langle\Omega\rangle_{N}\to\Omega$ along $p^{N},p$ the $N$-codensity
lifting. Concretely,

$\displaystyle[T,\sigma]^{\langle\mathbf{\Omega}\rangle_{N},\mathbf{\Omega}}(P_{1},\cdots,P_{N})$
$\displaystyle=\bigsqcap_{\begin{subarray}{c}a\in A,\\\
k_{i}\in\mathbb{E}(P_{i},\mathbf{\Omega}(a))\end{subarray}}(\sigma_{a}\circ
T(pk_{1},\cdots,pk_{n}))^{*}\mathbf{\Omega}(a).$

We overload the notation for the $N$-codensity lifting on that for the
codensity lifting: when $N$ can be read-off from $T$, we simply write
$[T,\sigma]^{\mathbf{\Omega}}$ to mean
$[T,\sigma]^{\langle\mathbf{\Omega}\rangle_{N},\mathbf{\Omega}}$.

###  5.1 Product Functors by Codensity Liftings

One of the most fundamental operators for composing processes and transition
systems is parallel composition. Typically it generates a new transition
system whose states are pairs $x||y$ of component system’s states. This
suggests that the carrier of the composed system is the binary product of the
carrier of its components. We thus study the case where the structure functor
$T$ is $\times\colon\mathbb{B}^{2}\to\mathbb{B}$.

As a side note, we can also handle other structure functors including
coproducts, thanks to the generality of §4. Moreover, our framework
facilitates the investigation of various modalities, even when we fix $T$ to
the product functor, as illustrated in §5.1.2. This enables us to accommodate
various non-trivial liftings for achieving compositionality, particulary in
quantitative analysis (§7).

In this section we illustrate some liftings of the binary product functor, and
show that they can be expressed by the single-parameter $2$-codensity lifting.
It is easy to apply results here to the multiple-parameter codensity lifting
because it is the intersection of the single-parameter one.

####  5.1.1 Product functor on the total category

Suppose that the base category $\mathbb{B}$ has a binary product functor
$\times\colon\mathbb{B}^{2}\to\mathbb{B}$. Since
$p\colon\mathbb{E}\to\mathbb{B}$ is a ${\mathbf{CLat}_{\sqcap}}$-fibration,
the functor $\mathbin{\dot{\times}}\colon\mathbb{E}^{2}\to\mathbb{E}$ defined
by

$P\mathbin{\dot{\times}}Q\coloneq\pi^{*}P\sqcap\pi^{\prime*}Q\quad(\text{$\pi,\pi^{\prime}$
are 1st and 2nd projections})$

is a fibered lifting of $\times$ along $p^{2},p$. It also preserves all meets.
In fact, it is the binary product functor on $\mathbb{E}$ [19, Proposition
9.2.1].

When can $\mathbin{\dot{\times}}$ be expressed by the codensity lifting
$[\times,\sigma]^{\mathbf{\Omega}}$? Since Proposition 4.9 is applicable to
$\mathbin{\dot{\times}}$, we obtain the following:

######  Corollary 5.1.

Let $(\Omega,\mathbf{\Omega})\colon Id_{1}\to(p\colon\mathbb{E}\to\mathbb{B})$
be a ${\mathbf{CLat}_{\sqcap}}$-fibration with truth values such that
$\mathbb{B}$ has binary products, and $R^{p,\mathbf{\Omega}}\circ
L^{p,\mathbf{\Omega}}=\mathrm{id}$. Then for any modality
$\sigma\colon\Omega\times\Omega\to\Omega$, we have
$\mathbin{\dot{\times}}=[\times,\sigma]^{\mathbf{\Omega}}$ if and only if
$[\times,\sigma]^{\mathbf{\Omega}}(\mathbf{\Omega},\mathbf{\Omega})=\mathbf{\Omega}\mathbin{\dot{\times}}\mathbf{\Omega}$.
∎

Therefore one can check
$\mathbin{\dot{\times}}=[\times,\sigma]^{\mathbf{\Omega}}$ only by checking
the equality
$[\times,\sigma]^{\mathbf{\Omega}}(\mathbf{\Omega},\mathbf{\Omega})=\mathbf{\Omega}\mathbin{\dot{\times}}\mathbf{\Omega}$.

######  Example 5.2.

Upon the same ${\mathbf{CLat}_{\sqcap}}$-fibration with truth values
$(2,\mathrm{Eq}_{2})\colon Id_{1}\to U_{\mathbf{EqRel}}$ in Example 4.2, let
$\land\colon 2\times 2\to 2$ be the logical conjunction. Then the binary
product $\mathbin{\dot{\times}}$ on $\mathbf{EqRel}$ is the 2-codensity
lifting $[\times,\land]^{\mathrm{Eq}_{2}}$.

####  5.1.2 Metric lifting of the binary product by a modality

Here we focus on the ${\mathbf{CLat}_{\sqcap}}$-fibration with truth values
$(\mathbb{I},(\mathbb{I},d_{\mathbb{I}}))\colon Id_{1}\to U_{\mathbf{PMet}}$
where $\mathbb{I}$ is the interval $[0,1]$ and
$(\mathbb{I},d_{\mathbb{I}})\in\mathbf{PMet}$ is the Euclidean distance over
the interval on it. We will use it for quantitative bisimulations in §7.1 and
§7.3.

We introduce a metric lifting of the binary product functor using a binary
function on the interval (which we also call a modality). We show that it is
equal to the codensity lifting given by the modality.

######  Proposition 5.3.

Let $\sigma\colon\mathbb{I}\times\mathbb{I}\to\mathbb{I}$ be a function. Given
pseudometric spaces $(X,d_{X}),(Y,d_{Y})$, we define the function
$\times^{\sigma}(d_{X},d_{Y})\colon(X\times Y)^{2}\to\mathbb{I}$ by

$\times^{\sigma}(d_{X},d_{Y})((x,y),(x^{\prime},y^{\prime}))\coloneqq\sigma(d_{X}(x,x^{\prime}),d_{Y}(y,y^{\prime})).$

Then this is a lifting of the product functor
$\times\colon\mathbb{B}^{2}\to\mathbb{B}$ along $U_{\mathbf{PMet}}$ if and
only if $\sigma$ satisfies the following condition:

$\left\\{\begin{array}[]{l}\sigma\text{ is monotone},\\\ \sigma(0,0)=0,\\\
\sigma(a,b)-\sigma(c,d)\leq\sigma(|a-c|,|b-d|).\end{array}\right.$ (6)

Moreover, if $\sigma$ satisfies (6) then
$\times^{\sigma}=[\times,\sigma]^{d_{\mathbb{I}}}$. ∎

For example, the modalities ${\sigma_{\oplus}}(a,b)\coloneqq 1-(1-a)(1-b)$,
${\sigma_{\mathrm{av}}}(a,b)\coloneqq(a+b)/2$, and
$\sigma_{\lor}(a,b)\coloneqq\max(a,b)$ satisfy (6), see Appendix A.2. The
modalities ${\sigma_{\otimes}}(a,b)\coloneqq a\cdot b$ and
$\sigma_{\land}(a,b)\coloneqq\min(a,b)$ do not satisfy the last condition of
(6). However, their codensity liftings are equal to those of
${\sigma_{\oplus}}$ and $\sigma_{\lor}$, respectively. This follows from the
following proposition.

######  Proposition 5.4.

Let $f\colon\Omega\to\Omega$ be an isomorphism in $\mathbb{B}$ satisfying
$f^{*}\mathbf{\Omega}=\mathbf{\Omega}$. Then
$[T,\sigma]^{\mathbf{\Omega}}=[T,\sigma\circ
T(f^{N})]^{\mathbf{\Omega}}=[T,f\circ\sigma]^{\mathbf{\Omega}}$. ∎

Putting $f(a)\coloneqq 1-a$, the proposition above implies
$[\times,{\sigma_{\otimes}}]^{d_{\mathbb{I}}}=[\times,{\sigma_{\oplus}}]^{d_{\mathbb{I}}}$
and
$[\times,\sigma_{\land}]^{d_{\mathbb{I}}}=[\times,\sigma_{\lor}]^{d_{\mathbb{I}}}$
because ${\sigma_{\otimes}}=f\circ{\sigma_{\oplus}}\circ(f\times f)$ and
$\sigma_{\land}=f\circ\sigma_{\lor}\circ(f\times f)$ hold.

##  6 Codensity Lifting of One-Step Composition Operations

As discussed at the end of §3, our focus is on _modalities that lift one-step
composition operations for coalgebras_. Technically, this is equivalent to the
liftability of distributive law $\lambda\colon T\circ F^{N}\to F\circ T$ with
respect to codensity liftings of $F,T$.

######  Definition 6.1.

Let $((\Omega,\mathbf{\Omega})\colon
Id_{A}\to(p\colon\mathbb{E}\to\mathbb{B}),F,\tau)$ be codensity bisimulation
data, and $(T,\lambda)$ be an $N$-ary one-step composition on $F$-coalgebras,
see §3.2 for the definition. We say that _a modality $\sigma\colon
T\circ\langle\Omega\rangle_{N}\to\Omega$ lifts $\lambda$ along $p$_ if
$\lambda$ is liftable with respect to
$[T,\sigma]^{\mathbf{\Omega}}\circ([F,\tau]^{\mathbf{\Omega}})^{N}$ and
$[F,\tau]^{\mathbf{\Omega}}\circ[T,\sigma]^{\mathbf{\Omega}}$.

Recall that the liftability of $\alpha$ may be restricted to a class $C$ of
objects in $\mathbb{E}$. This restriction only appears in §7.3.

###  6.1 Sufficient Condition for Liftability

We provide a sufficient condition for the modality $\sigma$ to lift a
distributive law. Our approach employs the lifting of the distributive law
$\lambda$ by the 2-functor $\mathrm{Sp}$ introduced in Theorem 4.5, and the
decomposed definition of the generalized codensity lifting (5).

First, we restrict $\sigma$ so that $\lambda$ becomes a 2-cell
${A}/\\!/{\mathbf{CAT}}$ of type

$(T,\sigma)\circ(F^{N},\tau^{N})\Rightarrow(F,\tau)\circ(T,\sigma).$

Its image by the 2-functor $\mathrm{Sp}$ yields a lifting $\dot{\lambda}$ of
$\lambda$, whose type is

$\mathrm{Sp}^{A}(T,\sigma)\circ\mathrm{Sp}^{A}(F^{N},\tau^{N})\Rightarrow\mathrm{Sp}^{A}(F,\tau)\circ\mathrm{Sp}^{A}(T,\sigma).$

This lifting enables us to interchange the center of two codensity liftings
that meets in the middle of their composition (below we put $R\coloneq
R^{p,\mathbf{\Omega}},L\coloneq L^{p,\mathbf{\Omega}},R_{N}\coloneq
R^{p^{N},\langle\mathbf{\Omega}\rangle_{N}},L_{N}\coloneq
L^{p^{N},\langle\mathbf{\Omega}\rangle_{N}}$):

$\displaystyle[T,\sigma]^{\mathbf{\Omega}}\circ([F,\tau]^{\mathbf{\Omega}})^{N}$
$\displaystyle=[T,\sigma]^{\mathbf{\Omega}}\circ[F^{N},\tau^{N}]^{\langle\mathbf{\Omega}\rangle_{N}}\hfill\quad(([F,\tau]^{\mathbf{\Omega}})^{N}=[F^{N},\tau^{N}]^{\langle\mathbf{\Omega}\rangle_{N}})$
$\displaystyle=R\circ\mathrm{Sp}^{A}(T,\sigma)\circ L_{N}\circ
R_{N}\circ\mathrm{Sp}^{A}(F^{N},\tau^{N})\circ L_{N}$
$\displaystyle\Rightarrow
R\circ\mathrm{Sp}^{A}(T,\sigma)\circ\mathrm{Sp}^{A}(F^{N},\tau^{N})\circ
L_{N}\hfill\quad(\text{by }L_{N}\dashv R_{N})$ $\displaystyle\Rightarrow
R\circ\mathrm{Sp}^{A}(F,\tau)\circ\mathrm{Sp}^{A}(T,\sigma)\circ L_{N}.$ (7)

Overall, the above natural transformation is again a lifting of $\lambda$,
because the last natural transformation is a lifting of $id$.

Next, we impose the last line (7) to be equal to the composition
$[F,\tau]^{\mathbf{\Omega}}\circ[T,\sigma]^{\mathbf{\Omega}}$ of codensity
liftings. Overall, we obtain a desired lifting of $\lambda$ with respect to
$[T,\sigma]^{\mathbf{\Omega}}\circ([F,\tau]^{\mathbf{\Omega}})^{N}$ and
$[F,\tau]^{\mathbf{\Omega}}\circ[T,\sigma]^{\mathbf{\Omega}}$.

######  Theorem 6.2 (sufficient condition).

Let $((\Omega,\mathbf{\Omega})\colon
Id_{A}\to(p\colon\mathbb{E}\to\mathbb{B}),F,\tau)$ be codensity bisimulation
data and $(T,\lambda)$ be an $N$-ary composition operation on $F$-coalgebras.
Then a modality $\sigma$ lifts $\lambda$ along $p$ if the following conditions
hold.

  1. 1.

$\sigma$ makes $\lambda$ a 2-cell of type
$(T,\sigma)\circ(F^{N},\tau^{N})\Rightarrow(F,\tau)\circ(T,\sigma)$ in
${A}/\\!/{\mathbf{CAT}}$, and

  2. 2.

$R^{p,\mathbf{\Omega}}\circ\mathrm{Sp}^{A}(F,\tau)\circ\mathrm{Sp}^{A}(T,\sigma)\circ
L^{p^{N},\langle\mathbf{\Omega}\rangle_{N}}=[F,\tau]^{\mathbf{\Omega}}\circ[T,\sigma]^{\mathbf{\Omega}}$.
∎

The first condition is equivalent to $\sigma_{a}\circ
T(\left({\tau_{a}}\right)_{i\in N})=\tau_{a}\circ F\sigma_{a}\circ\lambda$ for
each $a\in A$, and it induces
$\mathrm{Sp}^{A}(T,\sigma)\circ\mathrm{Sp}^{A}(F^{N},\tau^{N})=\lambda^{*}\mathrm{Sp}^{A}(F,\tau)\circ\mathrm{Sp}^{A}(T,\sigma)$.

We investigate the second condition. First, it can be expressed as
“$\mathrm{Sp}^{A}(T,\sigma)\circ
L^{p^{N},\langle\mathbf{\Omega}\rangle_{N}}(P)$ is approximating to
$[F,\tau]^{\mathbf{\Omega}}$ for each $P\in\mathbb{E}^{N}$” by the concept of
approximating families introduced by Komorida et al. [24] for expressivity of
coalgebraic modal logics (in a restricted setting where $\mathbf{\Omega}$ is
constant on $A$).

######  Definition 6.3.

An object $S\in\mathrm{Sp}^{A}(\mathbb{B},\Omega)$ is _approximating_ to the
codensity lifting $[F,\tau]^{\mathbf{\Omega}}$ if

$R^{p,\mathbf{\Omega}}\circ\mathrm{Sp}^{A}(F,\tau)(S)\sqsubseteq
R^{p,\mathbf{\Omega}}\circ\mathrm{Sp}^{A}(F,\tau)\circ
L^{p,\mathbf{\Omega}}\circ R^{p,\mathbf{\Omega}}(S).$

That is, for each $a\in A$ and $k\in\mathbb{E}(\bigsqcap_{a^{\prime}\in
A,k^{\prime}\in
S_{a^{\prime}}}k^{\prime*}\mathbf{\Omega}(a^{\prime}),\mathbf{\Omega}(a))$,
$\bigsqcap_{a^{\prime}\in A,k^{\prime}\in
S_{a^{\prime}}}(\tau_{a^{\prime}}\circ
Fk^{\prime})^{*}\mathbf{\Omega}(a^{\prime})\sqsubseteq(\tau_{a}\circ
Fpk)^{*}\mathbf{\Omega}(a)$.

It is equivalent to
$R^{p,\mathbf{\Omega}}\circ\mathrm{Sp}^{A}(F,\tau)(S)=R^{p,\mathbf{\Omega}}\circ\mathrm{Sp}^{A}(F,\tau)\circ
L^{p,\mathbf{\Omega}}\circ R^{p,\mathbf{\Omega}}(S)$ by the counit of
$L^{p,\mathbf{\Omega}}\dashv R^{p,\mathbf{\Omega}}$. Thus (2) in Theorem 6.2
can be written as “$\mathrm{Sp}^{A}(T,\sigma)\circ
L^{p^{N},\langle\mathbf{\Omega}\rangle_{N}}(P)$ is approximating to
$[F,\tau]^{\mathbf{\Omega}}$ for each $P\in\mathbb{E}^{N}$”.

Next we show a result for the approximating condition that is applicable when
we can express $k\in\mathbb{E}(\bigsqcap_{a^{\prime}\in A,k^{\prime}\in
S_{a^{\prime}}}k^{\prime*}\mathbf{\Omega}(a^{\prime}),\mathbf{\Omega}(a))$ by
a subset of $S_{a}$.

######  Proposition 6.4.

Assume that each hom-poset $(\mathbb{B}(X,\Omega),\leq_{X})$ is a complete
lattice, and write $\bigvee$ for the join. Then
$(X,S)\in\mathrm{Sp}^{A}(\mathbb{B},\Omega)$ is approximating to
$[F,\tau]^{\mathbf{\Omega}}$ if all of the following hold, for each $a\in A$:

  1. 1.

For each $S^{\prime}\subseteq\mathbb{C}(X^{\prime},\Omega(a))$, $\tau_{a}\circ
F\bigvee_{f\in S^{\prime}}f=\bigvee_{f\in S^{\prime}}\tau_{a}\circ Ff$.

  2. 2.

For each $S^{\prime}\subseteq\mathbb{C}(X^{\prime},\Omega(a))$,
$\bigsqcap_{f\in S^{\prime}}f^{*}\mathbf{\Omega}\sqsubseteq(\bigvee_{f\in
S^{\prime}}f)^{*}\mathbf{\Omega}(a)$.

  3. 3.

For each $k\in\mathbb{E}(\bigsqcap_{a^{\prime}\in A,k^{\prime}\in
S_{a^{\prime}}}k^{\prime*}\mathbf{\Omega}(a^{\prime}),\mathbf{\Omega}(a))$,
there exists $S^{\prime}_{k}\subseteq S_{a}$ s.t. $pk=\bigvee_{k^{\prime}\in
S^{\prime}_{k}}k^{\prime}$.

Additionally, if these conditions hold,
$(X,S_{a})\in\mathrm{Sp}^{1}(\mathbb{B},\Omega(a))$ is approximating to
$[F,\tau_{a}]^{\mathbf{\Omega}(a)}$ for each $a\in A$. ∎

As a side note, when we prove the sufficient condition by Proposition 6.4, we
get the liftability of $\lambda$ with respect to the composition of not only
$[T,\sigma]^{\mathbf{\Omega}}$ and $[F,\tau]^{\mathbf{\Omega}}$ but also
$[T,\sigma]^{\mathbf{\Omega}}$ and $[F,\tau_{a}]^{\mathbf{\Omega}(a)}$ for
each $a\in A$. The latter is stronger than the former. It enables us to
compose bisimulations with respect to each $a\in A$.

######  Lemma 6.5.

Let $\alpha$ be a natural transformation $F\Rightarrow G$. Then $\alpha$ is a
2-cell $(F,\tau)\Rightarrow(G,\upsilon)$ in ${A}/\\!/{\mathbf{CAT}}$ if and
only if $\alpha$ is a 2-cell $(F,\tau_{a})\Rightarrow(G,\upsilon_{a})$ in
${1}/\\!/{\mathbf{CAT}}$ for each $a\in A$. ∎

######  Proposition 6.6.

If a distributive law $\lambda\colon T\circ F^{N}\Rightarrow F\circ T$ is
liftable w.r.t.
$[T,\sigma]^{\mathbf{\Omega}}\circ([F,\tau_{a}]^{\mathbf{\Omega}(a)})^{N}$ and
$[F,\tau_{a}]^{\mathbf{\Omega}(a)}\circ[T,\sigma]^{\mathbf{\Omega}}$ for each
$a\in A$, then $\sigma$ lifts $\lambda$. ∎

####  6.1.1 Example: Bisimulation for ${\mathcal{P}}$-coalgebras

This example aims to show the composition of standard bisimulations.

##### Codensity bisimulation data

We take the ${\mathbf{CLat}_{\sqcap}}$-fibration with truth values
$(2,\mathrm{Eq}_{2})\colon Id_{1}\to U_{\mathbf{EqRel}}$ and the covariant
powerset functor ${\mathcal{P}}$ (Example 3.1) with the modality
$\diamond\colon{\mathcal{P}}2\to 2$ (Example 4.2) to form codensity
bisimulation data. We have
$[{\mathcal{P}},\diamond]^{\mathrm{Eq}_{2}}=\dot{\mathcal{P}}$ (Example 3.3).

##### Binary one-step composition operation for ${\mathcal{P}}$-coalgebras

We adopt $(\times,\lambda^{{\mathcal{P}}})$ in Example 3.5; recall that the
distributive law $\lambda^{{\mathcal{P}}}$ is given by
$\lambda^{{\mathcal{P}}}_{X,Y}(A,B)=A\times B$.

##### Modality for $\times$

We adopt the modality $\land\colon 2\times 2\to 2$ in Example 5.2. The
codensity lifting $[\times,\land]^{\mathrm{Eq}_{2}}$ coincides with the binary
product of predicates as in Example 5.2.

######  Proposition 6.7.

The modality $\wedge$ lifts $\lambda^{{\mathcal{P}}}$ along
$U_{\mathbf{EqRel}}$. ∎

This proposition, together with Corollary 3.10, implies that for two
${\mathcal{P}}$-coalgebras $c_{1}\colon X_{1}\to{\mathcal{P}}(X_{1})$ and
$c_{2}\colon X_{2}\to{\mathcal{P}}(X_{2})$, if $x_{i}$ and $x_{i}^{\prime}$
are $[{\mathcal{P}},\diamond]^{\mathrm{Eq}_{2}}$-bisimilar in $c_{i}$
($i\in\\{1,2\\}$), the pairs $(x_{1},x_{2})$ and
$(x_{1}^{\prime},x_{2}^{\prime})$ are
$[{\mathcal{P}},\diamond]^{\mathrm{Eq}_{2}}$-bisimilar in the composed
${\mathcal{P}}$-coalgebra $\lambda^{{\mathcal{P}}}\circ(c_{1}\times c_{2})$.

The proof of Proposition 6.7 is the following: $\wedge$ satisfies two
conditions in Theorem 6.2: 1) For each $A,B\subseteq 2$, $\diamond
A\land\diamond B=\diamond\\{a\land b\mid a\in A,b\in B\\}$. 2) As discussed
before Definition 6.3, it is equivalent to approximating objects
$\\{\land\circ(k_{P}\times k_{Q})\mid k_{P}\colon
P\to\mathrm{Eq}_{2},k_{Q}\colon Q\to\mathrm{Eq}_{2}\\}$ for each
$P,Q\in\mathbf{EqRel}$. We can prove it by Proposition 6.4 with the ordered
object $(2,\leq)$ where $\leq$ is the order satisfying
$\mathrm{false}\leq\mathrm{true}$. One easily verifies the first and second
condition in Proposition 6.4. For the third condition, for each $a\in A$ and
$k\colon[\times,\land]^{\mathrm{Eq}_{2}}(P,Q)\to\mathrm{Eq}_{2}$, we define
$S_{k}^{\prime}\coloneqq\\{\land\circ(\chi_{[x]_{P}}\times\chi_{[y]_{Q}})\mid
k(x,y)=1\\}$ where $\chi_{[x]_{P}},\chi_{[y]_{Q}}$ are characteristic
functions. Then $pk=\bigvee_{k^{\prime}\in S^{\prime}_{k}}k^{\prime}$ holds.

####  6.1.2 Example: Language Equivalence of Deterministic Automata

We next capture language equivalence of deterministic automata using codensity
bisimilarity.

##### Codensity bisimulation data

They are set-up in Example 4.3. We package the
${\mathbf{CLat}_{\sqcap}}$-fibration with truth values
$(\Omega,\mathbf{\Omega})\colon Id_{\Sigma\uplus\\{\epsilon\\}}\to
U_{\mathbf{EqRel}}$, the behavior functor ${F_{\mathrm{da}}}$ and the modality
$\tau$ there into codensity bisimulation data.

##### Binary one-step composition operation for ${F_{\mathrm{da}}}$-coalgebras

We adopt the one $(\times,\lambda^{\mathrm{da}})$ in Example 3.6.

##### Modality for $\times$

We adopt the modality $\sigma$ given by $\sigma_{a}\coloneq\land$ (the logical
conjunction; here $a\in\Sigma\uplus\\{\epsilon\\}$). The binary codensity
lifting $[\times,\land]^{\mathrm{Eq}_{2}}$ is equal to that in Example 5.2, so
that $[\times,\land]^{\mathrm{Eq}_{2}}=\mathbin{\dot{\times}}$.

######  Proposition 6.8.

The modality $\sigma$ lifts $\lambda^{\mathrm{da}}$ along
$U_{\mathbf{EqRel}}$. ∎

As a consequence, given deterministic automata $c_{1}\colon
X_{1}\to{F_{\mathrm{da}}}(X_{1})$ and $c_{2}\colon
X_{2}\to{F_{\mathrm{da}}}(X_{2})$, if $x_{i},x_{i}^{\prime}\in X_{i}$ are
language equivalent in $c_{i}$ ($i\in\\{1,2\\}$), the pairs $(x_{1},x_{2})$
and $(x_{1}^{\prime},x_{2}^{\prime})$ are also language equivalent in the
product automaton $\lambda^{\mathrm{da}}\circ(c_{1}\times c_{2})$.

The proof of Proposition 6.8 is as follows. The modality $\land$ satisfies two
conditions in Theorem 6.2: 1) For each $(t,\rho),(t^{\prime},\rho^{\prime})\in
2\times 2^{\Sigma}$, both $\land\circ\tau_{a}$ and
$\tau_{\epsilon}\circ(2\times\land^{\Sigma})\circ\lambda^{\mathrm{da}}$ map
$((t,\rho),(t^{\prime},\rho^{\prime}))$ to $t\land t$ if $a=\epsilon$ and
$\rho(a)\land\rho^{\prime}(a)$ otherwise. 2) We can prove it by Proposition
6.4. The second and third conditions are the same as §6.1.1. The first
condition in Proposition 6.4 holds because for each
$S^{\prime}\subseteq\mathbf{Set}(X^{\prime},2)$, both $\tau_{a}\circ
2\times(\bigvee_{f\in S^{\prime}}f)^{\Sigma}$ and $\bigvee_{f\in
S^{\prime}}\tau_{a}\circ 2\times f^{\Sigma}$ map $(t,\rho)\in 2\times
X^{\prime\Sigma}$ to $t$ if $a=\epsilon$, and $\bigvee_{f\in
S^{\prime}}f(\rho(a))$ otherwise.

###  6.2 Transferring Liftable Modalities

We next study the _transfer_ of liftable modalities from one
${\mathbf{CLat}_{\sqcap}}$-fibration to another. We first see the interaction
between $L/R$ and the $\mathrm{Sp}$.

######  Lemma 6.9.

Let $(F,{\dot{F}})\in\mathbf{CAT}^{{\mathbf{CLat}_{\sqcap}}}(p,q)$.

  1. 1.

$L^{q,{\dot{F}}\mathbf{\Omega}}\circ{\dot{F}}\sqsubseteq\mathrm{Sp}^{A}(F,id)\circ
L^{p,\mathbf{\Omega}}$. They are equal when ${\dot{F}}$ is full.

  2. 2.

${\dot{F}}\circ R^{p,\mathbf{\Omega}}\sqsubseteq
R^{q,{\dot{F}}\mathbf{\Omega}}\circ\mathrm{Sp}^{A}(F,id)$. They are equal when
${\dot{F}}$ is fibered and preserving fibered meets. ∎

When $F=Id$, these properties are working behind Komorida et al.’s argument of
transferring codensity bisimilarities [23]. Let $(Id,G)\colon p\to q$ be a
1-cell in $\mathbf{CAT}^{\mathbf{CLat}_{\sqcap}}$ such that $G$ is full,
fibered and preserving fiberwise meets; such a 1-cell is called a _transfer
situation_ in [23]. Then the 1-cell commutes with codensity liftings, that is,
$G\circ[F,\tau]^{\mathbf{\Omega}}=[F,\tau]^{G\circ\mathbf{\Omega}}\circ G$.
From this commutativity, together with the adjoint lifting theorem of Hermida
and Jacobs [17, Theorem 2.14] (see also [29, 23, 32] for relevant results),
the preservation of codensity bisimilarity is obtained:

$G(\nu(c^{*}\circ[F,\tau]^{\mathbf{\Omega}}))=\nu(c^{*}\circ[F,\tau]^{G\circ\mathbf{\Omega}})\quad(c\colon
X\to F(X)).$

Such $G$ not only transfers the codensity bisimilarities, but also the
liftability property of modalities.

######  Proposition 6.10.

Let $((\Omega,\mathbf{\Omega})\colon
Id_{A}\to(p\colon\mathbb{E}\to\mathbb{B}),F,\tau)$ be codensity bisimulation
data and $(T,\lambda)$ be an $N$-ary composition operation for $F$-coalgebras.
Let $(Id,G)\colon p\to(q\colon\mathbb{F}\to\mathbb{B})$ be a 1-cell in
$\mathbf{CAT}^{\mathbf{CLat}_{\sqcap}}$ such that $G$ is full, fibered and
preserving fibered meets. If a modality $\sigma$ lifts $\lambda$ along $p$,
then $\sigma$ lifts $\lambda$ also along $q$ in the
${\mathbf{CLat}_{\sqcap}}$-fibration with truth values
$((\Omega,G\circ\mathbf{\Omega})\colon
Id_{A}\to(q\colon\mathbb{F}\to\mathbb{B}))$.

The proof uses the equality
$G\circ[T,\sigma]^{\mathbf{\Omega}}=[T,\sigma]^{\langle\mathbf{\Omega}\rangle_{N}}\circ
G^{N}$ derivable from Lemma 6.9.

######  Example 6.11.

Consider the ${\mathbf{CLat}_{\sqcap}}$-fibration
$U_{\mathbf{ERel}}\colon\mathbf{ERel}\to\mathbf{Set}$ and the inclusion
functor $i\colon\mathbf{EqRel}\hookrightarrow\mathbf{ERel}$. Then
$(U_{\mathbf{EqRel}},U_{\mathbf{ERel}},i)$ is a transfer situation. In §6.1.1,
we showed that $\sigma_{\land}$ lifts $\lambda^{\mathcal{P}}$ along
$U_{\mathbf{EqRel}}$. Proposition 6.10 induces that $\sigma_{\land}$ lifts
$\lambda^{\mathcal{P}}$ also along $U_{\mathbf{ERel}}$.

##  7 Examples of Lifting Distributive laws via Modalities

###  7.1 Bisimilarity Pseudometric for Deterministic Automata

We next study a bisimilarity pseudometric for deterministic automata [2, 5],
which is a quantitative extension of language equivalence. We fix a weight
$w\in\mathbb{I}$ where $\mathbb{I}$ is the interval $[0,1]$. We regard the
interval $\mathbb{I}$ as a quantitative extension of binary truth values via
the cast function $i\colon 2\to\mathbb{I}$ defined by $i(\mathrm{true})=0$ and
$i(\mathrm{false})=1$.

##### Codensity bisimulation data

We use the same coalgebraic formulation of deterministic automata as
${F_{\mathrm{da}}}$-coalgebras as §6.1.2 where the functor ${F_{\mathrm{da}}}$
is introduced in Example 4.3. The difference from that example is that we
employ the category of pseudometric spaces for modeling bisimilarity
pseudometrics. We adopt the ${\mathbf{CLat}_{\sqcap}}$-fibration with truth
values $(\Omega,\mathbf{\Omega})\colon Id_{\Sigma\uplus\\{\epsilon\\}}\to
U_{\mathbf{PMet}}$ where $\mathbf{\Omega}$ constantly returns the Euclidean
space $(\mathbb{I},d_{\mathbb{I}})$ over the $[0,1]$-interval. We pair it with
the behavior functor ${F_{\mathrm{da}}}$ for deterministic automata and the
following modality $\tau_{a}\colon{F_{\mathrm{da}}}(\mathbb{I})\to\mathbb{I}$
to obtain codensity bisimulation data:

$\tau_{a}(t,\rho)=\left\\{\begin{array}[]{ll}t&a=\epsilon\\\
w\cdot\rho(a)&a\in\Sigma.\end{array}\right.$

The codensity lifting $[{F_{\mathrm{da}}},\tau]^{\mathbf{\Omega}}$ maps
$(X,d)\in\mathbf{PMet}$ to the space over ${F_{\mathrm{da}}}X$ with the
following pseudometric:

$((t_{1},\rho_{1}),(t_{2},\rho_{2}))\mapsto
max\\{|t_{1}-t_{2}|,w\cdot\max_{a\in\Sigma}d(\rho_{1}(a),\rho_{2}(a))\\}.$

Now, $[{F_{\mathrm{da}}},\tau]^{\mathbf{\Omega}}$-bisimilarity on an
${F_{\mathrm{da}}}$-coalgebra $c\colon X\to{F_{\mathrm{da}}}(X)$ is a
quantitative extension of language equivalence on $X$. It maps
$(x,x^{\prime})\in X^{2}$ to $0$ if the languages of $x,x^{\prime}$ are the
same, and $w^{n}$ otherwise where $n$ is the minimum length of a word that is
accepted from one and not from the other. This notion corresponds to language
equivalence if $w=1$.

##### Binary one-step composition operation

We reuse $(\times,\lambda^{\mathrm{da}})$ in Example 3.6.

##### Modality for $\times$

We adopt $\sigma_{\land}\colon\mathbb{I}^{2}\to\mathbb{I}$ given in §5.1.2. As
we saw in §5.1.2, the binary codensity lifting
$[\times,\sigma_{\land}]^{d_{\mathbb{I}}}$ maps
$(X,d_{1}),(X,d_{2})\in\mathbf{PMet}$ to the space on $X\times Y$ with the
following pseudometric:

$((x,y),(x^{\prime},y^{\prime}))\mapsto\max(d_{1}(x,x^{\prime}),d_{2}(y,y^{\prime})).$

######  Proposition 7.1.

The modality $\sigma_{\land}$ lifts $\lambda^{\mathrm{da}}$ along
$U_{\mathbf{PMet}}$. ∎

This liftability yields a bound of bisimilarity pseudometrics of composite
automata: given deterministic automata $c_{1}\colon
X_{1}\to{F_{\mathrm{da}}}(X_{1})$ and $c_{2}\colon
X_{2}\to{F_{\mathrm{da}}}(X_{2})$, the distance between $(x,y)$ and
$(x^{\prime},y^{\prime})$ in the product automaton
$\lambda^{\mathrm{da}}\circ(c_{1}\times c_{2})$ is bounded by
$\max(v_{1},v_{2})$ where $v_{1}$ is the distance between $x,x^{\prime}$ in
$c_{1}$ and $v_{2}$ is the distance between $y,y^{\prime}$ in $c_{2}$.

The proof is to show that two conditions in Theorem 6.2. See Appendix A.3.1
for its proof.

###  7.2 Similarity Pseudometric for Deterministic Automata

Let us consider similarity on deterministic automata, as a variation of the
example in the previous subsection.

We get a similarity framework just by relaxing the symmetry condition of
$\mathbf{PMet}$ and taking an asymmetric truth-value domain instead of the
Euclidean distance $d_{\mathbb{I}}$. For omitted proofs, see Appendix A.3.2.

##### Codensity bisimulation data

Let $\mathbf{LMet}$ be the category of Lawvere metric spaces (meaning
asymmetric pseudometric spaces) and non-expansive maps. The forgetful functor
$U_{\mathbf{LMet}}\colon\mathbf{LMet}\to\mathbf{Set}$ is a
${\mathbf{CLat}_{\sqcap}}$-fibration like $U_{\mathbf{PMet}}$. We adopt the
${\mathbf{CLat}_{\sqcap}}$-fibration with truth values
$(\Omega,\mathbf{\Omega})\colon Id_{A}\to U_{\mathbf{LMet}}$ such that
$\mathbf{\Omega}$ constantly returns the space over the interval with the
Lawvere metric $d_{\mathbb{I}}^{\mathrm{as}}(x,y)\coloneqq\max(0,y-x)$. We
pair it with the behavior functor ${F_{\mathrm{da}}}$ for deterministic
automata and the same modality $\tau$ in §7.1 to form codensity bisimulation
data.

The codensity lifting $[{F_{\mathrm{da}}},\tau]^{\mathbf{\Omega}}$ maps
$(X,d)\in\mathbf{LMet}$ to the space on ${F_{\mathrm{da}}}(X)$ with the
following Lawvere metric:

$((t_{1},\rho_{1}),(t_{2},\rho_{2}))\mapsto
max\\{d_{\mathbb{I}}^{\mathrm{as}}(i(t_{1}),i(t_{2})),w\cdot\max_{a\in\Sigma}d(\rho_{1}(a),\rho_{2}(a))\\};$

recall that $i\colon 2\to\mathbb{I}$ is the cast function (§7.1). Note that
$d_{\mathbb{I}}^{\mathrm{as}}$ maps $(\mathrm{true},\mathrm{false})$ to $1$
and the others to $0$. In §7.1 we used the Euclidean distance $d_{\mathbb{I}}$
instead of $d_{\mathbb{I}}^{\mathrm{as}}$, which also maps
$(\mathrm{false},\mathrm{true})$ to $1$.

The choice of the Euclidean distance makes a difference in the notion of
bisimilarity. Now $[{F_{\mathrm{da}}},\tau]^{\mathbf{\Omega}}$-bisimilarity on
an ${F_{\mathrm{da}}}$-coalgebra $c\colon X\to{F_{\mathrm{da}}}(X)$ is a
similarity pseudometric on $X$ for the deterministic automaton $c$. It maps
$(x,x^{\prime})\in X^{2}$ to $0$ if the language of $x$ is included in that of
$x^{\prime}$, and $w^{n}$ otherwise where $n$ is the minimum length of a word
that is accepted from $x$ and not from $x^{\prime}$. A bisimialrity
pseudometric in §7.1 detects words that are accepted from $x^{\prime}$ and not
from $x$ while a similarity pseudometric doesn’t.

##### Binary one-step composition operation

We reuse $(\times,\lambda^{\mathrm{da}})$ in Example 3.6.

##### Modality for $\times$

We adopt $\sigma_{\land}\colon\mathbb{I}^{2}\to\mathbb{I}$ given in §5.1.2.
The binary codensity lifting
$[\times,\sigma_{\land}]^{d_{\mathbb{I}}^{\mathrm{as}}}$ maps $(X,d_{1})$ and
$(Y,d_{2})$ to the Lawvere metric on $X\times Y$

$((x,y),(x^{\prime},y^{\prime}))\mapsto\max(d_{1}(x,x^{\prime}),d_{2}(y,y^{\prime})).$

######  Proposition 7.2.

The modality $\sigma_{\land}$ lifts $\lambda^{\mathrm{da}}$ along
$U_{\mathbf{LMet}}$. ∎

This liftability yields a bound of similarity pseudometrics of composite
automata: given deterministic automata $c_{1}\colon
X_{1}\to{F_{\mathrm{da}}}(X_{1})$ and $c_{2}\colon
X_{2}\to{F_{\mathrm{da}}}(X_{2})$, the distance between $(x,y)$ and
$(x^{\prime},y^{\prime})$ in the product automaton
$\lambda^{\mathrm{da}}\circ(c_{1}\times c_{2})$ is bounded by
$\max(v_{1},v_{2})$ where $v_{1}$ is the distance between $x,x^{\prime}$ in
$c_{1}$ and $v_{2}$ is the distance between $y,y^{\prime}$ in $c_{2}$.

The proof is to show that two conditions in Theorem 6.2. See Appendix A.3.2
for its proof.

###  7.3 Bisimulation Metric for Markov Decision Processes

_Bisimulation metric_ is a quantitative notion of behavioral equivalences for
probabilistic systems [8, 7, 35]. We shall see liftability of a distributive
law for composing bisimulation metrics [8].

##### Codensity bisimulation data

We first set-up coalgebraic formulation of Markov decision processes (MDPs)
and bisimulation metric. Let us write
${\mathcal{D}}\colon\mathbf{Set}\to\mathbf{Set}$ for the probability
distribution functor which maps $X$ to the set of distributions on $X$. Then
MDPs are naturally modeled by ${\mathcal{P}}\circ{\mathcal{D}}$-coalgebras
$c\colon X\to{\mathcal{P}}{\mathcal{D}}(X)$. Hereafter we omit the composition
between ${\mathcal{P}}$ and ${\mathcal{D}}$.

For bisimulation metrics, let us provide two codensity bisimulation data for
the Kantorovich and Hausdorff lifting.

The first codensity bisimulation data is $((\mathbb{I},d_{\mathbb{I}})\colon
Id_{1}\to U_{\mathbf{PMet}},{\mathcal{D}},e)$ where $e$ is the expectation
function $e\colon{\mathcal{D}}\mathbb{I}\to\mathbb{I}$. The codensity lifting
$[{\mathcal{D}},e]^{d_{\mathbb{I}}}\colon\mathbf{PMet}\to\mathbf{PMet}$ maps
$d\in\mathbf{PMet}_{X}$ to the Kantorovich pseudometric $\mathcal{K}(d)$ on
${\mathcal{D}}X$:

$(\mu_{1},\mu_{2})\mapsto\sup_{k\in\mathbf{PMet}((X,d),(\mathbb{I},d_{\mathbb{I}}))}|\Sigma_{x\in
X}k(x)\cdot(\mu_{1}(x)-\mu_{2}(x))|.$

The second codensity bisimulation data is $((\mathbb{I},d_{\mathbb{I}})\colon
Id_{1}\to U_{\mathbf{PMet}},{\mathcal{P}},\mathrm{inf})$. The codensity
lifting
$[{\mathcal{P}},\mathrm{inf}]^{d_{\mathbb{I}}}\colon\mathbf{PMet}\to\mathbf{PMet}$
mapping $d\in\mathbf{PMet}_{X}$ to the Hausdorff $\mathcal{H}(d)$ pseudometric
on ${\mathcal{P}}X$:

$\displaystyle(A_{1},A_{2})\mapsto$
$\displaystyle\sup_{k\in\mathbf{PMet}((X,d),(\mathbb{I},d_{\mathbb{I}}))}|\mathrm{inf}_{a_{1}\in
A_{1}}k(a_{1})-\mathrm{inf}_{a_{2}\in A_{2}}k(a_{2})|$ $\displaystyle=$
$\displaystyle\max(\sup_{a_{1}\in A_{1}}\inf_{a_{2}\in
A_{2}}d(a_{1},a_{2}),\sup_{a_{2}\in A_{2}}\inf_{a_{1}\in
A_{1}}d(a_{1},a_{2}))$

Notice that $\mathrm{sup}\,\emptyset=0$ and $\mathrm{inf}\,\emptyset=1$, hence
$\mathcal{H}(d)(\emptyset,A_{2})=1$ for $A_{2}\neq\emptyset$. The equality is
proved in [23, Appendix 3].

Then a
$[{\mathcal{P}},\mathrm{inf}]^{d_{\mathbb{I}}}\circ[{\mathcal{D}},e]^{d_{\mathbb{I}}}$-bisimulation
on $c$ is called a _bisimulation metric_ , and the bisimilarity is called the
_bisimilarity metric_ [7]. It maps a pair of states $(x,y)$ to a distance that
measures quantitative analogue to behavioral equivalences.

##### Binary one-step composition operation

We have seen the binary one-step composition
$(\times,\lambda^{{\mathcal{P}}})$ for ${\mathcal{P}}$ in §6.1.1. We next
introduce the one for ${\mathcal{D}}$ by

$\lambda^{\mathcal{D}}(\mu,\mu^{\prime})\coloneqq(x,y)\mapsto\mu(x)\cdot\mu^{\prime}(y).$

This induces the binary one-step composition
$(\times,\lambda^{{{\mathcal{P}}{\mathcal{D}}}})$ for
${{\mathcal{P}}{\mathcal{D}}}$-coalgebras by

$\lambda^{{{\mathcal{P}}{\mathcal{D}}}}\coloneq({\mathcal{P}}\circ\lambda^{\mathcal{D}})\bullet(\lambda^{\mathcal{P}}\circ{\mathcal{D}}^{2}).$

##### Modality for $\times$

From the discussion above, it is sufficient to find a modality $\sigma$ for
$\times$ that lifts both distributive laws $\lambda^{\mathcal{P}}$ and
$\lambda^{\mathcal{D}}$. Then both distributive laws $\lambda^{\mathcal{P}}$
and $\lambda^{\mathcal{D}}$ become liftable, hence so is
$\lambda^{\mathcal{PD}}$. Among several modalities introduced in §5.1.2, only
${\sigma_{\oplus}}$ lifts both binary operations. Therefore:

######  Proposition 7.3.

The distributive law $\lambda^{{{\mathcal{P}}{\mathcal{D}}}}$ is liftable on
countable pseudometric spaces w.r.t.
$[\times,{\sigma_{\oplus}}]^{d_{\mathbb{I}}}\circ([{\mathcal{P}},\mathrm{inf}]^{d_{\mathbb{I}}}\circ[{\mathcal{D}},e]^{d_{\mathbb{I}}})^{N}$
and
$[{\mathcal{P}},\mathrm{inf}]^{d_{\mathbb{I}}}\circ[{\mathcal{D}},e]^{d_{\mathbb{I}}}\circ[\times,{\sigma_{\oplus}}]^{d_{\mathbb{I}}}$.
∎

As a consequence of the proposition above, given two MDPs $c_{i}\colon
X_{i}\to{{\mathcal{P}}{\mathcal{D}}}(X_{i})$ over at most countable states
$X_{i}$ ($i=1,2$), if $d_{i}$ is a bisimulation metric for $c_{i}$, then the
mapping

$d((x,y),(x^{\prime},y^{\prime}))\coloneq{\sigma_{\oplus}}(d_{1}(x,x^{\prime}),d_{2}(y,y^{\prime}))$

becomes a bisimulation metric for the composite MDP
$\lambda^{{\mathcal{P}}{\mathcal{D}}}\circ(c_{1}\times c_{2})$. Moreover, the
above proposition implies preservation of _bisimilarity metrics_. If $d_{i}$
is the bisimilarity metric for $c_{i}$, then the bisimilarity metric for the
composite MDP $\lambda^{{\mathcal{P}}{\mathcal{D}}}\circ(c_{1}\times c_{2})$
is bounded by $d$. This bound itself was shown in [12]. We give a proof in
terms of composition of distributive laws.

We prove Proposition 7.3 by checking if ${\sigma_{\oplus}}$ lifts both binary
operations $(\times,\lambda^{\mathcal{P}})$ and
$(\times,\lambda^{\mathcal{D}})$. Other $\sigma$ written in §5.1.2 do not
satisfy all conditions in the lemma.

######  Lemma 7.4.

Let $\sigma\colon\mathbb{I}^{2}\to\mathbb{I}$ be a modality satisfying (6), so
that $[\times,\sigma]^{d_{\mathbb{I}}}=\times^{\sigma}$.

  1. 1.

The modality $\sigma$ lifts $\lambda^{{\mathcal{P}}}$ if $\sigma$ is concave,
$\sigma$ preserves infimums, and $\sigma(1,x)=\sigma(x,1)=1$ for any
$x\in\mathbb{I}$.

  2. 2.

The modality $\sigma$ lifts $\lambda^{{\mathcal{D}}}$ on countable
pseudometric spaces if $\sigma$ is concave. ∎

The second statement comes from the following lemma, which is a direct
adaptation of [12, Theorem 2.20] in the context of pseudometric spaces. It can
be proved in almost the same way as the original theorem; here we rely on the
Kantorovich-Rubinstein duality theorem on at most countable sets [36].

######  Lemma 7.5.

Let $X,Y$ be at most countable sets, $(X,d_{1}),(Y,d_{2})\in\mathbf{PMet}$,
and $\sigma\colon\mathbb{I}^{2}\to\mathbb{I}$ be a concave function satisfying
(6). Then for each $\mu_{1},\mu_{1}^{\prime}\in{\mathcal{D}}X$ and
$\mu_{2},\mu_{2}^{\prime}\in{\mathcal{D}}Y$,

$\mathcal{K}(d)(\lambda^{{\mathcal{D}}}_{X,Y}(\mu_{1},\mu_{2}),\lambda^{{\mathcal{D}}}_{X,Y}(\mu_{1}^{\prime},\mu_{2}^{\prime}))\leq\sigma(\mathcal{K}(d_{1})(\mu_{1},\mu_{1}^{\prime}),\mathcal{K}(d_{2})(\mu_{2},\mu_{2}^{\prime}))$
(8)

where $d$ is the pseudometric on $X\times Y$ given by
$d((x,y),(x^{\prime},y^{\prime}))\coloneqq\sigma(d_{1}(x,x^{\prime}),d_{2}(y,y^{\prime}))$.
∎

We did not apply Theorem 6.2 to this case because as of now, it remains
unsolved whether the modality ${\sigma_{\oplus}}$ satisfies the second
condition in Theorem 6.2. We note that the modality satisfies the first
condition.

##  8 Composing Codensity Games

We introduce a composition of codensity games, and show that it preserves game
invariants. As a consequence, we prove the preservation of bisimilarities (the
inequality shown in Corollary 3.10) under the sufficient condition in Theorem
6.2 by composition of games.

###  8.1 Compositionality of Invariants

We briefly recall definitions and results on codensity games. We reserve the
variable $i$ for $N$-indices, and write $\overrightarrow{{x_{i}}}$ for the
sequence of mathematical entities $x_{i}$ (such as morphisms and objects)
indexed by $i\in N$.

######  Definition 8.1.

A _safety game_ is a game $\mathcal{G}=(Q_{\mathbf{D}},Q_{\mathbf{S}},E)$
played by two players $\mathbf{D}$ (Duplicator) and $\mathbf{S}$ (Spoiler)
where $Q_{\mathbf{D}},Q_{\mathbf{S}}$ are sets of positions of
$\mathbf{D},\mathbf{S}$ respectively and $E\subseteq(Q_{\mathbf{D}}\times
Q_{\mathbf{S}}\cup Q_{\mathbf{S}}\times Q_{\mathbf{D}})$ is a set of possible
moves. A play of $\mathcal{G}$ is a finite or infinite sequence of positions
$q_{0},q_{1},\dots$ such that $(q_{i},q_{i+1})\in E$ for each $i$. The player
$\mathbf{S}$ wins a play if the sequence is finite and the last position is in
$Q_{\mathbf{D}}$, and the player $\mathbf{D}$ wins the game otherwise.

A _strategy_ of $\mathbf{D}$ is a partial function $s\colon Q^{*}\times
Q_{\mathbf{D}}\rightharpoonup Q_{\mathbf{S}}$ where $Q^{*}$ is the set of
finite sequences of $Q_{\mathbf{D}}\uplus Q_{\mathbf{S}}$. A strategy $s$ of
$\mathbf{D}$ is _winning_ from $q$ if $\mathbf{D}$ wins any play
$q_{0},q_{1},\dots$ such that $q_{0}=q$ and
$q_{i+1}=s(q_{0},q_{1},\dots,q_{i})$ for each $q_{i}\in Q_{\mathbf{D}}$. A
position $q\in Q_{\mathbf{S}}$ is _winning_ (for $\mathbf{D}$) if there exists
a winning strategy $s$ of $\mathbf{D}$ from $q$.

Winning positions on a safety games are characterizes by _invariants_ , which
also induce winning strategies of $\mathbf{D}$.

######  Definition 8.2.

A set $\mathcal{V}\subseteq Q_{\mathbf{S}}$ is an _invariant_ for $\mathbf{D}$
if for each $q\in\mathcal{V}$ and $q^{\prime}\in Q_{\mathbf{D}}$,
$(q,q^{\prime})\in E$ implies that there is $q^{\prime\prime}\in\mathcal{V}$
such that $(q^{\prime},q^{\prime\prime})\in E$.

######  Proposition 8.3.

A position $q\in Q_{\mathbf{S}}$ is winning if and only if there is an
invariant $\mathcal{V}$ for $\mathbf{D}$ such that $q\in\mathcal{V}$. ∎

Codensity games are safety games that are induced by codensity liftings and
coalgebras.

######  Definition 8.4 (codensity games [23]).

Let $((\Omega,\mathbf{\Omega})\colon
Id_{A}\to(p\colon\mathbb{E}\to\mathbb{B}),F,\tau)$ be codensity bisimulation
data and $c\colon X\to F(X)$ be an $F$-coalgebra. The _codensity game_
$\mathcal{G}_{c}$ is the safety game $(Q_{\mathbf{D}},Q_{\mathbf{S}},E)$
played by two players $\mathbf{D},\mathbf{S}$ where
$Q_{\mathbf{D}}\coloneqq\\{(a,k)\mid a\in A,k\in\mathbb{B}(X,\Omega(a))\\}$,
$Q_{\mathbf{S}}\coloneqq\mathrm{Obj}(\mathbb{E}_{X})$, and
$E\coloneqq{\to_{\mathbf{S}}}\cup{\to_{\mathbf{D}}}$ is given by

$\displaystyle P\to_{\mathbf{S}}(a,k)\text{ if }\tau_{a}\circ Fk\circ c\colon
P\dot{\nrightarrow}\mathbf{\Omega}(a),$
$\displaystyle(a,k)\to_{\mathbf{D}}P^{\prime}\text{ if }k\colon
P^{\prime}\dot{\nrightarrow}\mathbf{\Omega}(a).$

We show characterizations of invariants and winning positions of codensity
games, which are required in the latter part.

######  Proposition 8.5 ([23]).

  1. 1.

A set $\mathcal{V}\subseteq\mathrm{Obj}(\mathbb{E}_{X})$ is an invariant for
$\mathbf{D}$ in the codensity game $\mathcal{G}_{c}$ if and only if
$\bigsqcup_{P\in\mathcal{V}}P$ is an $[F,\tau]^{\mathbf{\Omega}}$-bisimulation
on $c$.

  2. 2.

A position $P\in\mathbb{E}_{X}$ is winning in $\mathcal{G}_{c}$ if and only if
$P$ is a _witness_ of codensity bisimilarity on $c$, that is,
$P\sqsubseteq\nu\bigl{(}c^{*}\circ[F,\tau]^{\mathbf{\Omega}}\bigr{)}$. ∎

Now we move to a codensity game of a composite coalgebra. Given $F$-coalgebras
$c_{i}\colon X_{i}\to F(X_{i})$ ($i\in N$), the codensity game
$\mathcal{G}_{{T}_{\lambda}(\overrightarrow{{c_{i}}})}$ of the composite
coalgebra ${T}_{\lambda}(\overrightarrow{{c_{i}}})$ is given by

$\displaystyle(P\in\mathbb{E}_{T(\overrightarrow{{X_{i}}})})\to_{\mathbf{S}}(a,k)\text{
if }\tau_{a}\circ Fk\circ(\lambda\circ T(\overrightarrow{{c_{i}}}))\colon
P\dot{\nrightarrow}\mathbf{\Omega}(a),$ $\displaystyle(a\in
A,k\in\mathbb{B}(T(\overrightarrow{{X_{i}}}),\Omega(a)))\to_{\mathbf{D}}P^{\prime}\text{
if $k\colon P^{\prime}\dot{\nrightarrow}\mathbf{\Omega}(a)$.}$

In general, the codensity game
$\mathcal{G}_{{T}_{\lambda}(\overrightarrow{{c_{i}}})}$ may not be composed
from each game of $\mathcal{G}_{c_{i}}$: in particular, positions and moves
may not be composed by products, and therefore invariants may not be.

Instead, we define a composite codensity game (Definition 8.6), where
invariants are compositionally preserved:

######  Definition 8.6 (composite codensity games).

Let $((\Omega,\mathbf{\Omega})\colon
Id_{A}\to(p\colon\mathbb{E}\to\mathbb{B}),F,\tau)$ be a codensity bisimulation
data and $c_{i}\colon X_{i}\to F(X_{i})$ ($i\in N$) be $F$-coalgebras. The
_composite codensity game_ $\mathcal{G}_{\overrightarrow{{c_{i}}}}^{T,\sigma}$
is the safety game $(Q_{\mathbf{D}},Q_{\mathbf{S}},E)$ by two players
$\mathbf{D},\mathbf{S}$ where
$Q_{\mathbf{D}}\coloneqq\\{(a,\overrightarrow{{k_{i}}})\mid a\in
A,k_{i}\in\mathbb{C}(X_{i},\Omega(a))\\}$,
$Q_{\mathbf{S}}\coloneqq\prod_{i}\mathrm{Obj}(\mathbb{E}_{X_{i}})$, and
$E\coloneqq\to_{\mathbf{S}}\cup\to_{\mathbf{D}}$ is given by

$\displaystyle\overrightarrow{{P_{i}}}\to_{\mathbf{S}}(a,\overrightarrow{{k_{i}}})\text{
if }\sigma_{a}\circ T(\overrightarrow{{\tau_{a}\circ Fk_{i}\circ
c_{i}}})\colon[T,\sigma]^{\mathbf{\Omega}}\overrightarrow{{P_{i}}}\dot{\nrightarrow}\mathbf{\Omega}(a),$
$\displaystyle(a,\overrightarrow{{k_{i}}})\to_{\mathbf{D}}\overrightarrow{{P^{\prime}_{i}}}\text{
if there is $i\in N$ s.t.~{}$k_{i}\colon
P^{\prime}_{i}\dot{\nrightarrow}\mathbf{\Omega}(a)$.}$

The following proposition shows that we can construct an invariant by
composing invariants of component games $\mathcal{G}_{c_{i}}$.

######  Proposition 8.7.

If each $\mathcal{V}_{i}\subseteq\mathrm{Obj}(\mathbb{E}_{X_{i}})$ is an
invariant of $\mathcal{G}_{c_{i}}$ for $\mathbf{D}$ then $\prod_{i\in
N}\mathcal{V}_{i}$ is an invariant of
$\mathcal{G}_{\overrightarrow{{c_{i}}}}^{T,\sigma}$ for $\mathbf{D}$. ∎

######  Example 8.8.

Consider language equivalence of deterministic automata as presented in
§6.1.2. For an ${F_{\mathrm{da}}}$-coalgebra $c\colon X\to{F_{\mathrm{da}}}X$,
the codensity game $\mathcal{G}_{c}$ is
$((\Sigma\uplus\\{\epsilon\\})\times\mathbf{Set}(X,2),\mathrm{Obj}(\mathrm{EqRel}_{X}),\to_{\mathbf{S}}\cup\to_{\mathbf{D}})$
with

$\displaystyle P\to_{\mathbf{S}}(\epsilon,k)\text{ if }\exists(x,y)\in
P.~{}\pi_{1}c(x)\neq\pi_{1}c(y),$ $\displaystyle
P\to_{\mathbf{S}}(a\in\Sigma,k)\text{ if }\exists(x,y)\in
P.~{}k(\pi_{2}c(x))\neq k(\pi_{2}c(y)),$
$\displaystyle(a,k)\to_{\mathbf{D}}P^{\prime}\text{ if }\exists(x,y)\in
P^{\prime}.~{}k(x)\neq k(y),$

and for two ${F_{\mathrm{da}}}$-coalgebras $\\{c_{i}\colon
X_{i}\to{F_{\mathrm{da}}}X_{i}\\}_{i\in 2}$, the composite codensity game
$\mathcal{G}_{\overrightarrow{{c_{i}}}}^{\times,\sigma_{\land}}$ is
$((\Sigma\uplus\\{\epsilon\\})\times\mathbf{Set}(X_{1},2)\times\mathbf{Set}(X_{2},2),\mathrm{Obj}(\mathrm{EqRel}_{X_{1}})\times\mathrm{Obj}(\mathrm{EqRel}_{X_{2}}),\to_{\mathbf{S}}\cup\to_{\mathbf{D}})$
with

$\displaystyle(P_{1},P_{2})\to_{\mathbf{S}}(\epsilon,k_{1},k_{2})$
$\displaystyle\quad\text{ if }\exists(x_{1},y_{1})\in
P_{1}.~{}\exists(x_{2},y_{2})\in P_{2}.$ $\displaystyle\phantom{\quad\text{ if
}}\pi_{1}c(x_{1})\land\pi_{1}(c(x_{2}))\neq\pi_{1}c(y_{1})\land\pi_{1}c(y_{2}),$
$\displaystyle(P_{1},P_{2})\to_{\mathbf{S}}(a\in\Sigma,k_{1},k_{2})$
$\displaystyle\quad\text{ if }\exists(x_{1},y_{1})\in
P_{1}.~{}\exists(x_{2},y_{2})\in P_{2}.$ $\displaystyle\phantom{\quad\text{ if
}}k(\pi_{2}c(x_{1}))\land k(\pi_{2}(c(x_{2})))\neq k(\pi_{2}c(y_{1}))\land
k(\pi_{2}c(y_{2})),$
$\displaystyle(a,k_{1},k_{2})\to_{\mathbf{D}}(P^{\prime}_{1},P^{\prime}_{2})\text{
if }\exists i\in 2.~{}\exists(x,y)\in P^{\prime}_{i}.~{}k(x_{i})\neq
k(y_{i}).$

In this composite codensity game, positions are composed by pairing and
conditions are composed by the modality $\sigma_{\land}$.

###  8.2 Preservation of Bisimilarities

Under the sufficient condition in Theorem 6.2, as discussed in §6, we
naturally have the following natural transformation above $\lambda$.

$\displaystyle
R\circ\mathrm{Sp}^{A}(T,\sigma)\circ\mathrm{Sp}^{A}(F^{N},\tau^{N})\circ
L_{N}\hfill$ $\displaystyle\Rightarrow
R\circ\mathrm{Sp}^{A}(F,\tau)\circ\mathrm{Sp}^{A}(T,\sigma)\circ L_{N}$
$\displaystyle\text{by \eqref{item:2-cell} in
Thm.~{}\ref{thm:suf_lift_dist}},$
$\displaystyle=[F,\tau]^{\mathbf{\Omega}}[T,\sigma]^{\mathbf{\Omega}}$
$\displaystyle\text{by \eqref{item:approximating} in
Thm.~{}\ref{thm:suf_lift_dist}}.$

It connects invariants in composite codensity games
$\mathcal{G}_{\overrightarrow{{c_{i}}}}^{T,\sigma}$, which utilizes
combination of modalities $\sigma\circ T(\vec{\tau})$, and
$[F,\tau]^{\mathbf{\Omega}}$-bisimulations composed by
$[T,\sigma]^{\mathbf{\Omega}}$. We introduce a join-closure operation for
invariants: for a set $\mathcal{V}\subseteq\prod_{i\in
N}\mathrm{Obj}(\mathbb{E}_{X_{i}})$, we write $\overline{\mathcal{V}}$ for
$\mathcal{V}\cup\Big{\\{}\left({\bigsqcup_{\overrightarrow{{P_{i}}}\in\mathcal{V}}P_{i}}\right)_{i\in
N}\Big{\\}}$. We remark that if a set $\mathcal{V}$ is an invariant of a
codensity game $\mathcal{G}_{c}$ for $\mathbf{D}$ then so is
$\overline{\mathcal{V}}$.

######  Theorem 8.9.

Assume that the sufficient condition in Theorem 6.2 holds and let
$\mathcal{V}\subseteq\prod_{i\in N}\mathrm{Obj}(\mathbb{E}_{X_{i}})$ be a set.

  1. 1.

The set $\mathcal{V}$ is an invariant for $\mathbf{D}$ in
$\mathcal{G}_{\overrightarrow{{c_{i}}}}^{T,\sigma}$ if
$\bigsqcup_{\overrightarrow{{P_{i}}}\in\mathcal{V}}[T,\sigma]^{\mathbf{\Omega}}(\overrightarrow{{P_{i}}})$
is an $[F,\tau]^{\mathbf{\Omega}}$-bisimulation on
${T}_{\lambda}(\overrightarrow{{c_{i}}})$.

  2. 2.

The set $\overline{\mathcal{V}}$ is an invariant for $\mathbf{D}$ in
$\mathcal{G}_{\overrightarrow{{c_{i}}}}^{T,\sigma}$ if and only if
$\bigsqcup_{\overrightarrow{{P_{i}}}\in\overline{\mathcal{V}}}[T,\sigma]^{\mathbf{\Omega}}(\overrightarrow{{P_{i}}})$
is an $[F,\tau]^{\mathbf{\Omega}}$-bisimulation on
${T}_{\lambda}(\overrightarrow{{c_{i}}})$. ∎

######  Corollary 8.10.

Assume that the sufficient condition in Theorem 6.2 holds. If
$\overrightarrow{{P_{i}}}$ is a winning position for $\mathbf{D}$ with an
invariant $\overline{\mathcal{V}}$ then
$[T,\sigma]^{\mathbf{\Omega}}(\overrightarrow{{P_{i}}})$ is a witness on
${T}_{\lambda}(\overrightarrow{{c_{i}}})$, that is,
$[T,\sigma]^{\mathbf{\Omega}}(\overrightarrow{{P_{i}}})\sqsubseteq\nu\Bigl{(}{\big{(}{T}_{\lambda}(\overrightarrow{{c_{i}}})\big{)}}^{*}\circ[F,\tau]^{\mathbf{\Omega}}\Bigr{)}$.
∎

Finally, through a composite codensity game, we prove the preservation of
bisimilarities (the inequalities shown in Corollary 3.10). In the proof, we
instead prove the following equivalent statement:

######  Proposition 8.11.

Assume that the sufficient condition in Theorem 6.2 holds. If $P_{i}$ is a
witness on $c_{i}$, that is,
$P_{i}\sqsubseteq\nu\Bigl{(}{c_{i}}^{*}\circ[F,\tau]^{\mathbf{\Omega}}\Bigr{)}$
for each $i$, then $[T,\sigma]^{\mathbf{\Omega}}(\overrightarrow{{P_{i}}})$ is
a witness on $T_{\lambda}(c_{1},\cdots,c_{N})$, that is,
$[T,\sigma]^{\mathbf{\Omega}}(\overrightarrow{{P_{i}}})\sqsubseteq\nu(T_{\lambda}(c_{1},\cdots,c_{N})^{*}\circ[F,\tau]^{\mathbf{\Omega}})$.

We outline the alternative proof of the proposition by composite codensity
games. If each $P_{i}$ is a witness on codensity bisimilarity on $c_{i}$,
$P_{i}$ is a winning position for $\mathbf{D}$ in $\mathcal{G}_{c_{i}}$ by
Proposition 8.5. Then Proposition 8.3 ensures the existence of invariants
$\overline{\mathcal{V}}_{i}$ of $\mathcal{G}_{c_{i}}$ such that
$P_{i}\in\overline{\mathcal{V}}_{i}$. Proposition 8.7 and $\prod_{i\in
N}\overline{\mathcal{V}}_{i}=\overline{\prod_{i\in N}\mathcal{V}_{i}}$ imply
that $\overrightarrow{{P_{i}}}$ is a winning position with the invariant
$\overline{\prod_{i\in N}\mathcal{V}_{i}}$. Therefore, by Corollary 8.10 we
conclude that $[T,\sigma]^{\mathbf{\Omega}}(\overrightarrow{{P_{i}}})$ is a
witness of codensity bisimilarity on
${T}_{\lambda}(\overrightarrow{{c_{i}}})$.

##  9 Conclusion

In this paper, we have presented generalized codensity liftings in a
2-categorical framework. This development has facilitated the derivation of
liftings of structure functors, especially binary product functors, and
enhanced our understanding and manipulation of codensity liftings.

By integrating the 2-categorical framework of generalized codensity liftings
and structure functors through codensity liftings, we were able to identify a
sufficient condition to lift a distributive law between functors into one
between codensity liftings. Additionally, we have investigated our sufficient
condition from the perspective of compositional reasoning of codensity games.

For future work, we will continue to explore and expand the scope of our
approach, particularly considering different structure functors.

Additionally, we intend to streamline the current categorical notation using
the syntax of categorical logic.

Recently, higher-order abstract GSOS frameworks [14, 33, 15] are actively
studied: they extend behavior endofunctors to bifunctors and use certain
dinatural transformations for distributive laws. Seeking a higher-order
extension of our framework, that is, studying a liftability of distributive
laws along codensity liftings in a higher-order setting is an interesting
future direction. More generally, in the current paper we focused on
compositionality for individual operations. Accomodating languages and calculi
in our approach as defined, for instance, by (abstract) GSOS specifications,
remains future work.

## Acknowledgement

The authors are gradeful to Ichiro Hasuo, and Noboru Isobe for helpful
discussions, and to the anonymous reviewers for helpful feedback. MK, KW and
SK were supported by ERATO HASUO Metamathematics for Systems Design Project
(No. JPMJER1603), JST. MK was supported by JSPS DC KAKENHI Grant (No.
22J21742). KW was supported by the JST grants No. JPMJFS2136 and JPMJAX23CU.
JR was supported by the NWO grant No. OCENW.M20.053.

## References

  * [1] Paolo Baldan, Filippo Bonchi, Henning Kerstan, and Barbara König.  Behavioral metrics via functor lifting.  In FSTTCS, volume 29 of LIPIcs, pages 403–415. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2014.
  * [2] Paolo Baldan, Filippo Bonchi, Henning Kerstan, and Barbara König.  Coalgebraic behavioral metrics.  Log. Methods Comput. Sci., 14(3), 2018.
  * [3] Harsh Beohar, Sebastian Gurke, Barbara König, Karla Messing, Jonas Forster, Lutz Schröder, and Paul Wild.  Expressive quantale-valued logics for coalgebras: An adjunction-based approach.  In STACS, volume 289 of LIPIcs, pages 10:1–10:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024.
  * [4] Bard Bloom, Sorin Istrail, and Albert R. Meyer.  Bisimulation can’t be traced.  J. ACM, 42(1):232–268, 1995.
  * [5] Filippo Bonchi, Barbara König, and Daniela Petrisan.  Up-to techniques for behavioural metrics via fibrations.  In CONCUR, volume 118 of LIPIcs, pages 17:1–17:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018.
  * [6] Filippo Bonchi, Daniela Petrisan, Damien Pous, and Jurriaan Rot.  A general account of coinduction up-to.  Acta Informatica, 54(2):127–190, 2017.
  * [7] Yuxin Deng, Tom Chothia, Catuscia Palamidessi, and Jun Pang.  Metrics for action-labelled quantitative transition systems.  In QAPL, volume 153 of Electronic Notes in Theoretical Computer Science, pages 79–96. Elsevier, 2005.
  * [8] Josée Desharnais, Vineet Gupta, Radha Jagadeesan, and Prakash Panangaden.  Metrics for labelled markov processes.  Theor. Comput. Sci., 318(3):323–354, 2004.
  * [9] Josée Desharnais, François Laviolette, and Mathieu Tracol.  Approximate analysis of probabilistic processes: Logic, simulation and games.  In QEST, pages 264–273. IEEE Computer Society, 2008.
  * [10] Nathanaël Fijalkow, Bartek Klin, and Prakash Panangaden.  Expressiveness of probabilistic modal logics, revisited.  In ICALP, volume 80 of LIPIcs, pages 105:1–105:12. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017.
  * [11] Chase Ford, Stefan Milius, Lutz Schröder, Harsh Beohar, and Barbara König.  Graded monads and behavioural equivalence games.  In LICS, pages 61:1–61:13. ACM, 2022.
  * [12] Daniel Gebler, Kim G. Larsen, and Simone Tini.  Compositional bisimulation metric reasoning with probabilistic process calculi.  Log. Methods Comput. Sci., 12(4), 2016.
  * [13] Sergey Goncharov, Dirk Hofmann, Pedro Nora, Lutz Schröder, and Paul Wild.  Kantorovich functors and characteristic logics for behavioural distances.  In Orna Kupferman and Pawel Sobocinski, editors, Foundations of Software Science and Computation Structures - 26th International Conference, FoSSaCS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2023, Paris, France, April 22-27, 2023, Proceedings, volume 13992 of Lecture Notes in Computer Science, pages 46–67. Springer, 2023.
  * [14] Sergey Goncharov, Stefan Milius, Lutz Schröder, Stelios Tsampas, and Henning Urbat.  Towards a higher-order mathematical operational semantics.  Proc. ACM Program. Lang., 7(POPL):632–658, 2023.
  * [15] Sergey Goncharov, Alessio Santamaria, Lutz Schröder, Stelios Tsampas, and Henning Urbat.  Logical predicates in higher-order mathematical operational semantics.  In FoSSaCS (2), volume 14575 of Lecture Notes in Computer Science, pages 47–69. Springer, 2024.
  * [16] Ichiro Hasuo, Toshiki Kataoka, and Kenta Cho.  Coinductive predicates and final sequences in a fibration.  Math. Struct. Comput. Sci., 28(4):562–611, 2018.
  * [17] Claudio Hermida and Bart Jacobs.  Structural induction and coinduction in a fibrational setting.  Inf. Comput., 145(2):107–152, 1998.
  * [18] Horst Herrlich.  Topological functors.  General Topology and its Applications, 4(2):125 – 142, 1974.
  * [19] Bart Jacobs.  Categorical Logic and Type Theory, volume 141 of Studies in logic and the foundations of mathematics.  North-Holland, 2001.
  * [20] Bart Jacobs.  Introduction to Coalgebra: Towards Mathematics of States and Observation, volume 59 of Cambridge Tracts in Theoretical Computer Science.  Cambridge University Press, 2016.
  * [21] Shin-ya Katsumata and Tetsuya Sato.  Codensity liftings of monads.  In CALCO, volume 35 of LIPIcs, pages 156–170. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2015.
  * [22] Shin-ya Katsumata, Tetsuya Sato, and Tarmo Uustalu.  Codensity lifting of monads and its dual.  Log. Methods Comput. Sci., 14(4), 2018.
  * [23] Yuichi Komorida, Shin-ya Katsumata, Nick Hu, Bartek Klin, Samuel Humeau, Clovis Eberhart, and Ichiro Hasuo.  Codensity games for bisimilarity.  New Gener. Comput., 40(2):403–465, 2022.
  * [24] Yuichi Komorida, Shin-ya Katsumata, Clemens Kupke, Jurriaan Rot, and Ichiro Hasuo.  Expressivity of quantitative modal logics : Categorical foundations via codensity and approximation.  In LICS, pages 1–14. IEEE, 2021.
  * [25] Barbara König and Christina Mika-Michalski.  (metric) bisimulation games and real-valued modal logics for coalgebras.  In CONCUR, volume 118 of LIPIcs, pages 37:1–37:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018.
  * [26] Ugo Dal Lago and Maurizio Murgia.  Contextual behavioural metrics.  In CONCUR, volume 279 of LIPIcs, pages 38:1–38:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023.
  * [27] Mohammad Reza Mousavi, Michel A. Reniers, and Jan Friso Groote.  SOS formats and meta-theory: 20 years after.  Theor. Comput. Sci., 373(3):238–272, 2007.
  * [28] David Sprunger, Shin-ya Katsumata, Jérémy Dubut, and Ichiro Hasuo.  Fibrational bisimulations and quantitative reasoning.  In CMCS, volume 11202 of Lecture Notes in Computer Science, pages 190–213. Springer, 2018.
  * [29] David Sprunger, Shin-ya Katsumata, Jérémy Dubut, and Ichiro Hasuo.  Fibrational bisimulations and quantitative reasoning: Extended version.  J. Log. Comput., 31(6):1526–1559, 2021.
  * [30] Colin Stirling.  Bisimulation, modal logic and model checking games.  Log. J. IGPL, 7(1):103–124, 1999.
  * [31] Daniele Turi and Gordon D. Plotkin.  Towards a mathematical operational semantics.  In LICS, pages 280–291. IEEE Computer Society, 1997.
  * [32] Ruben Turkenburg, Harsh Beohar, Clemens Kupke, and Jurriaan Rot.  Forward and backward steps in a fibration.  In CALCO, volume 270 of LIPIcs, pages 6:1–6:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023.
  * [33] Henning Urbat, Stelios Tsampas, Sergey Goncharov, Stefan Milius, and Lutz Schröder.  Weak similarity in higher-order mathematical operational semantics.  In LICS, pages 1–13, 2023.
  * [34] Franck van Breugel.  The metric monad for probabilistic nondeterminism.  http://www.cse.yorku.ca/ franck/research/drafts/monad.pdf, 2005.
  * [35] Franck van Breugel and James Worrell.  A behavioural pseudometric for probabilistic transition systems.  Theor. Comput. Sci., 331(1):115–142, 2005.
  * [36] Cédric Villani.  Optimal transport: old and new, volume 338.  Springer, 2009.

##  Appendix A Omitted Proofs

###  A.1 Omitted Proofs for Section 5

######  Proposition A.1 (Proof for Example. 5.2).

In Example. 5.2, the ${\mathbf{CLat}_{\sqcap}}$-fibrations with truth values
$(2,(2,\mathrm{Eq_{2}}))\colon Id_{1}\to U_{\mathbf{EqRel}}$ and
$(2,(2,\\{\emptyset,\\{\mathrm{true}\\},2\\}))\colon Id_{1}\to
U_{\mathbf{Top}}$ satisfy
$R^{p,\mathbf{\Omega}}L^{p,\mathbf{\Omega}}=\mathrm{id}$.

###### Proof.

$R^{p,\mathbf{\Omega}}L^{p,\mathbf{\Omega}}=\mathrm{id}$ is equivalent to
$\bigsqcap_{k\colon\mathbf{\Omega}\to\mathbf{\Omega}}k^{*}\mathbf{\Omega}=\mathbf{\Omega}$.

  * •

($(2,(2,\mathrm{Eq_{2}}))\colon Id_{1}\to U_{\mathbf{EqRel}}$):
$\bigsqcap_{k\colon\mathbf{\Omega}\to\mathbf{\Omega}}k^{*}\mathbf{\Omega}=\\{(x,y)\mid\forall
k\colon\mathbf{\Omega}\to\mathbf{\Omega}.~{}kx=ky\\}=\mathbf{\Omega}$ holds.
The last equality is because $(x,y)$ in l.h.s. satisfies $x=y$ by letting
$k\coloneqq\mathrm{id}$, and $(x,y)$ in r.h.s. satisfies $kx=ky$ for each
$k\colon\mathbf{\Omega}\to\mathbf{\Omega}$.

  * •

($(2,(2,\\{\emptyset,\\{\mathrm{true}\\},2\\}))\colon Id_{1}\to
U_{\mathbf{Top}}$):
$\bigsqcap_{k\colon\mathbf{\Omega}\to\mathbf{\Omega}}k^{*}\mathbf{\Omega}$ is
the topology generated by
$\bigcup_{k\colon\mathbf{\Omega}\to\mathbf{\Omega}}\\{k^{-1}A\mid
A\in\mathbf{\Omega}\\}$. $\mathbf{\Omega}$ is included in the topology by
$k\coloneqq\mathrm{id}\colon\mathbf{\Omega}\to\mathbf{\Omega}$, and the
topology is included in $\mathbf{\Omega}$ because $k^{-1}A\in\mathbf{\Omega}$
for each $k\colon\mathbf{\Omega}\to\mathbf{\Omega}$ and $A\in\mathbf{\Omega}$.

∎

###### Proof of Proposition 5.3.

  1. 1.

($\Rightarrow$) Suppose
$\times^{\sigma}\colon\mathbf{PMet}^{2}\to\mathbf{PMet}$ is a lifting of the
product functor $\times$. Consider arbitrary $a,b,c,d\in[0,1]$. For
$x,x^{\prime},x^{\prime\prime}\in\\{a,b,c,d\\}$ we write
$P_{x}\in\mathbf{PMet}_{2}$ for the pseudometric satisfying $P_{x}(0,1)=x$,
and $P_{x,x^{\prime},x^{\prime\prime}}\in\mathbf{PMet}_{3}$ (when
$x+x^{\prime}\leq x^{\prime\prime})$ for the one mapping $(0,1)$ to $x$,
$(1,2)$ to $x^{\prime}$, $(0,2)$ to $x+x^{\prime}$ where $2=\\{0,1\\}$ and
$3=\\{0,1,2\\}$. The modality $\sigma$ is monotone because $a\leq c$ and
$b\leq d$ imply
$\sigma(a,b)=\sigma(P_{a}(0,1),P_{b}(0,1))\leq\sigma(P_{c}(0,1),P_{d}(0,1))=\sigma(c,d)$
by monotonicity of the functor $\times^{\sigma}$.
$\sigma(0,0)=\times^{\sigma}(P_{a},P_{a})((0,0),(0,0))=0$ because
$\times^{\sigma}(P_{a},P_{a})$ is a pseudometric.
$\sigma(a,b)=\times^{\sigma}(P_{c,|a-c|,a},P_{d,|b-d|,b})((0,0),(2,2))\leq\times^{\sigma}(P_{c,|a-c|,a},P_{d,|b-d|,b})((0,0),(1,1))+\times^{\sigma}(P_{c,|a-c|,a},P_{d,|b-d|,b})((1,1),(2,2))=\sigma(|a-c|,|b-d|)+\sigma(c,d)$.
Thus we have $\sigma(a,b)-\sigma(c,d)\leq\sigma(|a-c|,|b-d|)$.

($\Leftarrow$) Suppose $\sigma$ satisfies (6). Then $\times^{\sigma}(P,Q)$ is
a pseudometric for each $P,Q\in\mathbf{PMet}$: For arbitrary
$x,x^{\prime},x^{\prime\prime}\in pP$, $y,y^{\prime},y^{\prime\prime}\in pQ$,

     * •

$\times^{\sigma}(P,Q)((x,y),(x,y))=\sigma(P(x,x),Q(y,y))=\sigma(0,0)=0$,

     * •

$\times^{\sigma}(P,Q)((x,y),(x^{\prime},y^{\prime}))=\sigma(P(x,x^{\prime}),Q(y,y^{\prime}))=\sigma(P(x^{\prime},x),Q(y^{\prime},y))=\times^{\sigma}(P,Q)((x^{\prime},y^{\prime}),(x,y))$,

     * •

$\times^{\sigma}(P,Q)((x,y),(x^{\prime\prime},y^{\prime\prime}))=\sigma(P(x,x^{\prime\prime}),Q(y,y^{\prime\prime}))\leq\sigma(P(x,x^{\prime})+P(x^{\prime},x^{\prime\prime}),Q(y,y^{\prime})+Q(y^{\prime},y^{\prime\prime}))\leq\sigma(P(x,x^{\prime}),Q(y,y^{\prime}))+\sigma(P(x^{\prime},x^{\prime\prime}),Q(y^{\prime},y^{\prime\prime}))=\times^{\sigma}(P,Q)((x,y),(x^{\prime},y^{\prime}))+\times^{\sigma}(P,Q)((x^{\prime},y^{\prime}),(x^{\prime\prime},y^{\prime\prime}))$.

For each $f\colon P\to P^{\prime}$ and $g\colon Q\to Q^{\prime}$ in
$\mathbf{PMet}$, $f\times
g\colon\times^{\sigma}(P,Q)\dot{\rightarrow}\times^{\sigma}(P^{\prime},Q^{\prime})$
by monotonicity of $\sigma$.

  2. 2.

The third condition of (6) is equivalent to
$|\sigma(a,b)-\sigma(c,d)|\leq\sigma(|a-c|,|b-d|)$ for each $a,b,c,d\in[0,1]$,
and it corresponds to
$\sigma\colon\times^{\sigma}(d_{[0,1]})\dot{\rightarrow}d_{[0,1]}$. Therefore
it induces $\times^{\sigma}(P,Q)\sqsubseteq[\times,\sigma]^{d_{[0,1]}}(P,Q)$
for each $P,Q\in\mathbf{PMet}$ by Proposition 4.7. For each
$P,Q\in\mathbf{PMet}$,
$\times^{\sigma}(P,Q)\sqsupseteq[\times,\sigma]^{d_{[0,1]}}(P,Q)$ because for
each $x,x^{\prime}\in pP$ and $y,y^{\prime}\in pQ$, letting $k_{1}(t)\coloneqq
P(x,t)$ and $k_{2}(t)\coloneqq Q(y,t)$,

$\displaystyle\times^{\sigma}(P,Q)((x,y),(x^{\prime},y^{\prime}))$
$\displaystyle=\sigma(P(x,x^{\prime}),Q(y,y^{\prime}))$
$\displaystyle=\sigma(k_{1}(x^{\prime}),k_{2}(y^{\prime}))$
$\displaystyle=|\sigma(k_{1}(x),k_{2}(y))-\sigma(k_{1}(x^{\prime}),k_{2}(y^{\prime}))|$
$\displaystyle=(\sigma\circ k_{1}\times
k_{2})^{*}d_{[0,1]}((x,y),(x^{\prime},y^{\prime}))$
$\displaystyle\sqsupseteq[\times,\sigma]^{d_{[0,1]}}(P,Q)((x,y),(x^{\prime},y^{\prime})).$

∎

######  Proposition A.2.

The modalities ${\sigma_{\oplus}},\sigma_{\lor}$ defined by
${\sigma_{\oplus}}(a,b)\coloneqq 1-(1-a)(1-b)$ and
$\sigma_{\lor}(a,b)\coloneqq\max(a,b)$ satisfy (6).

###### Proof.

For each $\sigma\in\\{{\sigma_{\oplus}},\sigma_{\lor}\\}$, It is easy to show
that $\sigma$ is monotone and $\sigma(0,0)=0$. Here we only show
$\sigma(a,b)-\sigma(c,d)\leq\sigma(|a-c|,|b-d|)$ for each $a,b,c,d\in[0,1]$.

  * •

$(\sigma={\sigma_{\oplus}})$: Let $v_{1}\coloneqq a$, $\epsilon_{1}\coloneqq
a-c$, $v_{2}\coloneqq b$, and $\epsilon_{2}\coloneqq b-d$. Then
$\max(0,\epsilon_{i})\leq v_{i}\leq\min(1,1+\epsilon_{i})\,(i=1,2)$ and (lhs)
$={\sigma_{\oplus}}(v_{1},v_{2})-{\sigma_{\oplus}}(v_{1}-\epsilon_{1},v_{2}-\epsilon_{2})=\epsilon_{1}(1-v_{2})+\epsilon_{2}(1-v_{1})+\epsilon_{1}\epsilon_{2}$.

If $\epsilon_{1},\epsilon_{2}\geq 0$, (lhs)
$\leq\epsilon_{1}(1-\epsilon_{2})+\epsilon_{2}(1-\epsilon_{1})+\epsilon_{1}\epsilon_{2}={\sigma_{\oplus}}(\epsilon_{1},\epsilon_{2})\leq$
(rhs).

If $\epsilon_{1}\geq 0$ and $\epsilon_{2}\leq 0$, (lhs)
$\leq\epsilon_{1}(1-\epsilon_{2})+\epsilon_{2}(1-1)+\epsilon_{1}\epsilon_{2}=\epsilon_{1}\leq$
(rhs).

If $\epsilon_{1}\leq 0$ and $\epsilon_{2}\geq 0$, (lhs)
$\leq\epsilon_{1}(1-1)+\epsilon_{2}(1-\epsilon_{1})+\epsilon_{1}\epsilon_{2}=\epsilon_{2}\leq$
(rhs).

If $\epsilon_{1}\leq 0$ and $\epsilon_{2}\leq 0$, (lhs)
$\leq\epsilon_{1}(1-(1+\epsilon_{2}))+\epsilon_{2}(1-(1+\epsilon_{1}))+\epsilon_{1}\epsilon_{2}=-\epsilon_{1}\epsilon_{2}\leq
0\leq$ (rhs).

  * •

$(\sigma=\sigma_{\lor})$: Since $\sigma_{\lor}(x,y)=\sigma_{\lor}(y,x)$ for
each $x,y\in[0,1]$, we can assume $a\leq b$ without loss of generality.

If $c\leq d$, (lhs) = $b-d\leq|b-d|\leq$ (rhs).

If $c>d$, (lhs) = $b-c$. If $b\leq c$, (lhs) $\leq 0\leq$ (rhs). Otherwise
($b\geq c$), $b-c\leq b-d$ because $d\leq c\leq b$. Therefore (lhs)
$=b-c\leq|b-d|\leq$ (rhs).

∎

###### Proof of Proposition 5.4.

For each $\left({P_{i}}\right)_{i\in N}\in\mathbb{E}^{N}$ and $a\in A$,
$\\{\sigma\circ T(\left({k_{i}}\right)_{i\in N})\mid k_{i}\colon
P_{i}\dot{\to}\mathbf{\Omega}(a)\\}=\\{\sigma\circ T(\left({f\circ
k_{i}}\right)_{i\in N})\mid k_{i}\colon P_{i}\dot{\to}\mathbf{\Omega}(a)\\}$
because for each $\left({k_{i}\colon
P_{i}\dot{\to}\mathbf{\Omega}(a)}\right)_{i\in N}$, $\left({f\circ
k_{i}}\right)_{i\in N},\left({f^{-1}\circ k_{i}}\right)_{i\in N}\colon
P_{i}\dot{\to}\mathbf{\Omega}(a)$ by
$f^{*}\mathbf{\Omega}=\mathbf{\Omega}=(f^{-1})^{*}\mathbf{\Omega}$. It induces
$\mathrm{Sp}^{A}(T,\sigma)\circ
L^{p,\langle\mathbf{\Omega}\rangle_{N}}=\mathrm{Sp}^{A}(T,\sigma\circ
T(f^{N}))\circ L^{p,\langle\mathbf{\Omega}\rangle_{N}}$. Therefore,
$[T,\sigma]^{\mathbf{\Omega}}=R^{p,\langle\mathbf{\Omega}\rangle_{N}}\circ\mathrm{Sp}^{A}(T,\sigma)\circ
L^{p,\langle\mathbf{\Omega}\rangle_{N}}=R^{p,\langle\mathbf{\Omega}\rangle_{N}}\circ\mathrm{Sp}^{A}(T,\sigma\circ
T(f^{N}))\circ L^{p,\langle\mathbf{\Omega}\rangle_{N}}=[T,\sigma\circ
T(f^{N})]^{\mathbf{\Omega}}$.

Similarly, for each $S\in\mathrm{Sp}^{A}(\mathbb{B}^{N},\mathbf{\Omega})$ and
$a\in A$, $\bigsqcap_{a\in A,\left({k_{i}}\right)_{i\in N}\in S}(\sigma\circ
T(\left({k_{i}}\right)_{i\in N}))^{*}\mathbf{\Omega}(a)=\bigsqcap_{a\in
A,\left({k_{i}}\right)_{i\in N}\in S}(\sigma\circ T(\left({k_{i}}\right)_{i\in
N}))^{*}f^{*}\mathbf{\Omega}(a)=\bigsqcap_{a\in A,\left({k_{i}}\right)_{i\in
N}\in S}(f\circ\sigma\circ T(\left({k_{i}}\right)_{i\in
N}))^{*}\mathbf{\Omega}(a)$. It induces
$R^{p,\langle\mathbf{\Omega}\rangle_{N}}\circ\mathrm{Sp}^{A}(T,\sigma)=R^{p,\langle\mathbf{\Omega}\rangle_{N}}\circ\mathrm{Sp}^{A}(T,f\circ\sigma)$.
Therefore,
$[T,\sigma]^{\mathbf{\Omega}}=R^{p,\langle\mathbf{\Omega}\rangle_{N}}\circ\mathrm{Sp}^{A}(T,\sigma)\circ
L^{p,\langle\mathbf{\Omega}\rangle_{N}}=R^{p,\langle\mathbf{\Omega}\rangle_{N}}\circ\mathrm{Sp}^{A}(T,f\circ\sigma)\circ
L^{p,\langle\mathbf{\Omega}\rangle_{N}}=[T,f\circ\sigma]^{\mathbf{\Omega}}$. ∎

###  A.2 Omitted Proofs for Section 6

######  Lemma A.3.

In the setting of Proposition 6.4, if the three conditions in the proposition
hold, then for each $a\in A$,

$R^{p,\mathbf{\Omega}(a)}\circ\mathrm{Sp}^{1}(F,\tau_{a})(S_{a})\sqsubseteq
R^{p,\mathbf{\Omega}(a)}\circ\mathrm{Sp}^{1}(F,\tau_{a})\circ
L^{p,\mathbf{\Omega}(a)}\circ R^{p,\mathbf{\Omega}}(S).$

###### Proof.

For each $a\in A$ and $k\colon\bigsqcap_{a^{\prime}\in A,k^{\prime}\in
S_{a^{\prime}}}k^{\prime*}\mathbf{\Omega}(a^{\prime})\to\mathbf{\Omega}(a)$,

$\displaystyle\bigsqcap_{k^{\prime}\in S_{a}}(\tau_{a}\circ
Fk^{\prime})^{*}\mathbf{\Omega}(a)$
$\displaystyle\sqsubseteq\bigsqcap_{k^{\prime}\in
S^{\prime}_{k}}(\tau_{a}\circ Fk^{\prime})^{*}\mathbf{\Omega}(a)$
$\displaystyle\text{since }S^{\prime}_{k}\subseteq S_{a}$
$\displaystyle\sqsubseteq(\bigvee_{k^{\prime}\in S^{\prime}_{k}}\tau_{a}\circ
Fk^{\prime})^{*}\mathbf{\Omega}(a)$ by the second condition
$\displaystyle=(\tau_{a}\circ F(\bigvee_{k^{\prime}\in
S^{\prime}_{k}}k^{\prime}))^{*}\mathbf{\Omega}(a)$ by the first condition
$\displaystyle=(\tau_{a}\circ Fpk)^{*}\mathbf{\Omega}(a).$ by the third
condition

∎

###### Proof of Proposition 6.4.

Because
$R^{p,\mathbf{\Omega}}\circ\mathrm{Sp}^{A}(F,\tau)(S^{\prime})=\bigsqcap_{a\in
A}R^{p,\mathbf{\Omega}(a)}\circ\mathrm{Sp}^{1}(F,\tau_{a})(S^{\prime}_{a})$
for each $S^{\prime}\in\mathrm{Sp}^{A}(\mathbb{B},\Omega)$, $S$ is
approximating to $[F,\tau]^{\mathbf{\Omega}}$ is equivalent to
$R^{p,\mathbf{\Omega}}\circ\mathrm{Sp}^{A}(F,\tau)(S)\sqsubseteq
R^{p,\mathbf{\Omega}(a)}\circ\mathrm{Sp}^{1}(F,\tau_{a})\circ
L^{p,\mathbf{\Omega}(a)}\circ R^{p,\mathbf{\Omega}}(S)$ for each $a\in A$.
Lemma A.3 and $R^{p,\mathbf{\Omega}}\circ\mathrm{Sp}^{A}(F,\tau)(S)\sqsubseteq
R^{p,\mathbf{\Omega}(a)}\circ\mathrm{Sp}^{1}(F,\tau_{a})(S_{a})$ for each
$a\in A$ conclude the proof. ∎

###### Proof of Proposition 6.10.

Suppose that $\lambda$ is liftable with respect to
$[T,\sigma]^{\mathbf{\Omega}}$, $[F,\tau]^{\mathbf{\Omega}}$, i.e. there is a
natural transformation
$\dot{\lambda}\colon[T,\sigma]^{\mathbf{\Omega}}([F,\tau]^{\mathbf{\Omega}})^{N}\Rightarrow[F,\tau]^{\mathbf{\Omega}}[T,\sigma]^{\mathbf{\Omega}}$
above $\lambda$. Then we have the natural transformation $G\circ\dot{\lambda}$
above $\lambda$. The natural transformation $G\circ\dot{\lambda}$ is from
$[T,\sigma]^{G\mathbf{\Omega}}\circ([F,\tau]^{G\mathbf{\Omega}})^{N}\circ
G^{N}$ to $[F,\tau]^{G\mathbf{\Omega}}\circ[T,\sigma]^{G\mathbf{\Omega}}\circ
G^{N}$ because
$G\circ[T,\sigma]^{\mathbf{\Omega}}\circ([F,\tau]^{\mathbf{\Omega}})^{N}=[T,\sigma]^{G\mathbf{\Omega}}\circ([F,\tau]^{G\mathbf{\Omega}})^{N}\circ
G^{N}$ and
$G\circ[F,\tau]^{\mathbf{\Omega}}\circ[T,\sigma]^{\mathbf{\Omega}}=[F,\tau]^{G\mathbf{\Omega}}\circ[T,\sigma]^{G\mathbf{\Omega}}\circ
G^{N}$ hold by the discussion of §6.2.

Because $G$ is full, it ensures the existence of a natural transformation from
$[T,\sigma]^{G\mathbf{\Omega}}([F,\tau]^{G\mathbf{\Omega}})^{N}$ to
$[F,\tau]^{G\mathbf{\Omega}}[T,\sigma]^{G\mathbf{\Omega}}$ above $\lambda$. ∎

###### Proof of Proposition 6.6.

$[T,\sigma]^{\mathbf{\Omega}}\circ([F,\tau]^{\mathbf{\Omega}})^{N}\Rightarrow\bigsqcap_{a\in
A}[T,\sigma]^{\mathbf{\Omega}}\circ([F,\tau_{a}]^{\mathbf{\Omega}(a)})^{N}\Rightarrow\bigsqcap_{a\in
A}[F,\tau_{a}]^{\mathbf{\Omega}(a)}\circ[T,\sigma]^{\mathbf{\Omega}}=[F,\tau]^{\mathbf{\Omega}}\circ[T,\sigma]^{\mathbf{\Omega}}.$
The first natural transformation is above $\mathrm{id}$ and the second one is
above $\lambda$. ∎

###  A.3 Omitted Proofs for Section 7

####  A.3.1 Bisimilarity Pseudometric

######  Proposition A.4.

In the setting of §7.1, the tuple $((\Omega,\mathbf{\Omega})\colon Id_{A}\to
U_{\mathbf{PMet}},(\times,\lambda^{\mathrm{da}}),\sigma_{\land})$ satisfies
the conditions in Theorem 6.2.

###### Proof.

1) For each $(t,\rho),(t^{\prime},\rho^{\prime})\in 2\times[0,1]^{\Sigma}$,
$(\sigma_{\land}\circ\tau_{\epsilon}\times\tau_{\epsilon})((t,\rho),(t^{\prime},\rho^{\prime}))=t\land
t^{\prime}=(\tau_{\epsilon}\circ(2\times\sigma_{\land}^{\Sigma})\circ\lambda)((t,\rho),(t^{\prime},\rho^{\prime}))$
and
$(\sigma_{\land}\circ\tau_{a}\times\tau_{a})((t,\rho),(t^{\prime},\rho^{\prime}))=w\cdot(\rho(a)\land\rho^{\prime}(a))=(\tau_{a}\circ(2\times\sigma_{\land}^{\Sigma})\circ\lambda)((t,\rho),(t^{\prime},\rho^{\prime}))$
($a\in\Sigma$).

2) We aim to show that for each
$(d_{1},d_{2})\in\mathbf{PMet}_{X}\times\mathbf{PMet}_{Y}$, $a\in A$,
$k\colon[\times,\sigma_{\land}]^{d_{[0,1]}}(d_{1},d_{2})\to d_{[0,1]}$,
$(t_{1},f_{1}),(t_{2},f_{2})\in(2\times(X\times Y)^{\Sigma})$,

$\displaystyle|(\tau_{a}\circ(2\times
k^{\Sigma}))(t_{1},f_{1})-(\tau_{a}\circ(2\times k^{\Sigma}))(t_{2},f_{2})|$
$\displaystyle\leq\sup_{\begin{subarray}{c}a^{\prime}\in A,\\\ k_{1}\colon
d_{1}\to d_{[0,1]},\\\ k_{2}\colon d_{2}\to
d_{[0,1]}\end{subarray}}|(\tau_{a^{\prime}}\circ(2\times(\sigma_{\land}\circ
k_{1}\times
k_{2})^{\Sigma}))(t_{1},f_{1})-(\tau_{a^{\prime}}\circ(2\times(\sigma_{\land}\circ
k_{1}\times k_{2})^{\Sigma}))(t_{2},f_{2})|.$

If $a=\epsilon$, (lhs) $=|t_{1}-t_{2}|=$ (rhs). If $a\in\Sigma$, noting that
$|k(x_{1},y_{1})-k(x_{2},y_{2})|\leq\max(d_{1}(x_{1},x_{2}),d_{2}(y_{1},y_{2}))$
for each $x_{1},x_{2}\in X$ and $y_{1},y_{2}\in Y$, (lhs)
$=w\cdot|kf_{1}(a)-kf_{2}(a)|\leq
w\cdot\max(d_{1}(x_{1},x_{2}),d_{2}(y_{1},y_{2}))=|(\tau_{a}\circ(2\times(\sigma_{\land}\circ
k_{1}\times
k_{2})^{\Sigma}))(t_{1},f_{1})-(\tau_{a}\circ(2\times(\sigma_{\land}\circ
k_{1}\times k_{2})^{\Sigma}))(t_{2},f_{2})|\leq$ (rhs) where
$f_{1}(a)=(x_{1},y_{1})$, $f_{2}(a)=(x_{2},y_{2})$, $k_{1}(t)\coloneqq
1-d_{1}(x_{1},t)$, $k_{2}(t)\coloneqq 1-d_{2}(x_{2},t)$.

∎

####  A.3.2 Similarity Pseudometric

######  Lemma A.5.

$\min(a,b)-\min(c,d)\leq\max(a-c,b-d)$ for each $a,b,c,d\in[0,1]$.

###### Proof.

If $a\leq b$ and $c\leq d$, (lhs) $=a-c\leq$ (rhs). If $a\geq b$ and $c\geq
d$, (lhs) $=b-d\leq$ (rhs). If $a\leq b$ and $c\geq d$, (lhs) $=a-d\leq
b-d\leq$(rhs). If $a\geq b$ and $c\leq d$, (lhs) $=b-c\leq a-c\leq$(rhs). ∎

######  Proposition A.6.

$d_{\mathbb{I}}^{\mathrm{as}}$ is a Lawvere metric.

###### Proof.

For each $a,b,c\in[0,1]$,

  * •

$d_{\mathbb{I}}^{\mathrm{as}}(a,a)=0$ is easy.

  * •

$d_{\mathbb{I}}^{\mathrm{as}}(a,c)\leq
d_{\mathbb{I}}^{\mathrm{as}}(a,b)+d_{\mathbb{I}}^{\mathrm{as}}(b,c)$ is
because: If $a\leq b$ and $b\leq c$, (lhs) $=c-a=$ (rhs). If $a\geq b$ and
$b\geq c$, (lhs) $=0=$ (rhs). If $a\leq b$ and $b\geq c$, $c-a\leq b-a=$ (rhs)
and $0\leq b-a=$ (rhs). If $a\geq b$ and $b\leq c$, $c-a\leq c-b=$ (rhs) and
$0\leq c-b=$ (rhs).

∎

######  Proposition A.7.

  1. 1.

The codensity lifting $[F,\tau]^{d_{\mathbb{I}}^{\mathrm{as}}}$ maps
$(X,d)\in\mathbf{LMet}$ to the pseudometric on $FX$ given by
$((t_{1},\rho_{1}),(t_{2},\rho_{2}))\mapsto
max\\{d_{\mathbb{I}}^{\mathrm{as}}(t_{1},t_{2}),w\cdot\max_{a\in\Sigma}d(\rho_{1}(a),\rho_{2}(a))\\}$.

  2. 2.

The binary codensity lifting
$[\times,\sigma_{\land}]^{d_{\mathbb{I}}^{\mathrm{as}}}$ maps
$(d_{1},d_{2})\in\mathbf{LMet}_{X}\times\mathbf{LMet}_{Y}$ to the Lawvere
metric on $X\times Y$ given by
$((x,y),(x^{\prime},y^{\prime}))\mapsto\max(d_{1}(x,x^{\prime}),d_{2}(y,y^{\prime}))$.

###### Proof.

  1. 1.

Fix arbitrary $d\in\mathbf{LMet}_{X}$ and
$(t_{1},\rho_{1}),(t_{2},\rho_{2})\in 2\times X^{\Sigma}$. It is easy to see
that
$[F,\tau_{\epsilon}]^{d_{\mathbb{I}}^{\mathrm{as}}}(d)((t_{1},\rho_{1}),(t_{2},\rho_{2}))=d_{\mathbb{I}}^{\mathrm{as}}(t_{1},t_{2})$.
Let us prove that
$[F,\tau_{a}]^{d_{\mathbb{I}}^{\mathrm{as}}}(d)((t_{1},\rho_{1}),(t_{2},\rho_{2}))=w\cdot
d(\rho_{1}(a),\rho_{2}(a))$ for each $a\in\Sigma$. ($\geq$): Letting
$k(t)\coloneqq d(\rho_{1}(a),t)$, $k\colon d\to d_{\mathbb{I}}^{\mathrm{as}}$
and (lhs) $\geq d_{\mathbb{I}}^{\mathrm{as}}(w\cdot k\rho_{1}(a),w\cdot
k\rho_{2}(a))=w\cdot d(\rho_{1}(a),\rho_{2}(a))=$ (rhs). ($\leq$): For each
$k\colon d\to d_{\mathbb{I}}^{\mathrm{as}}$,
$d_{\mathbb{I}}^{\mathrm{as}}(w\cdot k\rho_{1}(a),w\cdot k\rho_{2}(a))=w\cdot
d_{\mathbb{I}}^{\mathrm{as}}(k\rho_{1}(a),k\rho_{2}(a))\leq w\cdot
d(\rho_{1}(a),\rho_{2}(a))$. Therefore we have (lhs) $\leq$ (rhs).

  2. 2.

Fix arbitrary $d_{1},d_{2}\in\mathbf{LMet}_{X}$ and
$(x,y),(x^{\prime},y^{\prime})\in X\times Y$. Let us prove
$[\times,\sigma_{\land}]^{d_{\mathbb{I}}^{\mathrm{as}}}(d_{1},d_{2})((x,y),(x^{\prime},y^{\prime}))=\max(d_{1}(x,x^{\prime}),d_{2}(y,y^{\prime}))$.
$(\geq)$: Letting $k_{1}(t)\coloneqq 1-d_{1}(t,x^{\prime})$ and
$k_{2}(t)\coloneqq 1-d_{2}(t,y^{\prime})$, $k_{1}\colon d_{1}\to
d_{\mathbb{I}}^{\mathrm{as}}$ and $k_{2}\colon d_{2}\to
d_{\mathbb{I}}^{\mathrm{as}}$. Therefore we have (lhs) $\geq
d_{\mathbb{I}}^{\mathrm{as}}(\min(k_{1}x,k_{2}y),\min(k_{1}x^{\prime},k_{2}y^{\prime}))=\max(d_{1}(x,x^{\prime}),d_{2}(y,y^{\prime}))=$
(rhs). $(\leq)$: For each $k_{1}\colon d_{1}\to d_{\mathbb{I}}^{\mathrm{as}}$
and $k_{2}\colon d_{2}\to d_{\mathbb{I}}^{\mathrm{as}}$,
$d_{\mathbb{I}}^{\mathrm{as}}(\min(k_{1}x,k_{2}y),\min(k_{1}x^{\prime},k_{2}y^{\prime}))\leq\min(k_{1}x^{\prime},k_{2}y^{\prime})-\min(k_{1}x,k_{2}y)\leq\max(k_{1}x^{\prime}-k_{1}x,k_{2}y^{\prime}-k_{2}y)\leq\max(d_{1}(x,x^{\prime}),d_{2}(y,y^{\prime}))$
by Lemma A.5. Therefore we have (lhs) $\leq$ (rhs).

∎

######  Proposition A.8.

In the setting of §7.2, the tuple $((\Omega,\mathbf{\Omega})\colon
Id_{A}\to(p\colon\mathbf{LMet}\to\mathbf{Set}),(\times,\lambda^{\mathrm{da}}),\sigma_{\land})$
satisfies the conditions in Theorem 6.2.

###### Proof.

We can prove it in the same way as Proposition A.4. ∎

####  A.3.3 Bisimulation Metric

###### Proof of Lemma 7.4.

1) We can prove it by letting
$d\coloneqq[T,\sigma]^{\mathbf{\Omega}}(d_{1},d_{2})$ and $z\coloneqq\sigma$
in Lemma 7.5.

2) Let $P\in\mathbf{PMet}_{X}$ and $Q\in\mathbf{PMet}_{Y}$.
$[T,\sigma]^{\mathbf{\Omega}}([\mathcal{P},\inf]^{\mathbf{\Omega}}P,[\mathcal{P},\inf]^{\mathbf{\Omega}}Q)\sqsubseteq\lambda^{{\mathcal{P}}*}[\mathcal{P},\inf]^{\mathbf{\Omega}}[T,\sigma]^{\mathbf{\Omega}}(P,Q)$
is equivalent to for any
$A_{1},A_{2}\in\mathcal{P}X,B_{1},B_{2}\in\mathcal{P}Y$,

$\sigma(([\mathcal{P},\inf]^{\mathbf{\Omega}}P)(A_{1},A_{2}),([\mathcal{P},\inf]^{\mathbf{\Omega}}Q)(B_{1},B_{2}))\geq([\mathcal{P},\inf]^{\mathbf{\Omega}}[T,\sigma]^{\mathbf{\Omega}}(P,Q))(\lambda^{\mathcal{P}}(A_{1},B_{1}),\lambda^{\mathcal{P}}(A_{2},B_{2})).$
(9)

If
$\lambda^{\mathcal{P}}(A_{1},B_{1})=\lambda^{\mathcal{P}}(A_{2},B_{2})=\emptyset$,
then (rhs) $=0$ by the definition of $[\mathcal{P},\inf]^{\mathbf{\Omega}}$ so
the inequality (9) holds.

If $\lambda^{\mathcal{P}}(A_{1},B_{1})=\emptyset$ and
$\lambda^{\mathcal{P}}(A_{2},B_{2})\neq\emptyset$, then ($A_{1}=\emptyset$ or
$B_{1}=\emptyset$), $A_{2}\neq\emptyset$, and $B_{2}\neq\emptyset$ by
definition of $\lambda^{\mathcal{P}}$. Thus at least one of
$([\mathcal{P},\inf]^{\mathbf{\Omega}}P)(A_{1},A_{2})$ and
$([\mathcal{P},\inf]^{\mathbf{\Omega}}Q)(B_{1},B_{2})$ is equal to $1$ by the
definition of $[\mathcal{P},\inf]^{\mathbf{\Omega}}$. Because
$\sigma(1,a)=\sigma(a,1)=1$ for any $a\in[0,1]$, we have (lhs) $=1$. It
indicates the inequality (9) holds.

Assume that $\lambda^{\mathcal{P}}(A_{1},B_{1})\neq\emptyset$ and
$\lambda^{\mathcal{P}}(A_{2},B_{2})\neq\emptyset$. The definition of
$[\mathcal{P},\inf]^{\mathbf{\Omega}}$ gives that

$\displaystyle\text{(rhs)}=\max\bigl{(}$
$\displaystyle\sup_{(a_{1},b_{1})\in\lambda^{\mathcal{P}}(A_{1},B_{1})}\inf_{(a_{2},b_{2})\in\lambda^{\mathcal{P}}(A_{2},B_{2})}[T,\sigma]^{\mathbf{\Omega}}(P,Q)((a_{1},b_{1}),(a_{2},b_{2})),$
$\displaystyle\sup_{(a_{2},b_{2})\in\lambda^{\mathcal{P}}(A_{2},B_{2})}\inf_{(a_{1},b_{1})\in\lambda^{\mathcal{P}}(A_{1},B_{1})}[T,\sigma]^{\mathbf{\Omega}}(P,Q)((a_{1},b_{1}),(a_{2},b_{2}))\bigr{)}.$

Therefore it’s enough to show that two inequalities:

  * •

(lhs)
$\geq\sup_{(a_{1},b_{1})\in\lambda^{\mathcal{P}}(A_{1},B_{1})}\inf_{(a_{2},b_{2})\in\lambda^{\mathcal{P}}(A_{2},B_{2})}[T,\sigma]^{\mathbf{\Omega}}(P,Q)((a_{1},b_{1}),(a_{2},b_{2}))$,

  * •

(lhs)
$\geq\sup_{(a_{2},b_{2})\in\lambda^{\mathcal{P}}(A_{2},B_{2})}\inf_{(a_{1},b_{1})\in\lambda^{\mathcal{P}}(A_{1},B_{1})}[T,\sigma]^{\mathbf{\Omega}}(P,Q)((a_{1},b_{1}),(a_{2},b_{2}))$.

Let us show the former. The other one can be shown similarly.

For any $(a_{1},b_{1})\in\lambda^{\mathcal{P}}(A_{1},B_{1})$,

(lhs)
$\displaystyle=\sigma(([\mathcal{P},\inf]^{\mathbf{\Omega}}P)(A_{1},A_{2}),([\mathcal{P},\inf]^{\mathbf{\Omega}}Q)(B_{1},B_{2}))$
$\displaystyle\geq\sigma(\sup_{a_{1}^{\prime}\in A_{1}}\inf_{a_{2}^{\prime}\in
A_{2}}P(a_{1}^{\prime},a_{2}^{\prime}),\sup_{b_{1}^{\prime}\in
B_{1}}\inf_{b_{2}^{\prime}\in B_{2}}Q(b_{1}^{\prime},b_{2}^{\prime}))$ by the
definition of $[\mathcal{P},\inf]^{\mathbf{\Omega}}$
$\displaystyle\geq\sigma(\inf_{a_{2}^{\prime}\in
A_{2}}P(a_{1},a_{2}^{\prime}),\inf_{b_{2}^{\prime}\in
B_{2}}Q(b_{1},b_{2}^{\prime}))$ since $\sigma$ is monotone
$\displaystyle=\inf_{a_{2}^{\prime}\in A_{2},b_{2}^{\prime}\in
B_{2}}\sigma(P(a_{1},a_{2}^{\prime}),Q(b_{1},b_{2}^{\prime}))$ since $\sigma$
preserves infimums
$\displaystyle=\inf_{(a_{2}^{\prime},b_{2}^{\prime})\in\lambda^{\mathcal{P}}(A_{2},B_{2})}[T,\sigma]^{\mathbf{\Omega}}(P,Q)((a_{1},b_{1}),(a_{2}^{\prime},b_{2}^{\prime})).$

∎

###  A.4 Omitted Proofs for Section 8

######  Lemma A.9.

Assume that two conditions in Theorem 6.2 hold. A set
$\mathcal{V}\subseteq|\prod_{i\in N}\mathbb{E}_{X_{i}}|$ is an invariant for
$\mathbf{D}$ in the composite codensity game
$\mathcal{G}_{\overrightarrow{{c_{i}}}}^{T,\sigma}$ if and only if
$\bigsqcup_{\overrightarrow{{P_{i}}}\in\mathcal{V}}[T,\sigma]^{\mathbf{\Omega}}(\overrightarrow{{P_{i}}})\sqsubseteq({T}_{\lambda}(\overrightarrow{{c_{i}}}))^{*}[F,\tau]^{\mathbf{\Omega}}[T,\sigma]^{\mathbf{\Omega}}(\left({\bigsqcup_{\overrightarrow{{P_{i}}}\in\mathcal{V}}P_{i}}\right)_{i\in
N})$.

###### Proof.

$\displaystyle\lambda^{*}[F,\tau]^{\mathbf{\Omega}}[T,\sigma]^{\mathbf{\Omega}}$
$\displaystyle=\lambda^{*}R^{p,\mathbf{\Omega}}\circ\mathrm{Sp}^{A}(F,\tau)\circ\mathrm{Sp}^{A}(T,\sigma)\circ
L^{p^{N},\langle\mathbf{\Omega}\rangle_{N}}$ by the condition (2) in Theorem
6.2
$\displaystyle=R^{p,\mathbf{\Omega}}\circ\lambda^{*}\mathrm{Sp}^{A}(F,\tau)\circ\mathrm{Sp}^{A}(T,\sigma)\circ
L^{p^{N},\langle\mathbf{\Omega}\rangle_{N}}$ since $R^{p,\mathbf{\Omega}}$
preserves cartesian morphisms
$\displaystyle=R^{p,\mathbf{\Omega}}\circ\mathrm{Sp}^{A}(T,\sigma)\circ\mathrm{Sp}^{A}(F^{N},\tau^{N})\circ
L^{p^{N},\langle\mathbf{\Omega}\rangle_{N}}$ by the condition (1) in Theorem
6.2, and discussion after Theorem 6.2
$\displaystyle=R^{p,\mathbf{\Omega}}\circ\mathrm{Sp}^{A}(T\circ
F^{N},\sigma\mathbin{\bullet}(T\circ\tau^{N}))\circ
L^{p^{N},\langle\mathbf{\Omega}\rangle_{N}}.$

From this equation,

$\displaystyle\bigsqcup_{\langle P_{i}\rangle_{i\in
N}\in\mathcal{V}}[T,\sigma]^{\mathbf{\Omega}}(\langle P_{i}\rangle_{i\in
N})\sqsubseteq(\lambda\circ T(\langle c_{i}\rangle_{i\in
N}))^{*}[F,\tau]^{\mathbf{\Omega}}([T,\sigma]^{\mathbf{\Omega}}(\langle\bigsqcup_{\langle
P_{i}\rangle_{i\in N}\in\mathcal{V}}P_{i}\rangle_{i\in N}))$ if and only if
$\displaystyle\bigsqcup_{\langle P_{i}\rangle_{i\in
N}\in\mathcal{V}}[T,\sigma]^{\mathbf{\Omega}}(\langle P_{i}\rangle_{i\in