theoremTheorem lemma[theorem]Lemma proposition[theorem]Proposition
corollary[theorem]Corollary definition[theorem]Definition
example[theorem]Example remark[theorem]Remark Cornell University,
USAkd349@cornell.eduhttps://orcid.org/0000-0002-8812-9612 Universität
Duisburg-Essen<EMAIL_ADDRESS>well as Barbara König and
Paul Wild were supported by the Deutsche Forschungsgemeinschaft (DFG, German
Research Foundation) – project number 434050016 (SpeQt) University of
Copenhagen<EMAIL_ADDRESS>supported by NSF grant DMS-2216871
Universität Duisburg-Essen, Germanybarbara_koenig@uni-
due.dehttps://orcid.org/0000-0002-4193-2889 Amirkabir University of
Technology<EMAIL_ADDRESS>University College London,
UKw.rozowski@cs.ucl.ac.ukhttps://orcid.org/0000-0002-8241-7277partially
supported by ERC grant Autoprobe (no. 101002697) Friedrich-Alexander-
Universität Erlangen-Nürnberg,
Germanypaul.wild@fau.dehttps://orcid.org/0000-0001-9796-9675 Keri D’Angelo,
Sebastian Gurke, Johanna Maria Kirss, Barbara König, Matina Najafi, Wojciech
Różowski and Paul Wild <ccs2012> <concept>
<concept_id>10003752.10003753</concept_id> <concept_desc>Theory of computation
Models of computation</concept_desc>
<concept_significance>500</concept_significance> </concept> </ccs2012>
[500]Theory of computation Models of computation

# Behavioural Metrics: Compositionality of the Kantorovich Lifting and an
Application to Up-To Techniques

Keri D’Angelo  Sebastian Gurke  Johanna Maria Kirss  Barbara König  Matina
Najafi  Wojciech Różowski  Paul Wild

###### Abstract

Behavioural distances of transition systems modelled as coalgebras for
endofunctors generalize the traditional notions of behavioural equivalence to
a quantitative setting, in which states are equipped with a measure of how
(dis)similar they are. Endowing transition systems with such distances
essentially relies on the ability to lift functors describing the one-step
behavior of the transition systems to the category of pseudometric spaces. We
consider the Kantorovich lifting of a functor on quantale-valued relations,
which subsumes equivalences, preorders and (directed) metrics. We use tools
from fibred category theory, which allow one to see the Kantorovich lifting as
arising from an appropriate fibred adjunction. Our main contributions are
compositionality results for the Kantorovich lifting, where we show that that
the lifting of a composed functor coincides with the composition of the
liftings. In addition we describe how to lift distributive laws in the case
where one of the two functors is polynomial. These results are essential
ingredients for adopting up-to-techniques to the case of quantale-valued
behavioural distances. Up-to techniques are a well-known coinductive technique
for efficiently showing lower bounds for behavioural distances. We conclude by
illustrating the results of our paper in two case studies.

###### keywords:

behavioural metrics, coalgebra, Galois connections, quantales, Kantorovich
lifting, up-to techniques

##  1 Introduction

In concurrency theory, behavioural equivalences are a fundamental concept:
they explain whether two states exhibit the same behaviour and there are
efficient techniques for checking behavioural equivalence [s:bisimulation-
coinduction]. More recently, this idea has been generalized to behavioural
metrics that measure the behavioural distance of two states [bw:behavioural-
pseudometric, afs:linear-branching-metrics, dgjp:metrics-labelled-markov].
This is in particular interesting for quantitative systems where the behaviour
of two states might be similar but not identical.

There are two dimensions along which notions of behavioural distances for
(quantitative) transition systems can be generalized: first, instead of only
considering metrics that return a real-valued distance, one can use an
arbitrary quantale, yielding the notion of quantale-valued relations or
conformances that subsume equivalences, preorders and (directed) metrics.
Second, one can abstract from the branching type of the transition system
under consideration, using a functor specifying various forms of branching
(non-deterministic, probabilistic, weighted, etc.). This leads us to a
coalgebraic framework [r:universal-coalgebra] that provides several techniques
for studying and analyzing systems and has also been adapted to behavioural
metrics [bbkk:coalgebraic-behavioral-metrics]. A coalgebra is a function
$c\colon X\to FX$ where $X$ is a set of states and $F$ is a functor.

For defining (and computing) behavioural conformances in coalgebraic
generality, a fundamental notion is the lifting of a functor $F$ to
$\overline{F}$, acting on conformances. Given a set $X$ and a conformance $d$
(preorder, equivalence, metric, …) on $X$, the lifted functor $\overline{F}$
canonically determines a conformance on $FX$, based on a set of evaluation
maps. A subsequent reindexing with the coalgebra $c$ results in a function
whose (greatest) fixpoint is the desired behavioural conformance. In this
paper we focus on directed conformances such as preorders or directed metrics
(also called hemimetrics).

The aim of this paper is twofold: we consider the so-called Kantorovich
lifting of functors [bbkk:coalgebraic-behavioral-metrics] that – as opposed to
the Wasserstein lifting [bbkk:coalgebraic-behavioral-metrics] – has the
advantage of extra flexibility, since it allows the use of a set of evaluation
maps and places fewer restrictions on both the functor and these predicate
liftings [bbkk:coalgebraic-behavioral-metrics]. Then we study compositionality
results for the Kantorovich lifting, answering the question under which
conditions the lifting is compositional in the sense that
$\overline{FG}=\overline{F}\,\overline{G}$. This compositionality result is
then an essential ingredient in adapting up-to techniques to the setting of
behavioural metrics based on the Kantorovich lifting, inspired by the results
of [bkp:up-to-behavioural-metrics-fibrations-journal], which were developed
for the Wasserstein lifting. Up-to techniques are coinductive techniques that
allow small witnesses for lower bounds of behavioural distances by exploiting
an algebraic structure on the state space.

We first set up a framework based on Galois connections and fibred
adjunctions, extending [bgkmfsw:logics-coalgebra-adjunction]. This sets the
stage for the definition of the Kantorovich lifting based on this adjunction.
We next answer the question of compositionality positively for the case where
$F$ is polynomial, and show several negative results for combinations of
powerset and distribution functor.

The positive compositionality result for the case where $F$ is polynomial
opens the door to developing up-to techniques for trace-like behavioural
conformances that are computed on determinized transition systems, or – more
generally – determinized coalgebras. More concretely, we consider coalgebras
of type $c\colon X\to FTX$ where $F$ is a polynomial functor, providing the
explicit branching type of the coalgebra, and $T$ is a monad, describing the
implicit branching. For instance, in the case of a non-deterministic automaton
we would use $FX=2\times X^{A}$ and $T=\mathcal{P}$ (powerset functor). There
is a well-known determinization construction [jss:trace-determinization-
journal, sbbr:generalizing-determinization-journal] that transforms such a
coalgebra into $c^{\\#}\colon TX\to FTX$ via a distributive law $\zeta\colon
TF\Rightarrow FT$. This yields a determinized system $c^{\\#}$ acting on the
state space $TX$, which has an algebraic structure given by the multiplication
of the monad. On the other hand, $TX$ might be very large (e.g., in the case
of $T=\mathcal{P}$) or even infinite (e.g., in the case of $T=\mathcal{D}$,
distribution functor), making it hard to compute conformances for $c^{\\#}$.

However, the algebraic structure on $TX$ can be fruitfully employed using up-
to techniques [p:complete-lattices-up-to, bppr:general-coinduction-up-to] that
allow to consider post-fixpoints up to the algebraic structure, making it much
easier to display a witness proving a (lower) bound on the distance of two
states. The validity of the up-to technique rests on a compatibility property
that is ensured whenever the distributive law $\zeta$ can be lifted, i.e., if
it is non-expansive wrt. the lifted conformances. We show that this holds,
where an essential step in the proof relies on the compositionality results.

In this sense, we complement the up-to techniques in [bkp:up-to-behavioural-
metrics-fibrations-journal] that provide a similar result for the Wasserstein
lifting. This enables us to use the up-to technique for Kantorovich liftings
that allow more flexibility. The reason for this extra flexibility is that
they are based on a set of evaluation maps, rather than a single evaluation
map in the Wasserstein case, which leads to less fine-grained distances, in
particular in the presence of products and coproducts. Indeed, as can be seen
later in the paper, several case studies can only be treated appropriately in
the Kantorovich case. Furthermore, we can show the lifting of the distributive
law for an entire class of functors (polynomial functors), while [bkp:up-to-
behavioural-metrics-fibrations-journal] contained generic results for a
different class of canonical liftings. In the non-canonical case it was
necessary to prove a complex condition ensuring compositionality in [bkp:up-
to-behavioural-metrics-fibrations-journal].

We apply our technique to several examples, such as trace metrics for
probabilistic automata and trace semantics for systems with exceptions. We
give concrete instances where up-to techniques help and show how witnesses
yielding upper bounds can be reduced in size or even become finite (as opposed
to infinite).

##  2 Preliminaries

We begin by recalling some relevant definitions and fix some notation.

As outlined in the introduction, we use quantales as the domain for
behavioural conformances. A _quantale_ is a complete lattice
$(\mathcal{V},\sqsubseteq)$ that is equipped with a commutative monoid
structure $(\mathcal{V},\otimes,k)$ (where $k$ is the unit of $\otimes$) such
that $\otimes$ is _join-continuous_ , that is, $a\otimes\bigsqcup
b_{i}=\bigsqcup a\otimes b_{i}$ for each $a\in\mathcal{V}$ and each family
$b_{i}$ in $\mathcal{V}$, where $\bigsqcup$ denotes least upper bounds. Join-
continuity of $\otimes$ implies that the operation $a\otimes-$ has a right
adjoint, which we denote by $d_{\mathcal{V}}(a,-)$. This means that we have
$a\otimes b\sqsubseteq c\iff b\sqsubseteq d_{\mathcal{V}}(a,c)$ for all
$a,b,c\in\mathcal{V}$. The operation $d_{\mathcal{V}}$ is called the
_residuation_ or _internal hom_ of the quantale.

######  Lemma 2.1.

Residuation (internal hom) in a quantale satisfies the following properties
for $u,v,w,a,b,c,a_{i},b_{i}\in\mathcal{V}$:

  1. 1.

$d_{\mathcal{V}}(v,w)=\bigsqcup\\{u\in\mathcal{V}\mid u\otimes v\sqsubseteq
w\\}$

  2. 2.

$d_{\mathcal{V}}(v,v)\sqsupseteq k$ (reflexivity).

  3. 3.

$d_{\mathcal{V}}(u,v)\otimes d_{\mathcal{V}}(v,w)\sqsubseteq
d_{\mathcal{V}}(u,w)$ (triangle inequality).

  4. 4.

$d_{\mathcal{V}}(k,w)=w$.

  5. 5.

$d_{\mathcal{V}}(\bot,w)=\top$.

  6. 6.

$d_{\mathcal{V}}(v,\top)=\top$.

  7. 7.

$d_{\mathcal{V}}(\top,\bot)=\bot$.

  8. 8.

$d_{\mathcal{V}}(a,c)\sqsubseteq
d_{\mathcal{V}}(d_{\mathcal{V}}(b,a),d_{\mathcal{V}}(b,c))$

  9. 9.

$d_{\mathcal{V}}(a,c)\sqsubseteq
d_{\mathcal{V}}(d_{\mathcal{V}}(c,b),d_{\mathcal{V}}(a,b))$

  10. 10.

$\bigsqcap_{i\in I}d_{\mathcal{V}}(a_{i},b_{i})\sqsubseteq
d_{\mathcal{V}}(\bigsqcap_{i\in I}a_{i},\bigsqcap_{i\in I}b_{i})$

######  Proof 2.2.

  1. 1.

Residuation is the right adjoint of the associative operation $\otimes$.

  2. 2.

$d_{\mathcal{V}}(v,v)=\bigsqcup\\{u\in\mathcal{V}\mid u\otimes v\sqsubseteq
v\\}\sqsupseteq k$, since $k\otimes v=v\sqsubseteq v$.

  3. 3.

From $d_{\mathcal{V}}(v,w)\sqsubseteq d_{\mathcal{V}}(v,w)$ and the adjunction
property, we obtain $v\oplus d_{\mathcal{V}}(v,w)\sqsubseteq w$ and
analogously $u\oplus d_{\mathcal{V}}(u,v)\sqsubseteq v$. Hence $u\otimes
d_{\mathcal{V}}(u,v)\otimes d_{\mathcal{V}}(v,w)\sqsubseteq v\otimes\otimes
d_{\mathcal{V}}(v,w)\sqsubseteq w$. This implies $d_{\mathcal{V}}(u,v)\otimes
d_{\mathcal{V}}(v,w)\sqsubseteq d_{\mathcal{V}}(u,w)$.

  4. 4.

$d_{\mathcal{V}}(k,w)=\bigsqcup\\{u\in\mathcal{V}\mid u\otimes k\sqsubseteq
w\\}=\bigsqcup\\{u\in\mathcal{V}\mid u\sqsubseteq w\\}=w$.

  5. 5.

$d_{\mathcal{V}}(\bot,w)=\bigsqcup\\{u\in\mathcal{V}\mid
u\otimes\bot\sqsubseteq w\\}=\bigsqcup\\{u\in\mathcal{V}\mid\bot\sqsubseteq
w\\}=\bigsqcup\mathcal{V}=\top$. This holds, since $\bot$ is the empty join
and $\otimes$ preserves joins, hence $u\otimes\bot=\bot$.

  6. 6.

$d_{\mathcal{V}}(v,\top)=\bigsqcup\\{u\in\mathcal{V}\mid u\otimes
v\sqsubseteq\top\\}\bigsqcup\mathcal{V}=\top$.

  7. 7.

$d_{\mathcal{V}}(\top,\bot)=\bigsqcup\\{u\in\mathcal{V}\mid
u\otimes\top\sqsubseteq\bot\\}\sqsubseteq\bigsqcup\\{u\in\mathcal{V}\mid
u\otimes k\sqsubseteq\bot\\}=\\{u\in\mathcal{V}\mid u\sqsubseteq\bot\\}=\bot$,
where the inequality holds since $k\sqsubseteq\top$.

  8. 8.

Recall that the because of the definition of residuation, we have the
following property:

$d_{\mathcal{V}}(a,c)\sqsubseteq
d_{\mathcal{V}}\left(d_{\mathcal{V}}(b,a),d_{\mathcal{V}}(b,c)\right)\iff
d_{\mathcal{V}}(a,c)\otimes d_{\mathcal{V}}(b,a)\sqsubseteq
d_{\mathcal{V}}(b,c)$

Hence, it suffices to show the second inequality:

$\displaystyle d_{\mathcal{V}}(a,c)\otimes d_{\mathcal{V}}(b,a)$
$\displaystyle=d_{\mathcal{V}}(b,a)\otimes d_{\mathcal{V}}(a,c)$
$\displaystyle\sqsubseteq d_{\mathcal{V}}(b,c)$ (Triangle inequality, Lemma
2.1(3))

  9. 9.

Symmetric to (8)

  10. 10.

Because of the definition of the residuation, for all $i\in I$, we have that:

$d_{\mathcal{V}}(a_{i},b_{i})\sqsubseteq d_{\mathcal{V}}(a_{i},b_{i})\iff
d_{\mathcal{V}}(a_{i},b_{i})\otimes a_{i}\sqsubseteq b_{i}$

Therefore, we have that:

$\displaystyle\bigsqcap_{i\in I}b_{i}$
$\displaystyle\sqsupseteq\bigsqcap_{i\in I}d_{\mathcal{V}}(a_{i},b_{i})\otimes
a_{i}$ $\displaystyle\sqsupseteq\bigsqcap_{i\in
I}d_{\mathcal{V}}(a_{i},b_{i})\otimes\bigsqcap_{i\in I}a_{i}$

Again, by the definition of residuation the above is equivalent to
$\bigsqcap_{i\in I}d_{\mathcal{V}}(a_{i},b_{i})\sqsubseteq
d_{\mathcal{V}}(\bigsqcap_{i\in I}a_{i},\bigsqcap_{i\in I}b_{i})$ as desired,
which completes the proof.

We work with three main examples of quantales. The first is the _Boolean
quantale_ ${2_{\sqcap}}$, consisting of two elements $\bot\sqsubseteq\top$ and
with binary meet $\sqcap$ as the monoid structure. In this quantale, the unit
$k$ is $\top$, and residuation is Boolean implication:
$d_{\mathcal{V}}(a,b)=a\to b=\neg a\sqcup b$. The second main example is the
_unit interval quantale_ ${[0,1]_{\oplus}}$, where the underlying lattice is
the unit interval $[0,1]$ under the reversed order (that is,
${\sqsubseteq}={\geq}$), and with _truncated addition_ $a\oplus b=\min(a+b,1)$
as the monoid structure. In this case, the unit of $\oplus$ is $0$, and its
residuation is _truncated subtraction_ , which is given by
$d_{\mathcal{V}}(a,b)=b\ominus a=\max(b-a,0)$. The third main example is the
quantale ${[0,\infty]_{\oplus}}$ of _extended positive reals_ , with structure
analogous to ${[0,1]_{\oplus}}$, i.e. reversed lattice order and using
truncated addition as the monoid.

######  Remark 2.3.

As many of our examples use the real-valued quantales ${[0,1]_{\oplus}}$ and
${[0,\infty]_{\oplus}}$, where the order is reversed, we reserve the use of
the symbols $\geq$ and $\leq$ for the usual order in the reals, and instead
use $\sqsubseteq$ and $\sqsupseteq$ when working with general quantales.
Similarly, we use $\bigsqcup$ and $\bigsqcap$ for joins and meets in the
quantalic order, but switch to $\inf$ and $\sup$ when working in
${[0,1]_{\oplus}}$ or ${[0,\infty]_{\oplus}}$.

We consider several types of conformances based on a quantale $\mathcal{V}$.
First, given a set $X$, we may consider $\mathcal{V}$-valued endorelations on
$X$, that is, maps of type $d\colon X\times X\to\mathcal{V}$. We call these
structures _$\mathcal{V}$ -graphs_, and write
$\mathcal{V}\textrm{-}\mathsf{Graph}_{X}$ for the set of $\mathcal{V}$-graphs
with underlying set $X$. Each set $\mathcal{V}\textrm{-}\mathsf{Graph}_{X}$ is
a complete lattice where both the order and joins are pointwise, that is
$d\sqsubseteq d^{\prime}$ if $d(x,y)\sqsubseteq d^{\prime}(x,y)$ for all
$x,y\in X$ . Given two $\mathcal{V}$-graphs
$d_{X}\in\mathcal{V}\textrm{-}\mathsf{Graph}_{X}$ and
$d_{Y}\in\mathcal{V}\textrm{-}\mathsf{Graph}_{Y}$ we say that a map $f\colon
X\to Y$ is _non-expansive_ or a _$\mathcal{V}$ -functor_ if $d_{X}\sqsubseteq
d_{Y}\circ(f\times f)$ in $\mathcal{V}\textrm{-}\mathsf{Graph}_{X}$ and in
this case we write $f\colon(X,d_{X})\to(Y,d_{Y})$. $\mathcal{V}$-graphs and
non-expansive maps form a category $\mathcal{V}\textrm{-}\mathsf{Graph}$.

######  Remark 2.4.

In some parts of the literature, the category
$\mathcal{V}\textrm{-}\mathsf{Graph}$ is denoted by
$\mathcal{V}\textrm{-}\mathsf{Rel}$ instead [bkp:up-to-behavioural-metrics-
fibrations-journal]. We opt for $\mathcal{V}\textrm{-}\mathsf{Graph}$ as in
[Lawvere73], as $\mathcal{V}\textrm{-}\mathsf{Rel}$ more often denotes the
category with sets as objects and $\mathcal{V}$-valued relations between them
as morphisms [Hofmann07].

Second, within $\mathcal{V}\textrm{-}\mathsf{Graph}$ we consider the
subcategory consisting of those $\mathcal{V}$-graphs that satisfy additional
axioms, corresponding to a generalized notion of a metric space, or,
equivalently, (small) categories enriched over $\mathcal{V}$ [Lawvere73]. A
_$\mathcal{V}$ -category_ is an object of
$\mathcal{V}\textrm{-}\mathsf{Graph}_{X}$ for some set $X$ where we
additionally have $k\sqsubseteq d(x,x)$ and $d(x,y)\otimes d(y,z)\sqsubseteq
d(x,z)$ for all $x,y,z\in X$. Instantiated to the quantales ${2_{\sqcap}}$ and
${[0,1]_{\oplus}}$, $\mathcal{V}$-categories correspond precisely to
_preorders_ and _$1$ -bounded hemimetric spaces_, respectively. The quantale
$\mathcal{V}$ itself becomes a $\mathcal{V}$-category when equipped with the
residuation $d_{\mathcal{V}}$. The class of all $\mathcal{V}$-categories is
denoted by $\mathcal{V}\textrm{-}\mathsf{Cat}$, and the set of
$\mathcal{V}$-categories based on a set $X$ is denoted by
$\mathcal{V}\textrm{-}\mathsf{Cat}_{X}$.

In this paper, we use a coalgebraic framework. Recall a coalgebra is a pair
$(X,c)$, where $X$ is the state space and $c\colon X\to FX$ is the transition
structure parametric on an endofunctor $F\colon\mathsf{Set}\to\mathsf{Set}$.
We also utilize two specific functors for (counter)examples below. The
_powerset functor_ is defined as $\mathcal{P}(X)=\\{U\mid U\subseteq X\\}$ on
sets and $\mathcal{P}(f)(U)=\\{f(x)\mid x\in U\\}$ on functions. The
_countably supported distribution functor_ is defined as
$\mathcal{D}(X)=\left\\{p:X\to[0,1]\mid\sum_{x\in
X}p(x)=1,\textsf{supp}(p)\text{ is countable}\right\\}$ on sets, where
$\textsf{supp}(p)=\\{x\mid p(x)\neq 0\\}$, and as
$\mathcal{D}(f)(p)(y)=\sum\\{p(x)\mid x\in X,f(x)=y\\}$ on functions.

Given $f_{i}\colon X\to Y_{i}$, $i\in\\{1,2\\}$, we denote by $\langle
g_{1},g_{2}\rangle\colon X\to Y_{1}\times Y_{2}$ the mediating morphism of the
product, namely $\langle g_{1},g_{2}\rangle(x)=(g_{1}(x),g_{2}(x))$. Given
$g_{i}\colon X_{i}\to Y$, $i\in\\{1,2\\}$, $[g_{1},g_{2}]\colon X_{1}+X_{2}\to
Y$ is the mediating morphism of the coproduct, namely
$[g_{1},g_{2}](x)=g_{i}(x)$ if $x\in X_{i}$.

inline]P: What can we or do we need to say about symmetric distances?
inline]B: Check that all the constructions in the paper also work for
$\mathcal{V}\textrm{-}\mathsf{Graph}$, not just
$\mathcal{V}\textrm{-}\mathsf{Cat}$, or state restrictions accordingly.

##  3 Setting Up a Fibred Adjunction

One of the key aspects of this paper is equipping sets of states of coalgebras
with an extra structure of conformances (in particular preorders or
hemimetrics). The very idea of “extra structure” can be phrased formally
through the lenses of fibrations and fibred category theory, extending the
ideas of [bgkmfsw:logics-coalgebra-adjunction]. In particular, we show that
those results can be strengthened to the setting of fibred adjunctions.

inline]B: Say what is new compared to [bgkmfsw:logics-coalgebra-adjunction]

#### The category $\mathcal{V}\textrm{-}\mathsf{SPred}$.

The adjunction-based framework from [bgkmfsw:logics-coalgebra-adjunction],
besides working with $\mathcal{V}$-graphs, makes use of sets of
$\mathcal{V}$-valued predicates, i.e., maps of the form $p\colon
X\to\mathcal{V}$. We will use $\mathcal{V}\textrm{-}\mathsf{SPred}_{X}$ to
denote the collection of sets of $\mathcal{V}$-valued predicates over some set
$X$. A morphism between sets $S\subseteq\mathcal{V}^{X}$ and
$T\subseteq\mathcal{V}^{Y}$ is a function $f\colon X\to Y$ satisfying
$f^{\bullet}(T):=\\{q\circ f\mid q\in T\\}\subseteq S$, where $f^{\bullet}$
describes reindexing. We obtain a category
$\mathcal{V}\textrm{-}\mathsf{SPred}$ with objects being pairs
$(X,S\subseteq\mathcal{V}^{X})$ and arrows are defined as above.

#### Grothendieck completion.

It turns out that both
$\mathcal{V}\textrm{-}\mathsf{Graph}/\mathcal{V}\textrm{-}\mathsf{Cat}$ and
$\mathcal{V}\textrm{-}\mathsf{SPred}$ can be viewed as fibred categories
[Lawvere73, bkp:up-to-behavioural-metrics-fibrations-journal]. We here only
consider fibred categories arising from the Grothendieck construction, which
can be viewed equivalently as a special kind of split indexed categories, that
in our case are functors $A:\mathsf{Set}^{\text{op}}\to\mathsf{Pos}$.
Intuitively, such functors assign to each set a poset of “extra structure” and
take functions $f:X\to Y$ to monotone maps canonically reindexing the “extra
structure” on set $Y$ by $f$.

The _Grothendieck completion_ [j:categorical-logic-type-theory] of a functor
$A\colon\mathsf{Set}^{\text{op}}\to\mathsf{Pos}$ is a category denoted $\int
A$, whose objects are pairs $(X,i)$ where $X\in\mathsf{Set}$ and $i\in A(X)$.
The arrows $(X,i)\to(Y,j)$ are maps $f\colon X\to Y$ such that $i\sqsubseteq
A(f)(j)$, where $\sqsubseteq$ is the partial order on $A(X)$. The
corresponding fibration is given by the forgetful functor $U\colon\int
A\to\mathsf{Set}$ taking each pair $(X,i)$ to its underlying set $X$. The
fibre of each set $X$ is corresponds to the poset $A(X)$.

####  $\mathcal{V}\textrm{-}\mathsf{Graph}/\mathcal{V}\textrm{-}\mathsf{Cat}$
and $\mathcal{V}\textrm{-}\mathsf{SPred}$ as Grothendieck completions.

The category $\mathcal{V}\textrm{-}\mathsf{Graph}$ arises as the Grothendieck
completion of the functor $\Phi:\mathsf{Set}^{\text{op}}\to\mathsf{Pos}$ that
takes each set $X$ to
$\Phi(X)=(\mathcal{V}\textrm{-}\mathsf{Graph}_{X},\sqsubseteq)$, the lattice
of $\mathcal{V}$-valued relations equipped with a pointwise order
$\sqsubseteq$. Given a function $f\colon X\to Y$, we define $\Phi(f)=f^{*}$ by
reindexing, where $f^{*}(d_{Y})=d_{Y}\circ(f\times f)$.

Similarly, to obtain $\mathcal{V}\textrm{-}\mathsf{SPred}$, we define a
functor $\Psi:\mathsf{Set}^{\text{op}}\to\mathsf{Pos}$ that maps each set $X$
to $\Psi(X)=(\mathcal{V}\textrm{-}\mathsf{SPred}_{X},\supseteq)$, the lattice
of collections of $\mathcal{V}$-valued predicates on $X$ ordered by reverse
inclusion. Furthermore $\Psi(f)=f^{\bullet}$.

######  Lemma 3.1.

$\mathcal{V}\textrm{-}\mathsf{Graph}=\int\Phi$ and
$\mathcal{V}\textrm{-}\mathsf{SPred}=\int\Psi$.

######  Proof 3.2.

The objects of $\int\Phi$ are pairs $(X,d_{X})$, where $X$ is a set and
$d_{X}$ is an element of the lattice $\mathcal{V}\textrm{-}\mathsf{Graph}_{X}$
of $\mathcal{V}$-valued relations. The arrows $f\colon(X,d_{X})\to(Y,d_{Y})$
are functions $f\colon X\to Y$, which satisfy $d_{X}\sqsubseteq f^{*}(d_{Y})$,
which is the same as $d_{X}\sqsubseteq d_{Y}\circ(f\times f)$. This precisely
corresponds to the definition of the $\mathcal{V}\textrm{-}\mathsf{Graph}$
category.

Similarly, the objects of $\int\Psi$ are pairs $(X,S)$, where $X$ is a set and
$S\in\mathcal{V}\textrm{-}\mathsf{SPred}_{X}$ (and hence
$S\subseteq\mathcal{V}^{X}$) is the element of the lattice of subsets of
$\mathcal{V}^{X}$ ordered by reverse inclusion. The arrows $(X,S)\to(Y,T)$ are
functions $f\colon X\to Y$, such that $S\supseteq f^{\bullet}(T)$, which is
the same as $\\{q\circ f\mid q\in T\\}\subseteq S$. Again this precisely
corresponds to the definition of $\mathcal{V}\textrm{-}\mathsf{SPred}$
category.

Additionally, observe that if we were to restrict $\Phi$ to send each set $X$
to the lattice $(\mathcal{V}\textrm{-}\mathsf{Cat}_{X},\sqsubseteq)$ of
$\mathcal{V}$-categories on $X$, which is a sublattice of
$(\mathcal{V}\textrm{-}\mathsf{Graph}_{X},\sqsubseteq)$ of all
$\mathcal{V}$-graphs, then the Grothendieck completion would yield
$\mathcal{V}\textrm{-}\mathsf{Cat}$ instead of
$\mathcal{V}\textrm{-}\mathsf{Graph}$.

#### Galois connection on the fibres.

In the adjunction-based framework from [bgkmfsw:logics-coalgebra-adjunction],
the Kantorovich lifting of a functor is phrased through the means of a
contravariant Galois connection between the fibres of
$\mathcal{V}\textrm{-}\mathsf{Cat}$ and $\mathcal{V}\textrm{-}\mathsf{SPred}$
and we here generalize from $\mathcal{V}\textrm{-}\mathsf{Cat}$ to
$\mathcal{V}\textrm{-}\mathsf{Graph}$. For each set $X$, we define a map
$\alpha_{X}\colon\mathcal{V}\textrm{-}\mathsf{SPred}_{X}\to\mathcal{V}\textrm{-}\mathsf{Graph}_{X}$
given by:

$\alpha_{X}(S)(x_{1},x_{2})=\bigsqcap\nolimits_{f\in
S}d_{\mathcal{V}}(f(x_{1}),f(x_{2}))\qquad(S\subseteq\mathcal{V}^{X})$

Intuitively, $\alpha_{X}$ takes a collection $S$ of $\mathcal{V}$-valued
predicates on $X$ and generates the greatest conformance on $X$ that turns all
predicates into non-expansive maps. For the other part of the Galois
connection, we have a map
$\gamma_{X}\colon\mathcal{V}\textrm{-}\mathsf{Graph}_{X}\to\mathcal{V}\textrm{-}\mathsf{SPred}_{X}$
defined by the following:

$\gamma_{X}(d_{X})=\\{f\colon X\to\mathcal{V}\mid d_{\mathcal{V}}\circ(f\times
f)\sqsupseteq d_{X}\\}$

Given a conformance $d_{X}\colon X\times X\to\mathcal{V}$, $\gamma_{X}$
generates a set of $\mathcal{V}$-valued predicates on $X$ which are non-
expansive maps from $d_{X}$ to the residuation distance. As mentioned before,
we can instantiate the previous result [bgkmfsw:logics-coalgebra-adjunction,
Theorem 7] and obtain the following:

######  Theorem 3.3 ([bgkmfsw:logics-coalgebra-adjunction]).

Let $X$ be an arbitrary set, $d_{X}\colon X\times X\to\mathcal{V}$ a
$\mathcal{V}$-graph and $S\subseteq\mathcal{V}^{X}$ a collection of
$\mathcal{V}$-valued predicates. Then $\alpha_{X}$ and $\gamma_{X}$ are both
antitone (in $\subseteq$, $\sqsubseteq$) and form a contravariant Galois
connection:

$d_{X}\sqsubseteq\alpha_{X}(S)\iff S\subseteq\gamma_{X}(d_{X}).$

#### Fibred Adjunction.

Theorem 3.3 is a “local” property that only holds fiberwise. However, it turns
out that we can argue something stronger, namely that we have a fibred
adjunction situation. This is a “global” property, as fibred functors
additionally preserve the notion of reindexing. Note that every natural
transformation between functors of type
$\mathsf{Set}^{\text{op}}\to\mathsf{Pos}$ (a so-called morphisms of split
indexed categories) [j:categorical-logic-type-theory, Definition 1.10.5]
induces a fibred functor between the corresponding Grothendieck completions.

One can quite easily verify that $\alpha$ is natural on
$\mathcal{V}\textrm{-}\mathsf{Graph}$, while $\gamma$ is only laxly natural on
$\mathcal{V}\textrm{-}\mathsf{Graph}$ and natural on
$\mathcal{V}\textrm{-}\mathsf{Cat}$. For the latter result, we rely on a
quantalic version of the McShane-Whitney extension theorem
[McS:ExtensionOfFunctions, W:ExtensionOfFunctions], mentioned also in
[Lawvere73] for the real-valued case.

######  Lemma 3.4.

$\alpha\colon\Psi\Rightarrow\Phi$ is natural.

######  Proof 3.5.

Let $f\colon X\to Y$ be an arbitrary function. We need to check the
commutativity of the following diagram in $\mathsf{Pos}$:

${{\Psi(Y)}}$${{\Psi(X)}}$${{\Phi(Y)}}$${{\Phi(X)}}$$\scriptstyle{\alpha_{X}}$$\scriptstyle{\alpha_{Y}}$$\scriptstyle{f^{\bullet}}$$\scriptstyle{f^{*}}$

Note that as a consequence of Theorem 3.3, we have that for all sets $X$ and
all $S,S^{\prime}\in\mathcal{V}\textrm{-}\mathsf{SPred}_{X}$, we have
antitonicity of $\alpha_{X}$ and hence $\alpha_{X}$ is a monotone map from the
lattice of sets of predicates with inverse inclusion order to the lattice of
$\mathcal{V}$-valued relations. It suffices to check $\alpha_{X}\circ
f^{\bullet}=f^{*}\circ\alpha_{Y}$. Let $T\subseteq\mathcal{V}^{Y}$ and
$x_{1},x_{2}\in X$ and consider the following:

$\displaystyle(\alpha_{X}\circ f^{\bullet})(T)(x_{1},x_{2})$
$\displaystyle=\bigsqcap_{p\in T}d_{\mathcal{V}}((p\circ f)(x_{1}),(p\circ
f)(x_{2}))$ $\displaystyle=\alpha_{Y}(T)(f(x_{1}),f(x_{2}))$
$\displaystyle=(f^{*}\circ\alpha_{Y}(T))(x_{1},x_{2})$

Unfortunately, in the case of $\gamma$, without any extra assumptions, we can
only prove a weaker statement, namely that it is laxly natural.

######  Lemma 3.6.

$\gamma\colon\Phi\Rightarrow\Psi$ is laxly natural, that is for all functions
$f\colon X\to Y$ and all $\mathcal{V}$-valued relations $d_{Y}$ on the set $Y$
we have that $(f^{\bullet}\circ\gamma_{Y})(d_{Y})\subseteq(\gamma_{X}\circ
f^{*})(d_{Y})$.

######  Proof 3.7.

Observing that $\gamma_{X}$ is antitone, we can show that for all sets $X$,
$\gamma_{X}$ is a monotone function from the lattice of $\mathcal{V}$-valued
relations to the lattice of collections of $\mathcal{V}$-valued predicates
(ordered by reverse inclusion order). The only thing we need to show is that
for all functions $f\colon X\to Y$, we have that
$(f^{\bullet}\circ\gamma_{Y})(d_{Y})\subseteq(\gamma_{X}\circ f^{*})(d_{Y})$
for all $\mathcal{V}$-valued relations $d_{Y}$ on the set $Y$.

Assume that $p\colon X\to\mathcal{V}$ belongs to
$(f^{\bullet}\circ\gamma_{Y})(d_{Y})$. In other words, $p=q\circ f$ for some
$q\colon Y\to\mathcal{V}$, such that $d_{\mathcal{V}}\circ(q\times
q)\sqsupseteq d_{Y}$. Observe that pre-composing $f\times f$ yields the
inequality $d_{\mathcal{V}}\circ((q\circ f)\times(q\circ f))\sqsupseteq
d_{Y}\circ(f\times f)$ and therefore $d_{\mathcal{V}}\circ(p\times
p)\sqsupseteq d_{Y}\circ(f\times f)=f^{*}(d_{Y})$. Hence,
$p\in(\gamma_{X}\circ f^{*})(d_{X})$, which completes the proof.

To obtain the converse inclusion, we need to be able to factorise any
$\mathcal{V}$-valued predicate on $X$, which is non-expansive with respect to
$f^{*}(d_{Y})$ as the composition of $f$ and a $\mathcal{V}$-valued predicate
on $Y$ which is non-expansive with respect to $d_{Y}$. Since $f$ can be seen
as isometry between $(X,f^{*}(d_{Y}))$ and $(Y,d_{Y})$, we are essentially
focusing on extending a non-expansive map into a residuation metric through an
isometry, which in the case of pseudometric spaces can be proved through the
McShane-Whitney extension Theorem. It turns out that those results can be
generalised to the setting of $\mathcal{V}$-categories.

[Quantalic McShane-Whitney Extension Theorem] Let $\mathcal{V}$ be a quantale
and $(X,d)$ be an object of $\mathcal{V}\textrm{-}\mathsf{Cat}$. For any
subset $Y\subseteq X$ and any non-expansive map
$f\colon(Y,d)\to(\mathcal{V},d_{\mathcal{V}})$ there is a non-expansive
extension $\bar{f}\colon(X,d)\to(\mathcal{V},d_{\mathcal{V}})$ of $f$.

######  Proof 3.8.

Define for every element $y\in Y$ a function $g_{y}\colon X\to\mathcal{V}$ by

$g_{y}(x)=d_{\mathcal{V}}(d(x,y),f(y))$

Note that all the functions $g_{y}$ are non-expansive, since for
$x_{1},x_{2}\in X$ we have $d(x_{1},x_{2})\otimes d(x_{2},y)\sqsubseteq
d(x_{1},y)$ (triangle inequality) and hence

$\displaystyle d(x_{1},x_{2})$ $\displaystyle\sqsubseteq
d_{\mathcal{V}}(d(x_{2},y),d(x_{1},y))$ $\displaystyle\sqsubseteq
d_{\mathcal{V}}(d_{\mathcal{V}}(d(x_{1},y),f(y)),d_{\mathcal{V}}(d(x_{2},y),f(y)))$
(Lemma 2.1(9)) $\displaystyle=d_{\mathcal{V}}(g_{y}(x_{1}),g_{y}(x_{2})).$

Now define $\bar{f}\colon X\to\mathcal{V}$ by

$\bar{f}(x)=\bigsqcap_{y\in Y}g_{y}(x)=\bigsqcap_{y\in
Y}d_{\mathcal{V}}(d(x,y),f(y))$

Once can easily verify that $\bar{f}$ is also non-expansive, because

$\displaystyle d_{\mathcal{V}}(\bar{f}(x_{1}),\bar{f}(x_{2}))$
$\displaystyle=d_{\mathcal{V}}\Big{(}\bigsqcap_{y\in
Y}g_{y}(x_{1}),\bigsqcap_{y\in Y}g_{y}(x_{2})\Big{)}$
$\displaystyle\sqsupseteq\bigsqcap_{y\in
Y}d_{\mathcal{V}}(g_{y}(x_{1}),g_{y}(x_{2}))$ (Lemma 2.1(9))
$\displaystyle\sqsupseteq\bigsqcap_{y\in Y}d(x_{1},x_{2})=d(x_{1},x_{2})$

It remains to show that $\bar{f}(y)=f(y)$ for all $y\in Y$. Consider $z\in Y$,
then from the antitonicity of $d_{\mathcal{V}}$ in its first argument and
Lemma 2.1(4):

$\bar{f}(z)\sqsubseteq d_{\mathcal{V}}(d(z,z),f(z))\sqsubseteq
d_{\mathcal{V}}(k,f(z))=f(z)$

On the other hand, by the nonexpansivity of $f$, for all $y\in Y$ we have by
commutativity:

$\displaystyle d_{\mathcal{V}}(f(z),f(y))\sqsupseteq d(z,y)$
$\displaystyle\iff d(z,y)\otimes f(z)\sqsubseteq f(y)$ $\displaystyle\iff
d_{\mathcal{V}}(d(z,y),f(y))\sqsupseteq f(z)$

And therefore

$\bar{f}(z)=\bigsqcap_{y\in Y}d_{\mathcal{V}}(d(z,y),f(y))\sqsupseteq f(z)$

######  Remark 3.9.

Note that the function $\bar{f}$ constructed in the proof is the largest non-
expansive extension of $f$. That means for all non-expansive extensions
$h\colon(X,d)\to(\mathcal{V},d_{\mathcal{V}})$ of $f$ we have
$h\sqsubseteq\bar{f}$. For if $h$ is another non-expansive extension of $f$,
then for all $x\in X$ and all $y\in Y$ we have

$\displaystyle
d_{\mathcal{V}}(h(x),f(y))=d_{\mathcal{V}}(h(x),h(y))\sqsupseteq d(x,y)$
$\displaystyle\iff h(x)\otimes d(x,y)\sqsubseteq f(y)$ $\displaystyle\iff
h(x)\sqsubseteq d_{\mathcal{V}}(d(x,y),f(y))$

and therefore

$h(x)\sqsubseteq\bigsqcap_{y\in Y}d_{\mathcal{V}}(d(x,y),f(y))=\bar{f}(x).$

Similarly, the function $g\colon X\to\mathcal{V}$ defined by

$g(x)=\bigsqcup_{y\in Y}f(y)\otimes d(y,x)$

is the smallest non-expansive function extending $f$.

As a corollary, we obtain the desired property needed to show the converse
inclusion.

Let $d_{X}\in\mathcal{V}\textrm{-}\mathsf{Cat}_{X}$ and
$d_{Y}\in\mathcal{V}\textrm{-}\mathsf{Cat}_{Y}$ be elements of
$\mathcal{V}\textrm{-}\mathsf{Cat}$. If $i\colon(Y,d_{Y})\to(X,d_{X})$ is an
isometry, then for any non-expansive map
$f\colon(Y,d_{Y})\to(\mathcal{V},d_{\mathcal{V}})$ there exists a non-
expansive map $g\colon(X,d_{X})\to(\mathcal{V},d_{\mathcal{V}})$ such that
$f=g\circ i$.

######  Proof 3.10.

The function $i\colon Y\to X$ can be factorised as the composition of $e\colon
Y\to i[Y]$, where $i[Y]$ denotes the image of $Y$ under $i$ and $m\colon
i[Y]\to X$, where $m$ is the canonical inclusion function of $i[Y]$ into $X$.
We can equip $i[Y]$ with a distance $d_{i[Y]}\colon i[Y]\times
i[Y]\to\mathcal{V}$ defined to be the restriction of $d_{X}$ to the domain
$i[Y]\times i[Y]$. One can observe that $(i[Y],d_{i[Y]})$ is also an element
of $\mathcal{V}\textrm{-}\mathsf{Cat}$ and that
$m\colon(Y,d_{Y})\to(i[Y],d_{i[Y]})$ is an isometry as a consequence of $i$
being an isometry.

We define a function $h\colon i[Y]\to\mathcal{V}$ to be given by
$h(e(y))=f(y)$. We now argue that $h$ is well-defined. Let $y_{1},y_{2}\in Y$,
such that $e(y_{1})=e(y_{2})$. Since
$f\colon(Y,d_{Y})\to(\mathcal{V},d_{\mathcal{V}})$ is non-expansive, we have
that:

$d_{\mathcal{V}}(f(y_{1}),f(y_{2}))\sqsupseteq
d_{Y}(y_{1},y_{2})=d_{i[Y]}(e(y_{1}),e(y_{2}))\sqsupseteq k$

The second to last step relies on the fact that $d_{i[Y]}$ is reflexive. By
the definition of $d_{\mathcal{V}}$ we have that the above inequality is
equivalent to

$k\otimes f(y_{1})\sqsubseteq f(y_{2})\iff f(y_{1})\sqsubseteq f(y_{2})$

The second step above relies on the fact that $k$ is the unit of $\otimes$.
The argument that $f(y_{2})\sqsubseteq f(y_{1})$ is symmetric and therefore
omitted.

We now argue that $h\colon(i[Y],d_{i[Y]})\to(\mathcal{V},d_{\mathcal{V}})$ is
non-expansive. Let $x_{1},x_{2}\in i[Y]$. Since $e$ is surjective, there must
exist $y_{1},y_{2}$ with $e(y_{1})=x_{1}$ and $e(y_{2})=x_{2}$.

$\displaystyle d_{\mathcal{V}}(h(x_{1}),h(x_{2}))$
$\displaystyle=d_{\mathcal{V}}(h(e(y_{1})),h(e(y_{2})))$ ($e$ is surjective)
$\displaystyle=d_{\mathcal{V}}(f(y_{1}),f(y_{2}))$ (Def. of $h$)
$\displaystyle\sqsupseteq d_{Y}(y_{1},y_{2})$ ($f$ is non-expansive)
$\displaystyle=d_{i[Y]}(e(y_{1}),e(y_{2}))$ ($e$ is an isometry)
$\displaystyle=d_{i[Y]}(x_{1},x_{2})$

We can sum up the situation as the commuting diagram in
$\mathcal{V}\textrm{-}\mathsf{Cat}$.

${{(Y,d_{Y})}}$${{(i[Y],d_{i[Y]})}}$${{(\mathcal{V},d_{\mathcal{V}})}}$${{(X,d_{X})}}$$\scriptstyle{e}$$\scriptstyle{m}$$\scriptstyle{h}$$\scriptstyle{f}$$\scriptstyle{g}$

The upper triangle commutes by the definition of $h$, while $g$ exists and
makes the bottom one commute because of 3.7. Since $i=m\circ e$, we have that
there exists non-expansive $g$, such that $g\circ i=f$, which completes the
proof.

Note, that the property above does not hold for arbitrary $\mathcal{V}$-graphs
and only works for $\mathcal{V}$-categories. To make use of that, we restrict
$\Phi(X)$ to be the lattice
$(\mathcal{V}\textrm{-}\mathsf{Cat}_{X},\sqsubseteq)$ of
$\mathcal{V}$-categories on $X$.

######  Lemma 3.11.

When restricted to $\mathcal{V}\textrm{-}\mathsf{Cat}$,
$\gamma\colon\Phi\to\Psi$ is natural.

######  Proof 3.12.

It suffices to show the converse inclusion to the one argued in Lemma 3.6. Let
$p\colon X\to\mathcal{V}$ be an arbitrary $\mathcal{V}$-valued predicate on
$X$, such that $d_{Y}\circ(f\times f)\sqsubseteq d_{\mathcal{V}}\circ(p\times
p)$. We want to show that there exists a non-expansive map
$q\colon(Y,d_{Y})\to(\mathcal{V},d_{\mathcal{V}})$, such that $p=q\circ f$.
Observe that $p\colon X\to\mathcal{V}$ is a non-expansive map from
$(X,d_{Y}\circ(f\times f))$ to $(\mathcal{V},d_{\mathcal{V}})$ and
$f\colon(Y,d_{Y}\circ(f\times f))\to(Y,d_{Y})$ is an isometry.

${{(X,d_{Y}\circ(f\times
f))}}$${{(Y,d_{Y})}}$${{(\mathcal{V},d_{\mathcal{V}})}}$$\scriptstyle{f}$$\scriptstyle{\exists
q}$$\scriptstyle{p}$

We can use Section 3 and conclude that there exists a non-expansive function
$q\colon(Y,d_{Y})\to(\mathcal{V},d_{\mathcal{V}})$ such that $p=q\circ f$.
Hence, $p\in(f^{\bullet}\circ\gamma_{Y})(d_{Y})$, which completes the proof.

We have that $\alpha\colon\Psi\Rightarrow\Phi$ is natural and
$\gamma\colon\Phi\Rightarrow\Psi$ is laxly natural, that is for all functions
$f\colon X\to Y$ and all $\mathcal{V}$-valued relations $d_{Y}$ on the set $Y$
we have that $(f^{\bullet}\circ\gamma_{Y})(d_{Y})\subseteq(\gamma_{X}\circ
f^{*})(d_{Y})$. When restricted to $\mathcal{V}\textrm{-}\mathsf{Cat}$,
$\gamma\colon\Phi\Rightarrow\Psi$ is natural.

######  Proof 3.13.

Follows from Lemmas 3.4, 3.6 and 3.11.

Note that we can safely make this restriction, while still keeping $\alpha$ to
be well-defined, as its image always lies within
$\mathcal{V}\textrm{-}\mathsf{Cat}$.

######  Lemma 3.14.

For all sets $X$ and collections of predicates $S\subseteq\mathcal{V}^{X}$,
$\alpha_{X}(S)$ is a $\mathcal{V}$-category.

######  Proof 3.15.

Let $x\in X$. For reflexivity, we have that for all $p\in S$,
$d_{\mathcal{V}}(p(x),p(x))\sqsupseteq k$ and hence

$\alpha_{X}(S)(x,x)=\bigsqcap_{p\in S}d_{\mathcal{V}}(p(x),p(x))\sqsupseteq k$

For transitivity, let $x_{1},x_{2}\in X$. We have to show the following for
all $z\in X$:

$\alpha_{X}(S)(x_{1},z)\otimes\alpha_{X}(S)(z,x_{2})\sqsubseteq\alpha_{X}(S)(x_{1},x_{2})=\bigsqcap_{p\in
S}d_{\mathcal{V}}(p(x_{1}),p(x_{2}))$

To show the above, it is enough to argue that for all $p\in S$, we have that
$\alpha_{X}(S)(x_{1},z)\otimes\alpha_{X}(z,x_{2})\sqsubseteq
d_{\mathcal{V}}(p(x_{1}),p(x_{2}))$. We have the following:

$\displaystyle\alpha_{X}(S)(x_{1},z)\otimes\alpha_{X}(S)(z,x_{2})$
$\displaystyle=\left(\bigsqcap_{r\in
S}d_{\mathcal{V}}(r(x_{1}),r(z))\right)\otimes\left(\bigsqcap_{r\in
S}d_{\mathcal{V}}(r(z),r(x_{2}))\right)$
$\displaystyle\sqsubseteq\bigsqcap_{r\in
S}d_{\mathcal{V}}(r(x_{1}),r(z))\otimes d_{\mathcal{V}}(r(z),r(x_{2}))$
($\left(\bigsqcap_{i\in I}a_{i}\right)\otimes\left(\bigsqcap_{i\in
I}b_{i}\right)\sqsubseteq\bigsqcap_{i\in I}a_{i}\otimes b_{i}$)
$\displaystyle\sqsubseteq\bigsqcap_{r\in S}d_{\mathcal{V}}(r(x_{1}),r(x_{2}))$
($d_{\mathcal{V}}$ is transitive, Lemma 2.1(3)) $\displaystyle\sqsubseteq
d_{\mathcal{V}}(p(x_{1}),p(x_{2}))$ ($p\in S$)

which completes the proof.

Additionally, when restricting our attention to
$\mathcal{V}\textrm{-}\mathsf{Cat}$ (instead of all
$\mathcal{V}\textrm{-}\mathsf{Graph}$), it turns out that the co-closure
operator of the Galois connection (Theorem 3.3) becomes an identity.

######  Lemma 3.16.

The co-closure $\alpha_{X}\circ\gamma_{X}$ is the identity, when restricted to
$\mathcal{V}\textrm{-}\mathsf{Cat}$.

######  Proof 3.17.

Let $(X,d_{X})$ be an object of $\mathcal{V}\textrm{-}\mathsf{Cat}$. The
inequality $d_{X}\sqsubseteq(\alpha_{X}\circ\gamma_{X})(X,d_{X})$ holds
immediately because of Theorem 3.3. For the other direction, we will have to
show that for all $x_{1},x_{2}\in X$, we have that
$d_{X}(x_{1},x_{2})\sqsupseteq(\alpha_{X}\circ\gamma_{X})(X,d_{X})(x_{1},x_{2})$.
To observe that, we define a function $p\colon X\to\mathcal{V}$ given by
$p(x)=d_{X}(x_{1},x)$. First, recall that for all $x_{1},x_{2}\in X$

$\alpha_{X}(\gamma_{X}(d_{X}))(x_{1},x_{2})=\bigsqcap_{\begin{subarray}{c}p\colon
X\to\mathcal{V}\\\ d_{X}\sqsubseteq d_{\mathcal{V}}\circ(p\times
p)\end{subarray}}d_{\mathcal{V}}(p(x_{1}),p(x_{2}))$

We show that it is non-expansive with respect to $d_{\mathcal{V}}$

$\displaystyle d_{\mathcal{V}}(p(x_{1}),p(x_{2}))$
$\displaystyle=d_{\mathcal{V}}(d_{X}(x_{1},x_{1}),d_{X}(x_{1},x_{2}))$
$\displaystyle\sqsubseteq d_{\mathcal{V}}(k,d_{X}(x_{1},x_{2}))$ (Anttonicity
of $d_{\mathcal{V}}(-,-)$ in the first argument)
$\displaystyle=d_{X}(x_{1},x_{2})$ ($x=d_{\mathcal{V}}(k,x)$, Lemma 2.1(5))

Hence

$\alpha_{X}(\gamma_{X}(d_{X}))(x_{1},x_{2})\sqsubseteq
d_{\mathcal{V}}(p(x_{1}),p(x_{2}))\sqsubseteq d_{X}(x_{1},x_{2})$

For all sets $X$ and $S\subseteq\mathcal{V}^{X}$, $\alpha_{X}(S)$ is a
$\mathcal{V}$-category, i.e., an object of
$\mathcal{V}\textrm{-}\mathsf{Cat}$. The co-closure
$\alpha_{X}\circ\gamma_{X}$ is the identity, when restricted to
$\mathcal{V}\textrm{-}\mathsf{Cat}$. Combined, this implies that for
$d\in\mathcal{V}\textrm{-}\mathsf{Graph}_{X}$, $\alpha_{X}(\gamma_{X}(d))$ is
the metric closure of $d$, i.e., the least element of
$\mathcal{V}\textrm{-}\mathsf{Cat}_{X}$ above $d$.

######  Proof 3.18.

The first two statements follow from Lemmas 3.16 and 3.14.

Now let $d\in\mathcal{V}\textrm{-}\mathsf{Graph}_{X}$,
$d^{\prime}\in\mathcal{V}\textrm{-}\mathsf{Cat}_{X}$ with $d\sqsubseteq
d^{\prime}$. By antitonicity of $\alpha$, $\gamma$ it holds that
$\alpha_{X}(\gamma_{X}(d))\sqsubseteq\alpha_{X}(\gamma_{X}(d^{\prime}))=d^{\prime}$.
Furthermore $\alpha_{X}(\gamma_{X}(d))$ is a $\mathcal{V}$-category, which
implies the statement.

Because of the Grothendieck construction ([j:categorical-logic-type-theory,
Theorem 1.10.7]), $\alpha$ and $\gamma$ respectively correspond to fibred
functors
$\alpha\colon\mathcal{V}\textrm{-}\mathsf{SPred}\to\mathcal{V}\textrm{-}\mathsf{Cat}$
and
$\gamma:\mathcal{V}\textrm{-}\mathsf{Cat}\to\mathcal{V}\textrm{-}\mathsf{SPred}$.
Both functors keep morphisms unchanged and act on objects by respectively
applying the appropriate components of $\alpha$ and $\gamma$. Now, we can
state the strengthened version of Theorem 3.3, by showing that $\alpha$ and
$\gamma$ form a fibred adjunction. Note that due to the choice of the
orderings, $\gamma$ becomes the left and $\alpha$ the right adjoint (cf.
[kwrk:composing-codensity-bisimulations]). There is an adjunction
$\gamma\dashv\alpha$.

######  Proof 3.19.

Let $d_{X}\in\mathcal{V}\textrm{-}\mathsf{Cat}_{x}$ be an arbitrary reflexive
and transive $\mathcal{V}$-valued relation on $X$, $T\subseteq\mathcal{V}^{Y}$
and $f\colon X\to Y$ a non-expansive map from $(X,d_{X})$ to
$(Y,\alpha_{Y}(T))$. We will define a non-expansive map
$\eta_{d_{X}}\colon(X,d_{X})\to(X,\alpha_{X}(\gamma_{X}(d_{X})))$ and show
that there exists a unique arrow $g\colon\gamma_{X}(d_{X})\to T$ which makes
the following diagram commute.

${{(X,d_{X})}}$${(X,\alpha_{X}(\gamma_{X}(d_{X})))}$${{(Y,\alpha_{Y}(T))}}$$\scriptstyle{f}$$\scriptstyle{\eta_{d_{X}}}$$\scriptstyle{\alpha(g)}$

First, we set $\eta_{d_{X}}=\mathrm{id}$ to be the identity map. In order to
show that it is non-expansive, we need to argue that
$d_{X}\sqsubseteq\alpha_{X}(\gamma_{X}(d_{X}))=\alpha_{X}(\gamma_{X}(d_{X}))$.
This immediately follows from Theorem 3.3, where we have shown that
$\alpha_{X}$ and $\gamma_{X}$ form a contravariant Galois connection.

Recall that $\alpha(g)=g$ and hence the diagram above would uniquely commute
if we set $g=f$. The only remaining thing is to argue that $f$ is a morphism
in $\mathcal{V}\textrm{-}\mathsf{SPred}$ between $(X,\gamma_{X}(d_{X}))$ and
$(Y,T)$. In other words, we need to prove that:

$f^{\bullet}(T)=\\{q\circ f\mid q\in T\\}\subseteq\gamma_{X}(d_{X})=\\{p\colon
X\to\mathcal{V}\mid d_{X}\sqsubseteq d_{\mathcal{V}}\circ(p\times p)\\}$

Because $f\colon(X,d_{X})\to\alpha_{X}(T)$ is non-expansive, we have that for
all $x_{1},x_{2}\in X$:

$d_{X}(x_{1},x_{2})\sqsubseteq\bigsqcap_{q\in
T}d_{\mathcal{V}}(q(f(x_{1})),q(f(x_{2})))$

and therefore for any $q\in T$, we have that:

$d_{X}(x_{1},x_{2})\sqsubseteq d_{\mathcal{V}}((q\circ f)(x_{1}),(q\circ
f)(x_{2}))$

Observe that because of the inequality above every element of $f^{\bullet}(T)$
also belongs to $\gamma_{X}(d_{X})$, which completes the proof.

##  4 The Kantorovich Lifting

###  4.1 Definition of Kantorovich Lifting

Motivated by the transportation problem [v:optimal-transport], the Kantorovich
distance on probability distributions aims to maximize the relative logistics
profit by finding the optimal flow of commodities that satisfies demand from
supplies and minimizes the flow cost. In fact, it is based on the dual version
of this problem that asks for the optimal price function.

The coalgebraic Kantorovich lifting [bbkk:coalgebraic-behavioral-metrics] –
also known as codensity lifting [ks:codensity-liftings-monads] – is parametric
in a set of _evaluation functions_ for a set functor $F$. Evaluation functions
are used to lift $\mathcal{V}$-valued predicates on a set $X$ to
$\mathcal{V}$-valued predicates on the set $FX$. More precisely, given an
evaluation function $\mathit{ev}\colon F\mathcal{V}\to\mathcal{V}$ and a
predicate $f\colon X\to\mathcal{V}$ we obtain the predicate $\mathit{ev}\circ
Ff\colon FX\to\mathcal{V}$. This operation extends to sets of evaluation
functions and sets of $\mathcal{V}$-valued predicates, where a set
$\Lambda^{F}$ of evaluation functions for $F$ induces the fibred functor
$\Lambda^{F}\colon\mathcal{V}\textrm{-}\mathsf{SPred}\to\mathcal{V}\textrm{-}\mathsf{SPred}$,
defined on $S\subseteq\mathcal{V}^{X}$ as follows:

$\Lambda^{F}_{X}(S)=\\{\mathit{ev}\circ Ff\mid\mathit{ev}\in\Lambda^{F},f\in
S\\}\subseteq\mathcal{V}^{FX}.$

The Kantorovich lifting can now be restated via the fibred adjunction
introduced previously. Given $F$ and $\Lambda^{F}$ as above, we can define its
Kantorovich lifting $K_{\Lambda^{F}}$ as follows:

$K_{\Lambda^{F}}=\alpha{F}\circ\Lambda^{F}\circ\gamma$

or more concretely, for an object $d_{X}$ of
$\mathcal{V}\textrm{-}\mathsf{Graph}$ and $s,t\in FX$:

$K_{\Lambda^{F}}(d_{X})(s,t)=\bigsqcap\nolimits_{\mathit{ev}\in\Lambda^{F}}\bigsqcap\nolimits_{f\in\gamma_{X}(d_{X})}d_{\mathcal{V}}(\mathit{ev}(Ff(s)),\mathit{ev}(Ff(t))).$

If the set $\Lambda^{F}$ is clear from the context we sometimes write
$\overline{F}$ instead of $K_{\Lambda^{F}}$. The Kantorovich lifting of a
functor $F:\mathsf{Set}\to\mathsf{Set}$ is a functor
$\overline{F}=K_{\Lambda^{F}}\colon\mathcal{V}\textrm{-}\mathsf{Graph}\to\mathcal{V}\textrm{-}\mathsf{Graph}$,
and fibred when restricted to $\mathcal{V}\textrm{-}\mathsf{Cat}$.

######  Proof 4.1.

We need to show that for an arbitrary non-expansive function
$f\colon(X,d_{X})\to(Y,d_{X})$, $Ff$ becomes non-expansive function between
$\overline{F}(X,d_{X})$ and $\overline{F}(Y,d_{Y})$. In other words, we
require that:

$(\alpha_{FX}\circ\Lambda_{X}^{F}\circ\gamma_{X})(d_{X})\sqsubseteq(\alpha_{FY}\circ\Lambda_{Y}^{F}\circ\gamma_{Y})(d_{Y})\circ(Ff\times
Ff)$

First, we simplify the right-hand side:

$\displaystyle\left((\alpha_{FY}\circ\Lambda_{Y}^{F}\circ\gamma_{Y})(d_{Y})\circ(Ff\times
Ff)\right)$ $\displaystyle=$
$\displaystyle\left((\alpha_{FY}\circ\Lambda_{Y}^{F}\circ\gamma_{Y}(d_{Y}))\circ(Ff\times
Ff)\right)$ $\displaystyle=$
$\displaystyle\left(Ff^{*}\circ\alpha_{FY}\circ\Lambda_{Y}^{F}\circ\gamma_{Y}(d_{Y})\right)$
(Definition of $(-)^{*}$) $\displaystyle=$
$\displaystyle\left(\alpha_{FX}\circ(Ff)^{\bullet}\circ\Lambda_{Y}^{F}\circ\gamma_{Y}(d_{Y})\right)$
($\alpha$ is natural) $\displaystyle=$
$\displaystyle\left(\alpha_{FX}\circ\Lambda_{Z}^{F}\circ
f^{\bullet}\circ\gamma_{Y}(d_{Y})\right)$

Hence, we have the following:

$(\alpha_{FX}\circ\Lambda_{X}^{F}\circ\gamma_{X})(d_{X})\sqsubseteq\left(\alpha_{FX}\circ\Lambda_{X}^{F}\circ
f^{\bullet}\circ\gamma_{Y}(d_{Y})\right)$

Since $\alpha_{FX}$ is antitone (Theorem 3.3), it suffices to argue the
following:

$(\Lambda_{X}^{F}\circ\gamma_{X})(d_{X})\supseteq(\Lambda_{X}^{F}\circ
f^{\bullet}\circ\gamma_{Y})(d_{Y})$

Because of the lax naturality of $\gamma$ (Lemma 3.6), we simplify the above
even further:

$(\Lambda_{X}^{F}\circ\gamma_{X})(d_{X})\supseteq(\Lambda_{X}^{F}\circ\gamma_{X}\circ
f^{*})(d_{Y})$

Since it is not hard to see that $\Lambda_{X}^{F}$ is monotone, we are left
with proving:

$\gamma_{Y}(d_{Y}\circ(f\times f))\subseteq\gamma_{X}(d_{X})$

Let $p\in\gamma_{X}(d_{Y}\circ(f\times f))$. In other words, for all
$x_{1},x_{2}\in X$ we have that

$d_{\mathcal{V}}(p(x_{1}),p(x_{2}))\sqsupseteq d_{Y}(f(x_{1}),f(x_{2}))$

Combining the above with the fact that $f$ is non-expansive function from
$(X,d_{X})$ to $(Y,d_{Y})$, we obtain that
$d_{\mathcal{V}}(p(x_{1}),p(x_{2}))\sqsupseteq d_{X}(x_{1},x_{2})$ and
therefore $p\in\gamma_{X}(d_{X})$, thus showing functoriality.

For fibredness, consider a function $f:X\to Y$ in $\mathsf{Set}$, and an
object $(Y,d_{Y})$ in $\mathcal{V}\textrm{-}\mathsf{Cat}$. We wish to see that
for all $s,t\in FX$

$K_{\Lambda^{F}}(d_{Y}\circ(f\times
f))(s,t)=K_{\Lambda^{F}}(d_{Y})\circ(Ff\times Ff)(s,t)$

This is equivalent to

$\displaystyle\bigsqcap_{\mathit{ev}\in\Lambda^{F}}\bigsqcap_{p\in\gamma_{X}(d_{Y}\circ(f\times
f))}d_{\mathcal{V}}(\mathit{ev}(Fp(s)),\mathit{ev}(Fp(t)))$ $\displaystyle=$
$\displaystyle\bigsqcap_{\mathit{ev}\in\Lambda^{F}}\bigsqcap_{q\in\gamma_{Y}(d_{Y})}d_{\mathcal{V}}(\mathit{ev}(Fq(Ff(s))),\mathit{ev}(Fq(Ff(t))))$

and since in the category $\mathcal{V}\textrm{-}\mathsf{Cat}$, we have that
$(f^{\bullet}\circ\gamma_{Y})(d_{Y})=(\gamma_{X}\circ f^{*})(d_{Y})$, then the
above equality holds, completing the proof.

###  4.2 Compositionality of the Kantorovich Lifting

When an endofunctor is given as the composition of two or more individual set
functors, it is natural to ask under which conditions its Kantorovich lifting
is also the composition of Kantorovich liftings of the respective functors.
Specifically, our aim in this section is to identify situations where this
composition happens already at the level of the underlying sets of evaluation
maps. If $\mathit{ev}_{F}$ is an evaluation function for $F$ and
$\mathit{ev}_{G}$ is an evaluation function for $G$, then an evaluation
function for $FG$ is given by
$\mathit{ev}_{F}*\mathit{ev}_{G}:=\mathit{ev}_{F}\circ F\mathit{ev}_{G}$.
Extending this to sets of evaluation functions, we put
$\Lambda^{F}*\Lambda^{G}=\\{\mathit{ev}_{F}*\mathit{ev}_{G}\mid\mathit{ev}_{F}\in\Lambda^{F},\mathit{ev}_{G}\in\Lambda^{G}\\}$
for sets $\Lambda^{F}$ and $\Lambda^{G}$ of evaluation functions for functors
$F$ and $G$, respectively.

######  Definition 4.2 (Compositionality).

Given two functors $F$ and $G$ and sets $\Lambda^{F}$ and $\Lambda^{G}$ of
evaluation functions, we say that we have _compositionality_ if
$K_{\Lambda^{F}}\circ K_{\Lambda^{G}}=K_{\Lambda^{F}*\Lambda^{G}}.$

Expanding definitions, compositionality amounts to showing that

$K_{\Lambda^{F}}\circ K_{\Lambda^{G}}=\alpha FG\circ\Lambda^{F}\circ\gamma
G\circ\alpha G\circ\Lambda^{G}\circ\gamma=\alpha
FG\circ\Lambda^{F}\circ\Lambda^{G}\circ\gamma=K_{\Lambda^{F}*\Lambda^{G}}.$
(1)

One inequality (‘$\sqsubseteq$’) always holds. As $\alpha$ and $\gamma$ form a
Galois connection [bgkmfsw:logics-coalgebra-adjunction], we have
$\mathrm{id}_{\mathcal{V}\textrm{-}\mathsf{SPred}_{X}}\subseteq\gamma_{GX}\circ\alpha_{GX}$,
and thus we may use antitonicity of $\alpha$ to deduce ‘$\sqsubseteq$’ in (1).
Baldan et al. [bbkk:coalgebraic-behavioral-metrics, Lemma 7.5] prove this for
the special case of pseudometric liftings.

The other inequality, ‘$\sqsupseteq$’, does not hold in general, and requires
more work. Still, one notices that a sufficient condition is that
$\Lambda^{F}\circ\gamma\circ\alpha\subseteq\gamma{F}\circ\alpha{F}\circ\Lambda^{F}$:

$\displaystyle K_{\Lambda^{F}}\circ K_{\Lambda^{G}}$ $\displaystyle=$
$\displaystyle\alpha{FG}\circ\Lambda^{F}\circ\alpha{G}\circ\gamma{G}\circ\Lambda^{G}\circ\gamma$
$\displaystyle\sqsupseteq$
$\displaystyle\alpha{FG}\circ\gamma{FG}\circ\alpha{FG}\circ\Lambda^{F}\circ\Lambda^{G}\circ\gamma=\alpha
FG\circ\Lambda^{FG}\circ\gamma=K_{\Lambda^{F}*\Lambda^{G}},$

using that $\alpha\circ\gamma\circ\alpha=\alpha$ for every Galois connection.
Note that it is enough to prove the sufficient condition on non-empty sets,
since $\gamma$ always yields a non-empty set.

Before discussing the problem of systematically constructing sets of
evaluation functions such that $\Lambda^{F}\circ c\subseteq c\circ\Lambda^{F}$
holds, we consider a few examples where compositionality fails:

######  Example 4.3.

Consider the powerset functor $\mathcal{P}$ with the predicate lifting $\sup$
($\Lambda^{\mathcal{P}}=\\{\sup\\}$), and the discrete distribution functor
$\mathcal{D}$ with the predicate lifting $\mathbb{E}$ that takes expected
values ($\Lambda^{\mathcal{D}}=\\{\mathbb{E}\\}$). With just these predicate
liftings, compositionality fails for all four combinations
$\mathcal{P}\mathcal{P}$, $\mathcal{P}\mathcal{D}$, $\mathcal{D}\mathcal{P}$,
$\mathcal{D}\mathcal{D}$. We show this for the case of
$\mathcal{P}\mathcal{D}$ and discuss the others in the appendix (Example 4.4).
Let $X$ be the two-element set $\\{x,y\\}$, equipped with the discrete metric
$d$ (that is, $d(x,y)=d(y,x)=1$), so that in particular all maps $g\colon
X\to[0,1]$ are non-expansive. We also consider the non-expansive function
$f_{\mathcal{D}}\colon{(\mathcal{D}X,K_{\\{\mathbb{E}\\}}d)}\to{([0,1],d_{[0,1]_{\oplus}})}$
given by $f_{\mathcal{D}}(p\cdot x+(1-p)\cdot y)=\min(p,1-p).$ Put
$U=\\{1\cdot x,1\cdot y\\}$ and $V={\\{1\cdot x,\nicefrac{{1}}{{2}}\cdot
x+\nicefrac{{1}}{{2}}\cdot y,1\cdot y\\}}$. Then $\sup
f_{\mathcal{D}}[U]=\max(0,0)=0$ and $\sup
f_{\mathcal{D}}[V]=\max(0,\nicefrac{{1}}{{2}},0)=\nicefrac{{1}}{{2}},$ so that
$K_{\\{\sup\\}}(K_{\\{\mathbb{E}\\}}d)(U,V)\geq\nicefrac{{1}}{{2}}$. For every
$g\colon X\to[0,1]$ one finds that

$\displaystyle(\sup*\mathbb{E})(g)(U)$
$\displaystyle=\max(g(x),g(y))=\textstyle\max(g(x),\nicefrac{{g(x)+g(y)}}{{2}},g(y))=(\sup*\mathbb{E})(g)(V),$

implying that $K_{\\{\sup*\mathbb{E}\\}}d(U,V)=0$.

######  Example 4.4.

Consider the powerset functor $\mathcal{P}$ with the predicate lifting $\sup$,
and the discrete distribution functor $\mathcal{D}$ with the predicate lifting
$\mathbb{E}$ that takes expected values. With just these predicate liftings,
compositionality fails for all four combinations $\mathcal{P}\mathcal{P}$,
$\mathcal{P}\mathcal{D}$, $\mathcal{D}\mathcal{P}$, $\mathcal{D}\mathcal{D}$.
In all cases, let $X$ be the two-element set $\\{x,y\\}$, equipped with the
discrete metric $d$ (that is, $d(x,y)=d(y,x)=1$), so that in particular all
maps $g\colon X\to[0,1]$ are non-expansive. We also consider the following two
non-expansive functions on $\mathcal{P}X$ respectively $\mathcal{D}X$:

$\displaystyle
f_{\mathcal{P}}\colon{(\mathcal{P}X,K_{\\{\sup\\}}d)}\to{([0,1],d_{[0,1]_{\oplus}})}$
$\displaystyle
f_{\mathcal{D}}\colon{(\mathcal{D}X,K_{\\{\mathbb{E}\\}}d)}\to{([0,1],d_{[0,1]_{\oplus}})}$
$\displaystyle f_{\mathcal{P}}(A)=\begin{cases}1,&\text{if $A=\\{x,y\\}$}\\\
0,&\text{otherwise}\\\ \end{cases}$ $\displaystyle f_{\mathcal{D}}(p\cdot
x+(1-p)\cdot y)=\min(p,1-p)$

To see that $f_{\mathcal{P}}$ is indeed non-expansive, note that for
$B\subseteq A$ we have $f_{\mathcal{P}}(B)\ominus
f_{\mathcal{P}}(A)=0=K_{\\{\sup\\}}d(A,B)$ by monotonocity of
$f_{\mathcal{P}}$ and $\sup$, and for $B\nsubseteq A$ we have
$K_{\\{\sup\\}}d(A,B)=1$ as we may pick $g$ to be the characteristic function
of some $z\in B\setminus A$. In $\mathcal{D}X$, the distance of $\mu=p\cdot
x+(1-p)\cdot y$ and $\nu=q\cdot x+(1-q)\cdot y$ can be computed as

$K_{\\{\mathbb{E}\\}}d(\mu,\nu)=\sup\\{(q\cdot a+(1-q)\cdot b)-(p\cdot
a+(1-p)\cdot b)\mid a,b\in[0,1]\\}=|q-p|,$

so that $f_{\mathcal{D}}$ is easily seen to be non-expansive as well.

  1. 1.

Put $U=\\{\\{x\\},\\{y\\}\\}$ and $V=\\{\\{x\\},\\{y\\},\\{x,y\\}\\}$. Then

$\sup f_{\mathcal{P}}[U]=0\quad\text{and}\quad\sup f_{\mathcal{P}}[V]=1,$

so that $K_{\\{\sup\\}}(K_{\\{\sup\\}}d)(U,V)=1$. For every $g\colon
X\to[0,1]$ one finds that

$(\sup*\sup)(g)(U)=\max(g(x),g(y))=(\sup*\sup)(g)(V),$

implying that $K_{\\{\sup*\sup\\}}d(U,V)=0$.

  2. 2.

Put $U=\\{1\cdot x,1\cdot y\\}$ and $V=\\{1\cdot x,\nicefrac{{1}}{{2}}\cdot
x+\nicefrac{{1}}{{2}}\cdot y,1\cdot y\\}$. Then

$\textstyle\sup f_{\mathcal{D}}[U]=\max(0,0)=0\quad\text{and}\quad\sup
f_{\mathcal{D}}[V]=\max(0,\nicefrac{{1}}{{2}},0)=\nicefrac{{1}}{{2}},$

so that $K_{\\{\sup\\}}(K_{\\{\mathbb{E}\\}}d)(U,V)\geq\nicefrac{{1}}{{2}}$.
For every $g\colon X\to[0,1]$ one finds that

$\displaystyle(\sup*\mathbb{E})(g)(U)$
$\displaystyle=\max(g(x),g(y))=\textstyle\max(g(x),\nicefrac{{g(x)+g(y)}}{{2}},g(y))=(\sup*\mathbb{E})(g)(V),$

implying that $K_{\\{\sup*\mathbb{E}\\}}(d)(U,V)=0$.

  3. 3.

Put $\mu=\nicefrac{{1}}{{2}}\cdot\\{x\\}+\nicefrac{{1}}{{2}}\cdot\\{y\\}$ and
$\nu=1\cdot\\{x,y\\}$. Then

$\textstyle\mathbb{E}_{\mu}(f_{\mathcal{P}})=\nicefrac{{1}}{{2}}\cdot
0+\nicefrac{{1}}{{2}}\cdot
0=0\quad\text{and}\quad\mathbb{E}_{\nu}(f_{\mathcal{P}})=1\cdot 1=1,$

so that $K_{\\{\mathbb{E}\\}}(K_{\\{\sup\\}}d)(U,V)=1$. For every $g\colon
X\to[0,1]$ one finds that

$\textstyle(\mathbb{E}*\sup)(g)(\mu)=\nicefrac{{g(x)+g(y)}}{{2}}\quad\text{and}\quad(\mathbb{E}*\sup)(g)(\nu)=\max(g(x),g(y)),$

implying that $K_{\\{\mathbb{E}*\sup\\}}(d)(\mu,\nu)\leq\nicefrac{{1}}{{2}}$.

  4. 4.

Put $\mu=\nicefrac{{1}}{{2}}\cdot(1\cdot x)+\nicefrac{{1}}{{2}}\cdot(1\cdot
y)$ and $\nu=1\cdot(\nicefrac{{1}}{{2}}\cdot x+\nicefrac{{1}}{{2}}\cdot y)$.
Then

$\textstyle\mathbb{E}_{\mu}(f_{\mathcal{D}})=0\quad\text{and}\quad\mathbb{E}_{\nu}(f_{\mathcal{D}})=\nicefrac{{1}}{{2}},$

so that
$K_{\\{\mathbb{E}\\}}(K_{\\{\mathbb{E}\\}}d)(U,V)\geq\nicefrac{{1}}{{2}}$. For
every $g\colon X\to[0,1]$ one finds that

$\textstyle(\mathbb{E}*\mathbb{E})(g)(\mu)=\nicefrac{{g(x)+g(y)}}{{2}}=(\mathbb{E}*\mathbb{E})(g)(\nu),$

implying that $K_{\\{\mathbb{E}*\mathbb{E}\\}}(d)(\mu,\nu)=0$.

###  4.3 Polynomial Functors

We now assume that the first functor ($F$ with the lifting
$\overline{F}=K_{\Lambda_{F}}$) is in fact a polynomial functor and we show
that in this case compositionality holds automatically for certain sets of
predefined evaluation maps. This will later allow us to use compositionality
to define up-to techniques for large classes of coalgebras that are based on
such functors.

Consider the set of polynomial functors given by

$F\Coloneqq C_{B}\mid\mathrm{Id}\mid\textstyle\prod_{i\in I}F_{i}\mid
F_{1}+F_{2}$

where $C_{B}$ is the constant functor mapping to some set $B$ and
$\mathrm{Id}$ is the identity functor. We support products over arbitrary
index sets, but we restrict to finitary coproducts for simplicity.

For polynomial functors we can obtain compositionality in a structured manner,
by constructing suitable sets of predicate liftings alongside with the
functors themselves. We recursively define a set $\Lambda^{F}$ of evaluation
functions for each polynomial functor $F$ as follows:

constant functors:

$F=C_{B}$. Here we choose $\Lambda^{F}$ to be any set of maps of type
$B\to\mathcal{V}$. (For instance, when $B=\mathcal{V}$ we can put
$\Lambda^{F}=\\{\mathrm{id}_{\mathcal{V}}\\}$.)

identity functor:

$F=\mathrm{Id}$. We put $\Lambda^{F}=\\{\mathrm{id}_{\mathcal{V}}\\}$.

product functors:

$F=\textstyle\prod_{i\in I}F_{i}$. Let
$\Lambda^{F}=\\{\mathit{ev}_{i}\circ\pi^{\prime}_{i}\mid i\in
I,\mathit{ev}_{i}\in\Lambda^{F_{i}}\\}$ where
$\pi^{\prime}_{i}\colon\textstyle\prod_{i\in I}F_{i}\mathcal{V}\to
F_{i}\mathcal{V}$ are the projections.

coproduct functors:

$F=F_{1}+F_{2}$. We put
$\Lambda^{F}=\\{[\mathit{ev}_{1},\top]\mid\mathit{ev}_{1}\in\Lambda^{F_{1}}\\}\cup\\{[\bot,\mathit{ev}_{2}]\mid\mathit{ev}_{2}\in\Lambda^{F_{2}}\\}\cup\\{[\bot,\top]\\},$
where $\top$ and $\bot$ denote constant maps into $\mathcal{V}$.

######  Remark 4.5.

We note that the construction for coproduct functors is associative, that is,
for functors $F_{1}$, $F_{2}$ and $F_{3}$ the sets
$\Lambda^{(F_{1}+F_{2})+F_{3}}$ and $\Lambda^{F_{1}+(F_{2}+F_{3})}$ coincide
up to isomorphism.

Note also that the exponentiation $F^{A}X=(FX)^{A}$ is special case of the
product where $I=A$ and $F_{i}=F$ for all $i\in I$.

The choice of evaluation maps above induces the following liftings, leading to
the natural expected distances in the directed case.

Given a polynomial functor $F$ and a set of evaluation maps $\Lambda^{F}$ as
defined above, the corresponding lifting $\overline{F}=K_{\Lambda^{F}}$ is
defined as follows on objects of $\mathcal{V}\textrm{-}\mathsf{Graph}$:
$\overline{F}(d_{X})=d^{F}_{X}\colon FX\times FX\to\mathcal{V}$ where

constant functors:

$d^{F}_{X}\colon B\times B\to\mathcal{V}$,
$d^{F}_{X}(b,c)=\bigsqcap_{\mathit{ev}\in\Lambda^{F}}d_{\mathcal{V}}(\mathit{ev}(b),\mathit{ev}(c))$.

identity functor:

$d^{F}_{X}\colon X\times X\to\mathcal{V}$ with
$d^{F}_{X}=\alpha_{X}(\gamma_{X}(d))$.

product functors:

$d^{F}_{X}\colon\textstyle\prod_{i\in I}F_{i}X\times\textstyle\prod_{i\in
I}F_{i}X\to\mathcal{V}$, $d^{F}_{X}(s,t)=\bigsqcap_{i\in
I}d_{X}^{F_{i}}(\pi_{i}(s),\pi_{i}(t))$ where
$\pi_{i}\colon\textstyle\prod_{i\in I}F_{i}X\to F_{i}X$ are the projections.

coproduct functors:

$d^{F}_{X}\colon(F_{1}X+F_{2}X)\times(F_{1}X+F_{2}X)\to\mathcal{V}$, where

$d^{F}_{X}(s,t)=\begin{cases}d^{F_{i}}(s,t)&\mbox{if $s,t\in F_{i}X$ for
$i\in\\{1,2\\}$}\\\ \top&\mbox{if $s\in F_{1}X$, $t\in F_{2}X$}\\\
\bot&\mbox{if $s\in F_{2}X$, $t\in F_{1}X$}\end{cases}$

######  Proof 4.6.

constant functors:

let $b,c\in B$. We have, since $Ff$ is the identity:

$\displaystyle d^{F}_{X}(b,c)$ $\displaystyle=$
$\displaystyle\bigsqcap_{\mathit{ev}\in\Lambda^{F}}\bigsqcap_{f\in\gamma(d_{X})}d_{\mathcal{V}}(\mathit{ev}(Ff(b)),\mathit{ev}(Ff(c)))$
$\displaystyle=$
$\displaystyle\bigsqcap_{\mathit{ev}\in\Lambda^{F}}d_{\mathcal{V}}(\mathit{ev}(b),\mathit{ev}(c))$

identity functor:

let $x,y\in X$. We have, since $Ff=f$ and $\mathit{ev}$ is the identity:

$\displaystyle d^{F}_{X}(x,y)$ $\displaystyle=$
$\displaystyle\bigsqcap_{\mathit{ev}\in\Lambda^{F}}\bigsqcap_{f\in\gamma(d_{X})}d_{\mathcal{V}}(\mathit{ev}(Ff(x)),\mathit{ev}(Ff(y)))$
$\displaystyle=$
$\displaystyle\bigsqcap_{f\in\gamma(d_{X})}d_{\mathcal{V}}(f(x)),f(y)))=\alpha_{X}(\gamma_{X}(d_{X}))(x,y)$

product functors:

Let $s,t\in\textstyle\prod_{i\in I}F_{i}X$. Let
$\pi_{i}\colon\textstyle\prod_{i\in I}F_{i}X\to F_{i}X$,
$\pi^{\prime}_{i}\colon\textstyle\prod_{i\in I}F_{i}\mathcal{V}\to
F_{i}\mathcal{V}$. Then

$\displaystyle d^{F}_{X}(s,t)$ $\displaystyle=$
$\displaystyle\bigsqcap_{\mathit{ev}\in\Lambda^{F}}\bigsqcap_{f\in\gamma(d_{X})}d_{\mathcal{V}}(\mathit{ev}(Ff(s)),\mathit{ev}(Ff(t)))$
$\displaystyle=$ $\displaystyle\bigsqcap_{i\in
I}\bigsqcap_{\mathit{ev}_{i}\in\Lambda^{F_{i}}}\bigsqcap_{f\in\gamma(d_{X})}d_{\mathcal{V}}(\mathit{ev}_{i}(\pi^{\prime}_{i}(Ff(s))),\mathit{ev}_{i}(\pi^{\prime}_{i}(Ff(t))))$
$\displaystyle=$ $\displaystyle\bigsqcap_{i\in
I}\bigsqcap_{\mathit{ev}_{i}\in\Lambda^{F_{i}}}\bigsqcap_{f\in\gamma(d_{X})}d_{\mathcal{V}}(\mathit{ev}_{i}(F_{i}f(\pi_{i}(s))),\mathit{ev}_{i}(F_{i}f(\pi_{i}(t))))$
$\displaystyle=$ $\displaystyle\bigsqcap_{i\in
I}d_{X}^{F_{i}}(\pi_{i}(Ff(s)),\pi_{i}(Ff(t)))$

using the fact that $\pi^{\prime}_{i}\circ Ff=F_{i}f\circ\pi_{i}$.

coproduct functors:

We use the properties of $d_{\mathcal{V}}$ shown in Lemma 2.1. Whenever
$s,t\in F_{1}X$, we have that

$\displaystyle d^{F}_{X}(s,t)$ $\displaystyle=$
$\displaystyle\bigsqcap_{\mathit{ev}_{1}\in\Lambda^{F_{1}}}\bigsqcap_{f\in\gamma(d_{X})}d_{\mathcal{V}}(\mathit{ev}_{1}(Ff(s)),\mathit{ev}_{1}(Ff(t)))\sqcap
d_{\mathcal{V}}(\bot,\bot)$ $\displaystyle=$ $\displaystyle
d^{F_{1}}(s,t)\sqcap\top=d^{F_{1}}(s,t)$

If instead $s,t\in F_{2}X$, we obtain

$\displaystyle d^{F}_{X}(s,t)$ $\displaystyle=$
$\displaystyle\bigsqcap_{\mathit{ev}_{2}\in\Lambda^{F_{2}}}\bigsqcap_{f\in\gamma(d_{X})}d_{\mathcal{V}}(\mathit{ev}_{2}(Ff(s)),\mathit{ev}_{2}(Ff(t)))\sqcap
d_{\mathcal{V}}(\top,\top)$ $\displaystyle=$ $\displaystyle
d^{F_{2}}(s,t)\sqcap\top=d^{F_{2}}(s,t)$

Now assume that $s\in F_{1}X$, $t\in F_{2}X$. Then:

$\displaystyle d^{F}_{X}(s,t)$ $\displaystyle=$
$\displaystyle\bigsqcap_{\mathit{ev}_{1}\in\Lambda^{F_{1}}}\bigsqcap_{f\in\gamma(d_{X})}d_{\mathcal{V}}(\mathit{ev}_{1}(Ff(s)),\top)\mathop{\sqcap}$
$\displaystyle\qquad\bigsqcap_{\mathit{ev}_{2}\in\Lambda^{F_{2}}}\bigsqcap_{f\in\gamma(d_{X})}d_{\mathcal{V}}(\bot,\mathit{ev}_{1}(Ff(t)))\sqcap
d_{\mathcal{V}}(\bot,\top)$ $\displaystyle=$
$\displaystyle\top\sqcap\top\sqcap\top=\top$

Now assume that $s\in F_{2}X$, $t\in F_{1}X$. Then, since
$d_{\mathcal{V}}(\bot,\top)=\bot$:

$\displaystyle d^{F}_{X}(s,t)$ $\displaystyle=$
$\displaystyle\bigsqcap_{\mathit{ev}_{1}\in\Lambda^{F_{1}}}\bigsqcap_{f\in\gamma(d_{X})}d_{\mathcal{V}}(\top,\mathit{ev}_{1}(Ff(t)))\mathop{\sqcap}$
$\displaystyle\qquad\bigsqcap_{\mathit{ev}_{2}\in\Lambda^{F_{2}}}\bigsqcap_{f\in\gamma(d_{X})}d_{\mathcal{V}}(\mathit{ev}_{2}(Ff(s)),\bot))\sqcap
d_{\mathcal{V}}(\top,\bot)=\bot$

Under this choice of evaluation functions we can show the following, which
implies compositionality (cf. Section 4.2): For every polynomial functor $F$
and the corresponding set $\Lambda^{F}$ of evaluation maps (as above) we have
$\Lambda^{F}\circ\gamma\circ\alpha\subseteq\gamma{F}\circ\alpha{F}\circ\Lambda^{F}$
on non-empty sets of predicates.

######  Proof 4.7.

Given $F$ and $\Lambda^{F}$, we need to show that for every set $X$, every
$S\subseteq\mathcal{V}^{X}$, every
$f\colon{(X,\alpha_{X}(S))}\to{(\mathcal{V},d_{\mathcal{V}})}$, every
$\mathit{ev}\in\Lambda^{F}$ and every $t_{1},t_{2}\in FX$ we have

$\alpha_{X}(\Lambda^{F}_{X}(S))(t_{1},t_{2})\sqsubseteq
d_{\mathcal{V}}(\mathit{ev}\circ Ff(t_{1}),\mathit{ev}\circ Ff(t_{2})).$ (2)

We proceed by induction over $F$.

  * •

For $F=C_{B}$, the set $\Lambda^{F}$ consists of some maps of type
$B\to\mathcal{V}$. Then for (2) to hold we need that for every $b_{1},b_{2}\in
B$ and every $\mathit{ev}\in\Lambda^{F}$ we have

$\bigsqcap_{\mathit{ev}^{\prime}\in\Lambda^{F}}d_{\mathcal{V}}(\mathit{ev}^{\prime}(b_{1}),\mathit{ev}^{\prime}(b_{2}))\sqsubseteq
d_{\mathcal{V}}(\mathit{ev}(b_{1}),\mathit{ev}(b_{2})).$

This holds automatically, regardless of the specific choice of $\Lambda^{F}$,
as the term on the right is one of the terms in the meet on the left.

  * •

For $F=\mathrm{Id}$, the equation (2) reduces to the statement that $f$ is
non-expansive wrt. $\alpha_{X}(S)$, which is true by assumption.

  * •

For $F=\textstyle\prod_{i\in I}F_{i}$, let $s=(s_{i})_{i\in I},t=(t_{i})_{i\in
I}\in FX$ and fix some $j\in I$. Then we have for each
$\mathit{ev}\in\Lambda^{F_{j}}$ and each $g\colon X\to\mathcal{V}$ that
$\mathit{ev}\circ\pi_{j}\circ Fg(s)=\mathit{ev}\circ F_{j}g(s_{j})$ and
$\mathit{ev}\circ\pi_{j}\circ Fg(t)=\mathit{ev}\circ F_{j}g(t_{j})$, and thus

$\displaystyle\alpha_{X}(\Lambda^{F}_{X}(S))(s,t)$
$\displaystyle=\bigsqcap_{i\in
I}\bigsqcap_{\mathit{ev}\in\Lambda^{F_{i}}}\bigsqcap_{g\in
S}d_{\mathcal{V}}(\mathit{ev}\circ\pi_{i}\circ
Fg(s),\mathit{ev}\circ\pi_{i}\circ Fg(t))$
$\displaystyle\sqsubseteq\bigsqcap_{\mathit{ev}\in\Lambda^{F_{j}}}\bigsqcap_{g\in
S}d_{\mathcal{V}}(\mathit{ev}\circ\pi_{j}\circ
Fg(s),\mathit{ev}\circ\pi_{j}\circ Fg(t))$
$\displaystyle=\bigsqcap_{\mathit{ev}\in\Lambda^{F_{j}}}\bigsqcap_{g\in
S}d_{\mathcal{V}}(\mathit{ev}\circ F_{j}g(s_{j}),\mathit{ev}\circ
F_{j}g(t_{j}))$
$\displaystyle=\alpha_{X}(\Lambda^{F_{j}}_{X}(S))(s_{j},t_{j})$
$\displaystyle\sqsubseteq d_{\mathcal{V}}(\mathit{ev}\circ
F_{j}f(s_{j}),\mathit{ev}\circ F_{j}f(t_{j}))$ $\displaystyle(\text{IH})$
$\displaystyle=d_{\mathcal{V}}(\mathit{ev}\circ\pi_{j}\circ
Ff(s),\mathit{ev}\circ\pi_{j}\circ Ff(t))$

for each $f\colon{(X,\alpha_{X}(S))}\to{(\mathcal{V},d_{\mathcal{V}})}$ and
each $\mathit{ev}\in\Lambda^{F_{j}}$.

  * •

For $F=F_{1}+F_{2}$, let $s\in F_{i}X\subseteq FX$ and $t\in F_{j}X\subseteq
FX$, and let $\mathit{ev}\in\Lambda^{F}$.

    * –

If $i=1$ and $\mathit{ev}$ is of the form $[\bot,\top]$ or
$[\bot,\mathit{ev}_{2}]$, then the right hand side of (2) evaluates to
$d_{\mathcal{V}}(\bot,v)$ for some $v\in\mathcal{V}$, which equals $\top$.

    * –

If $j=2$ and $\mathit{ev}$ is of the form $[\bot,\top]$ or
$[\mathit{ev}_{1},\top]$, then the right hand side of (2) evaluates to
$d_{\mathcal{V}}(v,\top)$ for some $v\in\mathcal{V}$, which equals $\top$.

    * –

If $i=j=1$, and $\mathit{ev}$ is of the form $[\mathit{ev}_{1},\top]$, then we
show (2) as follows.

$\displaystyle\alpha_{X}(\Lambda^{F}_{X}(S))(s,t)$
$\displaystyle\sqsubseteq\bigsqcap_{\mathit{ev}_{1}\in\Lambda^{F_{1}}}\bigsqcap_{g\in
S}d_{\mathcal{V}}([\mathit{ev}_{1},\top]\circ
Fg(s),[\mathit{ev}_{1},\top]\circ Fg(t))$
$\displaystyle=\bigsqcap_{\mathit{ev}_{1}\in\Lambda^{F_{1}}}\bigsqcap_{g\in
S}d_{\mathcal{V}}(\mathit{ev}_{1}\circ F_{1}g(s),\mathit{ev}_{1}\circ
F_{1}g(t))$ $\displaystyle=\alpha_{X}(\Lambda^{F_{1}}_{X}(S))(s,t)$
$\displaystyle\sqsubseteq d_{\mathcal{V}}(\mathit{ev}_{1}\circ
F_{1}f(s),\mathit{ev}_{1}\circ F_{1}f(t))$ $\displaystyle(\text{IH})$
$\displaystyle=d_{\mathcal{V}}([\mathit{ev}_{1},\top]\circ
Ff(s),[\mathit{ev}_{1},\top]\circ Ff(t))$

    * –

If $i=j=2$, and $\mathit{ev}$ is of the form $[\bot,\mathit{ev}_{2}]$, the
proof is very similar to the previous item.

    * –

The only remaining case is that where $i=2$ and $j=1$. In that case, we can
pick $[\bot,\top]\in\Lambda^{F}$ and some arbitrary $g\in S$ (here it is
important that $S$ is non-empty) to show that the left hand side of (2)
evaluates to $\bot$:

$\alpha_{X}(\Lambda^{F}_{X}(S))(s,t)\sqsubseteq
d_{\mathcal{V}}([\bot,\top]\circ Fg(s),[\bot,\top]\circ
Fg(t))=d_{\mathcal{V}}(\top,\bot)=\bot.$

From this we can infer that $K_{\Lambda^{F}}\circ
K_{\Lambda^{G}}=K_{\Lambda^{F}*\Lambda^{G}}$ using the arguments of Section
4.2, hence we have compositionality.

##  5 Application: Up-To Techniques

We now adapt results from [bkp:up-to-behavioural-metrics-fibrations-journal]
on up-to techniques from Wasserstein to Kantorovich liftings. In particular we
instantiate the fibrational approach to coinductive proof techniques from
[bppr:general-coinduction-up-to] that allows to prove lower bounds for
greatest fixpoints, using post-fixpoints up-to as witnesses. As shown in
Section 6 this can greatly help to reduce the size of such witnesses, even
allowing finitary witnesses which would be infinite otherwise.

###  5.1 Introduction to Up-To Techniques

We first recall the notion of a bialgebra [j:bialgebraic-review], i.e., a
coalgebra with a compatible algebra structure.

######  Definition 5.1.

Consider two functors $F,T$ and a natural transformation $\zeta\colon
TF\Rightarrow FT$. A _bialgebra_ for $\zeta$ is a tuple $(Y,a,c)$ such that
$a\colon TY\to Y$ is a $T$-algebra, $c\colon Y\to FY$ is an $F$-coalgebra so
that the diagram below commutes.

${TY}$${Y}$${FY}$${TFY}$${FTY}$$\scriptstyle{a}$$\scriptstyle{Tc}$$\scriptstyle{c}$$\scriptstyle{\zeta_{Y}}$$\scriptstyle{Fa}$

In order to construct such bialgebras, distributive laws exchanging functors
and monads are helpful.

######  Definition 5.2.

A _distributive law_ or _EM-law_ of a monad $T:\mathbf{C}\to\mathbf{C}$ with
unit $\eta:\mathrm{Id}\Rightarrow T$ and multiplication $\mu:TT\Rightarrow T$
over a functor $F:\mathbf{C}\to\mathbf{C}$ is a natural transformation
$\zeta:TF\Rightarrow FT$ such that the following diagrams commute:

${FX}$${{T^{2}FX}}$${TFTX}$${{FT^{2}X}}$${TFX}$${FTX}$${TFX}$${FTX}$$\scriptstyle{\eta_{FX}}$$\scriptstyle{\zeta_{X}}$$\scriptstyle{F\eta_{X}}$$\scriptstyle{\mu_{FX}}$$\scriptstyle{F\mu_{X}}$$\scriptstyle{T\zeta_{X}}$$\scriptstyle{\zeta_{TX}}$$\scriptstyle{\zeta_{X}}$

Whenever $T$ is a monad and $\zeta$ is an EM-law, then a bialgebra can be
obtained by determinizing a coalgebra $c\colon X\to FTX$. More concretely, we
obtain $c^{\\#}\colon Y\to FY$ where $Y=TX$ and
$c^{\\#}=F\mu_{X}\circ\zeta_{TX}\circ Tc$. The algebra map is $a=\mu_{X}\colon
TY\to Y$. Examples involving determinization will be given in Section 6.

We now assume a bialgebra $(Y,a,c)$ and Kantorovich liftings
$\overline{T}=K_{\Lambda^{T}}$, $\overline{F}=K_{\Lambda^{F}}$ of $T,F$. Based
on this we can define a _behaviour function_ beh via

$\mathcal{V}\textrm{-}\mathsf{Graph}_{Y}\stackrel{{\scriptstyle\overline{F}}}{{\longrightarrow}}\mathcal{V}\textrm{-}\mathsf{Graph}_{FY}\stackrel{{\scriptstyle
c^{*}}}{{\longrightarrow}}\mathcal{V}\textrm{-}\mathsf{Graph}_{Y}$

The greatest fixpoint of beh corresponds to a behavioural conformance (e.g.,
behavioural equivalence or bisimulation metric). Furthermore we can define an
_up-to function_ $u$ via

$\mathcal{V}\textrm{-}\mathsf{Graph}_{Y}\stackrel{{\scriptstyle\overline{T}}}{{\longrightarrow}}\mathcal{V}\textrm{-}\mathsf{Graph}_{TY}\stackrel{{\scriptstyle\Sigma_{a}}}{{\longrightarrow}}\mathcal{V}\textrm{-}\mathsf{Graph}_{Y}$

where
$\Sigma_{f}\colon\mathcal{V}\textrm{-}\mathsf{Graph}_{X}\to\mathcal{V}\textrm{-}\mathsf{Graph}_{Y}$
is defined as
$\Sigma_{f}(d)(y_{1},y_{2})=\bigsqcup_{f(x_{i})=y_{i}}d(x_{1},x_{2})$ for
$f\colon X\to Y$ (direct image).

Both functions ($\mathrm{beh}$, $u$) are monotone functions on a complete
lattice. Hence we can use the Knaster-Tarski theorem [t:lattice-fixed-point]
and the theory of up-to techniques [p:complete-lattices-up-to]. In particular,
given a monotone function $f\colon L\to L$ over a complete lattice
$(L,\sqsubseteq)$, we know that its greatest fixpoint $\nu f$ coincides with
its greatest post-fixpoint, where a post-fixpoint is an element $\ell\in L$
with $\ell\sqsubseteq f(\ell)$. Furthermore, given a monotone function
$u\colon L\to L$ that is $f$-compatible (i.e., $u\circ f\sqsubseteq f\circ
u$), we can infer that $\ell\sqsubseteq f(u(\ell))$ (i.e., $\ell$ is a post-
fixpoint up-to $u$) implies $\ell\sqsubseteq\nu f$.

From [bkp:up-to-behavioural-metrics-fibrations-journal] we obtain the
following result that ensures compatibility:

######  Proposition 5.3 ([bkp:up-to-behavioural-metrics-fibrations-journal]).

Whenever the EM-law $\zeta\colon TF\Rightarrow FT$ lifts to
$\zeta\colon\overline{T}\,\overline{F}\Rightarrow\overline{F}\,\overline{T}$,
we have that $u\circ\textrm{beh}\sqsubseteq\textrm{beh}\circ u$ (for
$u$,$\mathrm{beh}$ as defined above).

Hence, we can deduce that every post-fixpoint up-to witnesses a lower bound of
the greatest fixpoint. More concretely:
$d_{Y}\sqsubseteq\textrm{beh}(u(d_{Y}))$ implies
$d_{Y}\sqsubseteq\nu\,\textrm{beh}$ (where
$d_{Y}\in\mathcal{V}\textrm{-}\mathsf{Graph}_{Y}$) (coinduction up-to proof
principle).

To use this proof technique, we have to show that $\zeta$ lifts accordingly to
obtain an up-to technique usable for Kantorovich liftings. We start by
defining distributive laws and lifting them to
$\mathcal{V}\textrm{-}\mathsf{Graph}$.

###  5.2 Lifting Distributive Laws

Let $F$ be a polynomial functor (cf. Section 4.3) and $(T,\mu,\eta)$ a monad
over $\mathsf{Set}$. Following [j:introduction-coalgebra, Exercise 5.4.4], EM-
laws $\zeta:TF\Rightarrow FT$ can then be constructed inductively over the
structure of $F$, i.e., for $F$ being an identity, constant, product and
coproduct functor. In the coproduct case we extend [j:introduction-coalgebra]
by weakening the requirement that $T$ preserves coproducts.

In the following, we inductively construct an EM-law $\zeta:TF\Rightarrow FT$
and first lift it to $\zeta:\overline{TF}\Rightarrow\overline{FT}$ (and then
to $\zeta:\overline{T}\,\overline{F}\Rightarrow\overline{F}\,\overline{T}$).
For the evaluation maps we assume that $\Lambda^{F}$ is defined as in Section
4.3 and that $\Lambda^{T}=\\{\mathit{ev}_{T}\\}$, where $\mathit{ev}_{T}\colon
T\mathcal{V}\to\mathcal{V}$ is a $T$-algebra.

constant functors:

For $F=C_{B}$ we have that $TF=TB$ and $FT=B$, and so define the EM-law as
$\zeta:TC_{B}\Rightarrow C_{B}$, where the (unique) component $\zeta_{X}\colon
TB\to B$ is an arbitrary $T$-algebra on $B$. (From now on, we assume that
evaluation maps $\mathit{ev}\colon B\to\mathcal{V}$ for constant functors are
$T$-algebra homomorphisms between $\zeta\colon TB\to B$ and
$\mathit{ev}_{T}\colon T\mathcal{V}\to\mathcal{V}$.)

identity functor:

For $F=\operatorname{Id}$, we let the EM-law be the identity map
$\operatorname{id}:T\Rightarrow T$.

product functors:

For $F=\textstyle\prod_{i\in I}F_{i}$, assuming we have distributive laws
$\zeta^{i}:TF_{i}\Rightarrow F_{i}T$, the EM-law is

$\langle\zeta^{i}\circ T\pi_{i}\rangle:T\textstyle\prod_{i\in
I}F_{i}\Rightarrow\textstyle\prod_{i\in I}F_{i}T.$

coproduct functors:

For $F=F_{1}+F_{2}$, assume that we have distributive laws
$\zeta^{i}:TF_{i}\Rightarrow F_{i}T$ and a natural transformation
$g:T((-)+(-))\Rightarrow T+T$ between bifunctors. The EM-law is given by

$(\zeta^{1}+\zeta^{2})\circ g_{F_{1},F_{2}}\colon T(F_{1}+F_{2})\Rightarrow
TF_{1}+TF_{2}\Rightarrow F_{1}T+F_{2}T$

######  Definition 5.4.

Let $T$ be a monad and let $g:T((-)+(-))\Rightarrow T+T$ be a natural
transformation as above. We say that $g$ is _compatible with the unit_ $\eta$
of the monad if for all sets $Y_{1},Y_{2}$ the left diagram below commutes.
Analogously, $g$ is _compatible with the multiplication_ $\mu$ of the monad if
the right diagram commutes for all sets $Y_{1},Y_{2}$.

${{Y_{1}+Y_{2}}}$${{T(Y_{1}+Y_{2})}}$${{TY_{1}+TY_{2}}}$$\scriptstyle{g_{Y_{1},Y_{2}}}$$\scriptstyle{\eta_{Y_{1}+Y_{2}}}$$\scriptstyle{\eta_{Y_{1}}+\eta_{Y_{2}}}$

${{TT(Y_{1}+Y_{2})}}$${{T(Y_{1}+Y_{2})}}$${{T(TY_{1}+TY_{2})}}$${{TTY_{1}+TTY_{2}}}$${{TY_{1}+TY_{2}}}$$\scriptstyle{Tg_{Y_{1},Y_{2}}}$$\scriptstyle{g_{TY_{1},TY_{2}}}$$\scriptstyle{\mu_{Y_{1}}+\mu_{Y_{2}}}$$\scriptstyle{g_{Y_{1},Y_{2}}}$$\scriptstyle{\mu_{Y_{1}+Y_{2}}}$

Assume that the natural transformation $g$ is compatible with unit and
multiplication of $T$. Then the transformation $\zeta$ as defined above is an
EM-law of $T$ over $F$.

######  Proof 5.5.

We will proceed by induction over the shape of $F$. We wish to show that they
$\zeta\colon TF\Rightarrow FT$ is a natural transformations and that the two
diagrams in Definition 5.2 commute.

constant functors:

If $F=C_{B}$, the naturality is clear and the distributive law diagrams become

${B}$${{T^{2}B}}$${TB}$${B}$${TB}$${B}$${TB}$${B,}$$\scriptstyle{\eta_{X}}$$\scriptstyle{\zeta}$$\scriptstyle{\operatorname{Id}_{B}}$$\scriptstyle{\mu_{B}}$$\scriptstyle{\mathrm{Id}_{B}}$$\scriptstyle{T\zeta}$$\scriptstyle{\zeta}$$\scriptstyle{\zeta}$

which are precisely the conditions for the map $\zeta:TB\to B$ being an
algebra over $T$.

identity functor:

For $F=\mathrm{Id}$, it is also clear that $\mathrm{id}:T\Rightarrow T$ is a
natural transformation and a distributive law.

product functors:

For $F=\textstyle\prod_{i\in I}F_{i}$, we note that the definition of the
distributive law $\zeta$ in terms of the $\zeta^{i}$ amounts to the set of
equalities $\zeta^{i}\circ T\pi_{i}=\pi_{i}\circ\zeta$ for each $i\in I$.
Therefore we can verify the triangle and pentagon diagrams via the following
computations:

$\displaystyle F\eta$ $\displaystyle=\langle F_{i}\eta\circ\pi_{i}\rangle$
$\displaystyle=\langle\zeta^{i}\circ\eta_{F_{i}}\circ\pi_{i}\rangle$
$\displaystyle(\text{IH})$ $\displaystyle=\langle\zeta^{i}\circ
T\pi_{i}\circ\eta_{F}\rangle$ $\displaystyle(\text{$\eta$ natural})$
$\displaystyle=\langle\pi_{i}\circ\zeta\circ\eta_{F}\rangle=\zeta\circ\eta_{F}$
$\displaystyle F\mu\circ\zeta\circ T\zeta$ $\displaystyle=\langle
F_{i}\mu\circ\pi_{i}\circ\zeta\circ T\zeta\rangle$ $\displaystyle=\langle
F_{i}\mu\circ\zeta^{i}\circ T\pi_{i}\circ T\zeta\rangle$
$\displaystyle=\langle F_{i}\mu\circ\zeta^{i}\circ T\zeta^{i}\circ
TT\pi_{i}\rangle$ $\displaystyle=\langle\zeta^{i}\circ\mu_{F_{i}}\circ
TT\pi_{i}\rangle$ $\displaystyle(\text{IH})$
$\displaystyle=\langle\zeta^{i}\circ T\pi_{i}\circ\mu_{F}\rangle$
$\displaystyle(\text{$\mu$ natural})$
$\displaystyle=\langle\pi_{i}\circ\zeta\circ\mu_{F}\rangle=\zeta\circ\mu_{F}$

coproduct functors:

For $F=F_{1}+F_{2}$, we first check the commutativity of the triangular
diagram. In the diagram below, the left inner triangle commutes because of
assumption on $g$, while the right inner triangle commutes by induction
hypothesis.

${{F_{1}X+F_{2}X}}$${{T(F_{1}X+F_{2}X)}}$${{TF_{1}X+TF_{2}X}}$${{F_{1}TX+F_{2}TX}}$$\scriptstyle{g_{F_{1}X,F_{2}X}}$$\scriptstyle{\eta_{F_{1}X+F_{2}X}}$$\scriptstyle{\eta_{F_{1}X}+\eta_{F_{2}X}}$$\scriptstyle{\zeta^{1}_{X}+\zeta^{2}_{X}}$$\scriptstyle{F_{1}\eta_{X}+F_{2}\eta_{X}}$

Hence, the outer diagram commutes, establishing the required condition. Moving
on to the pentagonal diagram, we have the following:

${{TT(F_{1}X+F_{2}X)}}$${{T(TF_{1}X+TF_{2}X)}}$${{T(F_{1}TX+F_{2}TX)}}$${{TTF_{1}X+TTF_{2}X}}$${{TF_{1}TX+TF_{2}TX}}$${{F_{1}TTX+F_{2}TTX}}$${{T(F_{1}X+F_{2}X)}}$${{TF_{1}X+TF_{2}X}}$${{F_{1}TX+F_{2}TX}}$$\scriptstyle{g_{F_{1}TX,F_{2}TX}}$$\scriptstyle{\zeta^{1}_{TX}+\zeta^{2}_{TX}}$$\scriptstyle{F_{1}\mu_{X}+F_{2}\mu_{X}}$$\scriptstyle{\zeta^{1}_{X}+\zeta^{2}_{X}}$$\scriptstyle{T\zeta^{1}_{X}+T\zeta^{2}_{X}}$$\scriptstyle{\mu_{F_{1}X}+\mu_{F_{2}X}}$$\scriptstyle{T(\zeta^{1}_{X}+\zeta^{2}_{X})}$$\scriptstyle{g_{TF_{1}X,TF_{2}X}}$$\scriptstyle{Tg_{F_{1}X,F_{2}X}}$$\scriptstyle{g_{F_{1}X,F_{2}X}}$$\scriptstyle{\mu_{F_{1}X+F_{2}X}}$

The top right square commutes by naturality of $g$, while the bottom right
diagram commutes by induction hypothesis. Finally, the left diagram commutes
because of the assumption we make on $g$. The commutativity of the outer
diagram yields the desired result.

In order to lift natural transformations (respectively distributive laws), we
will use the following result:

Let $F,G$ be functors on $\mathsf{Set}$ and let the sets of evaluation maps of
$F$ and $G$ be denoted by $\Lambda^{F}$ and $\Lambda^{G}$. Let
$\zeta:F\Rightarrow G$ be a natural transformation. If

$\Lambda^{G}\circ\zeta_{\mathcal{V}}:=\\{\mathit{ev}_{G}\circ\zeta_{\mathcal{V}}\mid\mathit{ev}_{G}\in\Lambda^{G}\\}\subseteq\Lambda^{F},$
(3)

then $\zeta$ lifts to $\zeta:\overline{F}\Rightarrow\overline{G}$ in
$\mathcal{V}\textrm{-}\mathsf{Graph}$, where $\overline{F}=K_{\Lambda^{F}}$,
$\overline{G}=K_{\Lambda^{G}}$.

######  Proof 5.6.

To prove this, we need to show that the transformation $\zeta$ is non-
expansive in each component, i.e. that for every
$(X,d)\in\mathcal{V}\textrm{-}\mathsf{Graph}$,

$d^{F}\sqsubseteq d^{G}\circ(\zeta_{X}\times\zeta_{X}).$

Unpacking the proof of the Kantorovich lifting, we wish to show that for every
$t_{1},t_{2}\in FX$

$\displaystyle d^{F}(t_{1},t_{2})$ $\displaystyle=$
$\displaystyle\bigsqcap\big{\\{}d_{\mathcal{V}}((\mathit{ev}_{F}\circ
Ff)(t_{1}),(\mathit{ev}_{F}\circ
Ff)(t_{2}))\mid\mathit{ev}_{F}\in\Lambda^{F},$ $\displaystyle\qquad\qquad
d\sqsubseteq d_{\mathcal{V}}\circ(f\times f),\,f:X\to\mathcal{V}\big{\\}}$
$\displaystyle\sqsubseteq$
$\displaystyle\bigsqcap\big{\\{}d_{\mathcal{V}}((\mathit{ev}_{G}\circ\zeta_{\mathcal{V}}\circ
Ff)(t_{1}),(\mathit{ev}_{G}\circ\zeta_{\mathcal{V}}\circ
Ff)(t_{2}))\mid\mathit{ev}_{G}\in\Lambda^{G},$ $\displaystyle\qquad\qquad
d\sqsubseteq d_{\mathcal{V}}\circ(f\times f),\,f:X\to\mathcal{V}\big{\\}}$
$\displaystyle=$
$\displaystyle\bigsqcap\big{\\{}d_{\mathcal{V}}((\mathit{ev}_{G}\circ
Gf\circ\zeta_{X})(t_{1}),(\mathit{ev}_{G}\circ
Gf\circ\zeta_{X})(t_{2}))\mid\mathit{ev}_{G}\in\Lambda^{G},$
$\displaystyle\qquad\qquad d\sqsubseteq d_{\mathcal{V}}\circ(f\times
f),\,f:X\to\mathcal{V}\big{\\}}$ $\displaystyle=$ $\displaystyle
d^{G}(\zeta_{X}(t_{1}),\zeta_{X}(t_{2})).$

by the assumption we know that the set of functions of the form
$\mathit{ev}_{G}\circ\zeta_{\mathcal{V}}$ is a superset of the set of
functions of the form $\mathit{ev}_{F}$, and so the first infimum is smaller
or equal than the second. And by the naturality of $\zeta$, we have that
$\zeta_{\mathcal{V}}\circ Ff=Gf\circ\zeta_{X}$.

We can show that the inclusion (3) (even equality) holds under some
conditions.

######  Definition 5.7.

Let $g:T((-)+(-))\Rightarrow T+T$ be a natural transformation as introduced
above and let $\mathit{ev}_{T}\colon T\mathcal{V}\to\mathcal{V}$ be the
evaluation map of the monad. We say that $g$ is _well-behaved_ wrt.
$\mathit{ev}_{T}$ if the following diagrams commute for $f_{i}\colon
X_{i}\to\mathcal{V}$, where $\bot,\top$ are constant maps of the appropriate
type.

${{T(X_{1}+X_{2})}}$${T\mathcal{V}}$${{TX_{1}+TX_{2}}}$${\mathcal{V}}$$\scriptstyle{g_{X_{1},X_{2}}}$$\scriptstyle{ev_{T}}$$\scriptstyle{T[f_{1},\top_{X_{2}}]}$$\scriptstyle{[\mathit{ev}_{T}\circ
Tf_{1},\top_{TX_{2}}]}$

${{T(X_{1}+X_{2})}}$${T\mathcal{V}}$${{TX_{1}+TX_{2}}}$${\mathcal{V}}$$\scriptstyle{g_{X_{1},X_{2}}}$$\scriptstyle{ev_{T}}$$\scriptstyle{T[\bot_{X_{1}},f_{2}]}$$\scriptstyle{[\bot_{TX_{1}},\mathit{ev}_{T}\circ
Tf_{2}]}$

${{T(X_{1}+X_{2})}}$${T\mathcal{V}}$${{TX_{1}+TX_{2}}}$${\mathcal{V}}$$\scriptstyle{g_{X_{1},X_{2}}}$$\scriptstyle{ev_{T}}$$\scriptstyle{T[\bot_{X_{1}},\top_{X_{2}}]}$$\scriptstyle{[\bot_{TX_{1}},\top_{TX_{2}}]}$

Let $F$ be a polynomial functor and $T$ a monad with
$\Lambda^{T}=\\{\mathit{ev}_{T}\\}$.

For distributive laws $\zeta$ as described above where the component $g$ is
well-behaved wrt. $\mathit{ev}_{T}$ and evaluation maps defined in Section
4.3, we have that

$(\Lambda^{F}*\Lambda^{T})\circ\zeta_{\mathcal{V}}=\Lambda^{T}*\Lambda^{F}.$

######  Proof 5.8.

We will prove this via the inductive definition of $F$. In particular we will
show that for each $\mathit{ev}\in\Lambda^{T}*\Lambda^{F}$ there exists
$\mathit{ev}^{\prime}\in\Lambda^{F}*\Lambda^{T}$ such that
$\mathit{ev}=\mathit{ev}^{\prime}\circ\zeta_{V}$. And for each
$\mathit{ev}^{\prime}\in\Lambda^{F}*\Lambda^{T}$ there exists
$\mathit{ev}\in\Lambda^{T}*\Lambda^{F}$ such that
$\mathit{ev}=\mathit{ev}^{\prime}\circ\zeta_{V}$.

For the case where $F=C_{B}$ we obtain:

$\displaystyle\Lambda^{F}*\Lambda^{T}$ $\displaystyle=$
$\displaystyle\\{\mathit{ev}_{F}\circ
F\mathit{ev}_{T}\mid\mathit{ev}_{F}\in\Lambda^{F}\\}=\\{\mathit{ev}_{F}\circ\mathrm{id}_{B}\mid\mathit{ev}_{F}\in\Lambda^{F}\\}=\Lambda^{F}$
$\displaystyle\Lambda^{T}*\Lambda^{F}$ $\displaystyle=$
$\displaystyle\\{\mathit{ev}_{T}\circ
T\mathit{ev}_{F}\mid\mathit{ev}_{F}\in\Lambda^{F}\\}=\\{\mathit{ev}_{F}\circ\zeta_{\mathcal{V}}\mid\mathit{ev}_{F}\in\Lambda^{F}\\}$

where the last equality holds since each map $\mathit{ev}_{F}$ is an algebra
map from $\zeta_{\mathcal{V}}$ to $\mathit{ev}_{T}$ by assumption. In this
case we clearly have the correspondence stated above.

For $F=\operatorname{Id}$ we have remember that
$\mathit{ev}_{F}\in\Lambda^{F}$ and $\zeta_{\mathcal{V}}$ are both the
identity. Hence:

$\displaystyle\Lambda^{F}*\Lambda^{T}$ $\displaystyle=$
$\displaystyle\\{\mathit{ev}_{F}\circ
F\mathit{ev}_{T}\mid\mathit{ev}_{F}\in\Lambda^{F}\\}=\\{\mathit{ev}_{T}\\}=\Lambda^{T}$
$\displaystyle\Lambda^{T}*\Lambda^{F}$ $\displaystyle=$
$\displaystyle\\{\mathit{ev}_{T}\circ\mathrm{id}_{T\mathcal{V}}\mid\mathit{ev}_{F}\in\Lambda^{F}\\}=\Lambda^{T}$

Since both sets are the same and $\zeta_{\mathcal{V}}$ is the identity, the
correspondence clearly holds.

Now, consider the case for the product functor $F=\textstyle\prod_{i\in
I}F_{i}$. Then

$\displaystyle\Lambda^{F}*\Lambda^{T}$ $\displaystyle=$
$\displaystyle\\{\mathit{ev}^{\prime}_{i}\circ\pi_{i}\circ
F\mathit{ev}_{T}\mid i\in
I,\mathit{ev}^{\prime}_{i}\in\Lambda^{F_{i}},\mathit{ev}_{T}\in\Lambda^{T}\\}$
$\displaystyle\Lambda^{T}*\Lambda^{F}$ $\displaystyle=$
$\displaystyle\\{\mathit{ev}_{T}\circ T\mathit{ev}_{i}\circ T\pi_{i}\mid i\in
I,\mathit{ev}_{i}\in\Lambda^{F_{i}},\mathit{ev}_{T}\in\Lambda^{T}\\}$

Here $\zeta_{\mathcal{V}}:T\textstyle\prod_{i\in
I}F_{i}\mathcal{V}\to\textstyle\prod_{i\in I}F_{i}T\mathcal{V}$ is given as
the universal map $\langle\zeta^{i}_{\mathcal{V}}\circ T\pi_{i}\rangle_{i\in
I}$, i.e. the map such that
$\pi^{\prime}_{i}\circ\zeta_{\mathcal{V}}=\zeta^{i}_{\mathcal{V}}\circ
T\pi_{i}$, where $\pi^{\prime}_{i}\colon\textstyle\prod_{i\in
I}F_{i}T\mathcal{V}\to F_{i}T\mathcal{V}$.

Fix $i\in I$, $\mathit{ev}_{i}\in\Lambda^{F_{i}}$. Then, $\mathit{ev}_{T}\circ
T\mathit{ev}_{i}\in\Lambda^{T}*\Lambda^{F_{i}}$ and by the induction
hypothesis there exists $\mathit{ev}_{i}^{\prime}\circ
F_{i}\mathit{ev}_{T}\in\Lambda^{F_{i}}*\Lambda^{T}$ with
$\mathit{ev}^{\prime}_{i}\in\Lambda^{F_{i}}$ such that $\mathit{ev}_{T}\circ
T\mathit{ev}_{i}=\mathit{ev}_{i}^{\prime}\circ
F_{i}\mathit{ev}_{T}\circ\zeta^{i}_{\mathcal{V}}$.

Now for $\mathit{ev}_{T}\circ T\mathit{ev}_{i}\circ
T\pi_{i}\in\Lambda^{T}*\Lambda^{F}$ we pick
$\mathit{ev}^{\prime}_{i}\circ\pi_{i}\circ
F\mathit{ev}_{T}\in\Lambda^{F}*\Lambda^{T}$ as corresponding map and we have:

$\displaystyle\mathit{ev}^{\prime}_{i}\circ\pi_{i}\circ
F\mathit{ev}_{T}\circ\zeta_{\mathcal{V}}$
$\displaystyle=\mathit{ev}^{\prime}_{i}\circ\pi_{i}\circ
F\mathit{ev}_{T}\circ\langle\zeta^{i}_{\mathcal{V}}\circ T\pi_{i}\rangle_{i}$
$\displaystyle=\mathit{ev}^{\prime}_{i}\circ\pi_{i}\circ\langle
F_{i}\mathit{ev}_{T}\circ\zeta^{i}_{\mathcal{V}}\circ T\pi_{i}\rangle$
$\displaystyle=\mathit{ev}^{\prime}_{i}\circ
F_{i}\mathit{ev}_{T}\circ\zeta^{i}_{\mathcal{V}}\circ T\pi_{i}$
$\displaystyle=\mathit{ev}_{T}\circ T\mathit{ev}_{i}\circ T\pi_{i}$

The proof is analogous for the other direction.

Finally we address the case of the coproduct functor. Then

$\displaystyle\Lambda^{F}*\Lambda^{T}$ $\displaystyle=$
$\displaystyle\\{[\mathit{ev}_{1}\circ
F\mathit{ev}_{T},\top]\mid\mathit{ev}_{1}\in\Lambda^{F_{1}}\\}\cup\\{[\bot,\mathit{ev}_{2}\circ
F\mathit{ev}_{T}]\mid\mathit{ev}_{2}\in\Lambda^{F_{2}}\\}\cup\\{[\bot,\top]\\}$
$\displaystyle\Lambda^{T}*\Lambda^{F}$ $\displaystyle=$
$\displaystyle\\{\mathit{ev}_{T}\circ
T[\mathit{ev}_{1},\top]\mid\mathit{ev}_{1}\in\Lambda^{F_{1}}\\}\cup\\{\mathit{ev}_{T}\circ
T[\bot,\mathit{ev}_{2}]\mid\mathit{ev}_{2}\in\Lambda^{F_{2}}\\}\cup\\{\mathit{ev}_{T}\circ
T[\bot,\top]\\}$

If we fix $\mathit{ev}_{i}\in\Lambda^{F_{i}}$, then $\mathit{ev}_{T}\circ
T\mathit{ev}_{i}\in\Lambda^{T}*\Lambda^{F_{i}}$ and by the induction
hypothesis there exists $\mathit{ev}_{i}^{\prime}\circ
F_{i}\mathit{ev}_{T}\in\Lambda^{F_{i}}*\Lambda^{T}$ with
$\mathit{ev}^{\prime}_{i}\in\Lambda^{F_{i}}$ such that $\mathit{ev}_{T}\circ
T\mathit{ev}_{i}=\mathit{ev}_{i}^{\prime}\circ
F_{i}\mathit{ev}_{T}\circ\zeta^{1}_{\mathcal{V}}$.

We now consider three cases, according to the three subsets above.

For $\mathit{ev}_{T}\circ T[\mathit{ev}_{1},\top]\in\Lambda^{T}*\Lambda^{F}$
we pick $[\mathit{ev}^{\prime}_{1}\circ
F\mathit{ev}_{T},\top]\in\Lambda^{F}*\Lambda^{T}$ as corresponding map and we
have, using well-behavedness of $g$:

$\displaystyle[\mathit{ev}^{\prime}_{1}\circ
F\mathit{ev}_{T},\top]\circ\zeta_{\mathcal{V}}$
$\displaystyle=[\mathit{ev}^{\prime}_{1}\circ
F\mathit{ev}_{T},\top]\circ(\zeta^{1}_{\mathcal{V}}+\zeta^{2}_{\mathcal{V}})\circ
g_{F_{1}X,F_{2}X}$ $\displaystyle=[\mathit{ev}^{\prime}_{1}\circ
F\mathit{ev}_{T}\circ\zeta^{1}_{\mathcal{V}},\top\circ\zeta^{2}_{\mathcal{V}}]\circ
g_{F_{1}X,F_{2}X}$ $\displaystyle=[\mathit{ev}^{\prime}_{1}\circ
F\mathit{ev}_{T}\circ\zeta^{1}_{\mathcal{V}},\top]\circ g_{F_{1}X,F_{2}X}$
$\displaystyle=[\mathit{ev}_{T}\circ T\mathit{ev}_{1},\top]\circ
g_{F_{1}X,F_{2}X}$ $\displaystyle=\mathit{ev}_{T}\circ
T[\mathit{ev}_{1},\top]$

For $\mathit{ev}_{T}\circ T[\bot,\mathit{ev}_{2}]\in\Lambda^{T}*\Lambda^{F}$
we pick $[\bot,\mathit{ev}^{\prime}_{2}\circ
F\mathit{ev}_{T}]\in\Lambda^{F}*\Lambda^{T}$ as corresponding map and we have,
using well-behavedness of $g$:

$\displaystyle[\bot,\mathit{ev}^{\prime}_{2}\circ
F\mathit{ev}_{T}]\circ\zeta_{\mathcal{V}}$
$\displaystyle=[\bot,\mathit{ev}^{\prime}_{2}\circ
F\mathit{ev}_{T}]\circ(\zeta^{1}_{\mathcal{V}}+\zeta^{2}_{\mathcal{V}})\circ
g_{F_{1}X,F_{2}X}$
$\displaystyle=[\bot\circ\zeta^{1}_{\mathcal{V}},\mathit{ev}^{\prime}_{2}\circ
F\mathit{ev}_{T}\circ\zeta^{2}_{\mathcal{V}}]\circ g_{F_{1}X,F_{2}X}$
$\displaystyle=[\bot,\mathit{ev}^{\prime}_{2}\circ
F\mathit{ev}_{T}\circ\zeta^{2}_{\mathcal{V}}]\circ g_{F_{1}X,F_{2}X}$
$\displaystyle=[\bot,\mathit{ev}_{T}\circ T\mathit{ev}_{2}]\circ
g_{F_{1}X,F_{2}X}$ $\displaystyle=\mathit{ev}_{T}\circ
T[\bot,\mathit{ev}_{2}]$

For $\mathit{ev}_{T}\circ T[\bot,\top]\in\Lambda^{T}*\Lambda^{F}$ we pick
$[\bot,\top]\in\Lambda^{F}*\Lambda^{T}$ as corresponding map and we have,
using well-behavedness of $g$:

$\displaystyle[\bot,\top]\circ\zeta_{\mathcal{V}}$
$\displaystyle=[\bot,\top]\circ(\zeta^{1}_{\mathcal{V}}+\zeta^{2}_{\mathcal{V}})\circ
g_{F_{1}X,F_{2}X}$ $\displaystyle=[\bot\circ\zeta^{1}_{\mathcal{V}},\top
circ\zeta^{2}_{\mathcal{V}}]\circ g_{F_{1}X,F_{2}X}$
$\displaystyle=[\bot,\top]\circ g_{F_{1}X,F_{2}X}$
$\displaystyle=\mathit{ev}_{T}\circ T[\bot,\mathit{ev}_{2}]$

The other directions can be shown analogously. This concludes the proof.

Then, when we have a coalgebra of the form $Y\to FTY$ for $F$ polynomial and
$T$ a monad as above, and we determinize it to get a coalgebra $X\to FX$ for
$X=TY$, we obtain a bialgebra with the algebra structure given by the monad
multiplication $\mu_{Y}:TX\to X$. The EM-law obtained then also forms a
distributive law for the bialgebra. By Section 5.2 and Section 5.2 we know
that the distributive law $\zeta$ lifts to
$\mathcal{V}\textrm{-}\mathsf{Graph}$, i.e.,
$\zeta\colon\overline{FT}\Rightarrow\overline{TF}$ where
$\overline{FT}=K_{\Lambda^{F}*\Lambda^{T}}$ and
$\overline{TF}=K_{\Lambda^{T}*\Lambda^{F}}$.

We now show that natural transformations $g$ as required above do exist for
the powerset and subdistribution monad for suitable quantales. Note that they
are “asymmetric” and prioritize one of the two sets over the other.

Let $T=\mathcal{P}$ be the powerset monad with evaluation map
$\mathit{ev}_{T}=\sup$ for $\mathcal{V}={[0,1]_{\oplus}}$. Then
$g_{X_{1},X_{2}}$ below is a natural transformation that is compatible with
unit and multiplication of $T$ and is well-behaved.

$g_{X_{1},X_{2}}\colon\mathcal{P}(X_{1}+X_{2})\to\mathcal{P}X_{1}+\mathcal{P}X_{2}\qquad
g_{X_{1},X_{2}}(X^{\prime})=\begin{cases}X^{\prime}\cap X_{1}&\mbox{if
$X^{\prime}\cap X_{1}\neq\emptyset$}\\\
X^{\prime}&\mbox{otherwise}\end{cases}$

######  Proof 5.9.

We have to prove the following properties of $g$:

naturality:

let $f_{i}\colon X_{i}\to Y_{i}$, $X^{\prime}\subseteq X_{1}+X_{1}$. We
distinguish the following cases: if $X^{\prime}\cap X_{1}\neq\emptyset$, then

$\displaystyle(\mathcal{P}(f_{1})+\mathcal{P}(f_{2}))\circ
g_{X_{1},X_{2}}(X^{\prime})$
$\displaystyle=(\mathcal{P}(f_{1})+\mathcal{P}(f_{2}))(X^{\prime}\cap X_{1})$
$\displaystyle=\mathcal{P}(f_{1})(X^{\prime}\cap X_{1})$
$\displaystyle=f_{1}[X^{\prime}\cap X_{1}]$
$\displaystyle=g_{Y_{1},Y_{2}}(f_{1}[X^{\prime}\cap
X_{1}]+f_{2}[X^{\prime}\cap X_{2}])$
$\displaystyle=g_{Y_{1},Y_{2}}((f_{1}+f_{2})[X^{\prime}])$
$\displaystyle=g_{Y_{1},Y_{2}}\circ\mathcal{P}(f_{1}+f_{2})(X^{\prime})$

Note that the equality on the third line holds since $X^{\prime}\cap X_{1}$ is
non-empty and the same is true for $f_{1}[X^{\prime}\cap X_{1}]$.

If $X^{\prime}\cap X_{1}=\emptyset$, hence $X^{\prime}\subseteq X_{2}$, then

$\displaystyle(\mathcal{P}(f_{1})+\mathcal{P}(f_{2}))\circ
g_{X_{1},X_{2}}(X^{\prime})$
$\displaystyle=(\mathcal{P}(f_{1})+\mathcal{P}(f_{2}))(X^{\prime})$
$\displaystyle=\mathcal{P}(f_{2})(X^{\prime})$
$\displaystyle=f_{2}[X^{\prime}]$
$\displaystyle=g_{X_{1},X_{2}}(f_{2}[X^{\prime}])$
$\displaystyle=g_{X_{1},X_{2}}((f_{1}+f_{2})[X^{\prime}])$
$\displaystyle=g_{X_{1},X_{2}}\circ\mathcal{P}(f_{1}+f_{2})(X^{\prime})$

compatibility with $\eta$:

$g_{X_{1},X_{2}}\circ\eta_{X_{1}+X_{2}}=\eta_{X_{1}}+\eta_{X_{2}}$

Let $x\in X_{1}+X_{2}$. Then, since $g_{X_{1},X_{2}}$ is the identity on
singletons:

$\displaystyle g_{X_{1},X_{2}}\circ\eta_{X_{1}+X_{2}}(x)$
$\displaystyle=g_{X_{1},X_{2}}(\\{x\\})=\\{x\\}$

compatibility with $\mu$:

$g_{X_{1},X_{2}}\circ\mu_{X_{1}+X_{2}}=(\mu_{X_{1}}+\mu_{X_{2}})\circ
g_{TX_{1},TX_{2}}\circ Tg_{X_{1},X_{2}}$

Let $\mathcal{X}\subseteq\mathcal{P}(X_{1}+X_{2})$. We can split
$\mathcal{X}=\mathcal{X}_{1}+\mathcal{X}_{2}$, where
$\mathcal{X}_{1}=\\{X^{\prime}\in\mathcal{X}\mid X^{\prime}\cap
X_{1}\neq\emptyset\\}$ and $\mathcal{X}_{2}=\\{X^{\prime}\in\mathcal{X}\mid
X^{\prime}\cap X_{1}=\emptyset\\}\subseteq\mathcal{P}(X_{2})$. Note that
$\mathcal{X}_{1}\cap X_{1}=\\{X^{\prime}\cap X_{1}\mid
X^{\prime}\in\mathcal{X}_{1}\\}\subseteq\mathcal{P}(X_{1})$. We consider two
cases: if $\mathcal{X}_{1}\neq\emptyset$, we have that $\bigcup\mathcal{X}$
contains at least one element from $X_{1}$ and hence:

$\displaystyle g_{X_{1},X_{2}}\circ\mu_{X_{1}+X_{2}}(\mathcal{X})$
$\displaystyle=g_{X_{1},X_{2}}(\bigcup\mathcal{X})$
$\displaystyle=\left(\bigcup\mathcal{X}\right)\cap X_{1}$
$\displaystyle=\bigcup(\mathcal{X}\cap X_{1})$
$\displaystyle=\bigcup(\mathcal{X}_{1}\cap X_{1})$
$\displaystyle=(\mu_{X_{1}}+\mu_{X_{2}})(\mathcal{X}_{1}\cap X_{1})$
$\displaystyle=(\mu_{X_{1}}+\mu_{X_{2}})\circ
g_{\mathcal{P}(X_{1}),\mathcal{P}(X_{2})}((\mathcal{X}_{1}\cap
X_{1})+\mathcal{X}_{2})$ $\displaystyle=(\mu_{X_{1}}+\mu_{X_{2}})\circ
g_{\mathcal{P}(X_{1}),\mathcal{P}(X_{2})}\circ
g_{X_{1},X_{2}}[\mathcal{X}_{1}+\mathcal{X}_{2}]$
$\displaystyle=(\mu_{X_{1}}+\mu_{X_{2}})\circ
g_{\mathcal{P}(X_{1}),\mathcal{P}(X_{2})}\circ\mathcal{P}(g_{X_{1},X_{2}})(\mathcal{X})$

If instead $\mathcal{X}_{1}=\emptyset$, we have that $\bigcup\mathcal{X}$
contains no element from $X_{1}$ and $\mathcal{X}=\mathcal{X}_{2}$. Then:

$\displaystyle g_{X_{1},X_{2}}\circ\mu_{X_{1}+X_{2}}(\mathcal{X})$
$\displaystyle=g_{X_{1},X_{2}}\circ\mu_{X_{1}+X_{2}}(\mathcal{X}_{2})$
$\displaystyle=g_{X_{1},X_{2}}(\bigcup\mathcal{X}_{2})$
$\displaystyle=\bigcup\mathcal{X}_{2}$
$\displaystyle=(\mu_{X_{1}}+\mu_{X_{2}})(\mathcal{X}_{2})$
$\displaystyle=(\mu_{X_{1}}+\mu_{X_{2}})\circ
g_{\mathcal{P}(X_{1}),\mathcal{P}(X_{2})}(\mathcal{X}_{2})$
$\displaystyle=(\mu_{X_{1}}+\mu_{X_{2}})\circ
g_{\mathcal{P}(X_{1}),\mathcal{P}(X_{2})}\circ
g_{X_{1},X_{2}}[\mathcal{X}_{2}]$
$\displaystyle=(\mu_{X_{1}}+\mu_{X_{2}})\circ
g_{\mathcal{P}(X_{1}),\mathcal{P}(X_{2})}\circ\mathcal{P}(g_{X_{1},X_{2}})(\mathcal{X})$

well-behavedness:

First, note that here $\top=0$ and $\bot=1$.

  * •

$[\sup\circ\mathcal{P}f_{1},\top_{\mathcal{P}X_{2}}]\circ
g_{X_{1},X_{2}}=\sup\circ\mathcal{P}[f_{1},\top_{X_{2}}]$:

Let $X^{\prime}\subseteq X_{1}+X_{2}$. We distinguish three subcases.

    * –

If $X^{\prime}\cap X_{2}\neq\emptyset$, then

$\displaystyle([\sup\circ\mathcal{P}f_{1},\top_{\mathcal{P}X_{2}}]\circ
g_{X_{1},X_{2}})(X^{\prime})$
$\displaystyle=(\sup\circ\mathcal{P}f_{1})(X^{\prime}\cap X_{1})$
$\displaystyle=\sup f_{1}[X^{\prime}\cap X_{1}]$
$\displaystyle=\sup\\{f_{1}[X^{\prime}\cap
X_{1}]\cup\top_{X_{2}}[X^{\prime}\cap X_{2}]\\}$
$\displaystyle=\sup\left(\mathcal{P}[f_{1},\top_{X_{2}}](X^{\prime})\right)$

    * –

If $X^{\prime}=\emptyset$, then

$\displaystyle([\sup\circ\mathcal{P}f_{1},\top_{\mathcal{P}X_{2}}]\circ
g_{X_{1},X_{2}})(X^{\prime})$
$\displaystyle=\top_{\mathcal{P}X_{2}}(\emptyset)$ $\displaystyle=\top$
$\displaystyle=\sup(\emptyset)$
$\displaystyle=\sup([\mathcal{P}f_{1},\top_{X_{2}}](\emptyset))$
$\displaystyle=(\sup\circ[\mathcal{P}f_{1},\top_{X_{2}}])(X^{\prime})$

    * –

$X^{\prime}\cap X_{1}=\emptyset$ and $X^{\prime}\cap X_{1}\neq\emptyset$,
hence $X^{\prime}\subseteq X_{2}$. We can assume that
$X^{\prime}\neq\emptyset$.

$\displaystyle([\sup\circ\mathcal{P}f_{1},\top_{\mathcal{P}X_{2}}]\circ
g_{X_{1},X_{2}})(X^{\prime})$
$\displaystyle=\top_{\mathcal{P}X_{2}}(X^{\prime}\cap X_{2})$
$\displaystyle=\top$ $\displaystyle=\sup(\top_{X_{2}}(X^{\prime}\cap X_{2}))$
$\displaystyle=\sup([\mathcal{P}f_{1},\top_{X_{2}}](X^{\prime}\cap X_{2}))$
$\displaystyle=(\sup\circ[\mathcal{P}f_{1},\top_{X_{2}}])(X^{\prime})$

  * •

$[\bot_{\mathcal{P}X_{1}},\sup\circ\mathcal{P}f_{2}]\circ
g_{X_{1},X_{2}}=\sup\circ\mathcal{P}[\bot_{X_{1}},f_{2}]$:

Let $X^{\prime}\subseteq X_{1}+X_{2}$. We distinguish two subcases.

    * –

If $X^{\prime}\cap X_{1}\neq\emptyset$, then:

$\displaystyle([\bot_{\mathcal{P}X_{1}},\sup\circ\mathcal{P}f_{2}]\circ
g_{X_{1},X_{2}})(X^{\prime})$
$\displaystyle=\bot_{\mathcal{P}X_{1}}(X^{\prime}\cap X_{2})$
$\displaystyle=\bot$ $\displaystyle=\sup(\bot_{X_{1}}[X^{\prime}\cap
X_{1}]\cup f_{2}[X^{\prime}\cap X_{2}])$
$\displaystyle=(\sup\circ\mathcal{P}[\bot_{X_{1}},f_{1}])(X^{\prime})$

    * –

If $X^{\prime}\cup X_{1}=\emptyset$, hence $X^{\prime}\subseteq X_{2}$

$\displaystyle([\bot_{\mathcal{P}X_{1}},\sup\circ\mathcal{P}f_{2}]\circ
g_{X_{1},X_{2}})(X^{\prime})$
$\displaystyle=(\sup\circ\mathcal{P}f_{2})(X^{\prime})$
$\displaystyle=\sup(f_{2}[X^{\prime}])$
$\displaystyle=\sup(\bot_{X_{1}}[X^{\prime}\cap X]\cup f_{2}[X^{\prime}\cap
X_{2}])$
$\displaystyle=(\sup\circ\mathcal{P}[\bot_{X_{1}},f_{2}])(X^{\prime})$

  * •

$[\bot_{\mathcal{P}X_{1}},\top_{\mathcal{P}X_{2}}]\circ
g_{X_{1},X_{2}}=\sup\circ\mathcal{P}[\bot_{X_{1}},\top_{X_{2}}]$: Let
$X^{\prime}\subseteq X_{1}+X_{2}$. We distinguish three subcases:

    * –

If $X^{\prime}\cap X_{1}\neq\emptyset$, then

$\displaystyle([\bot_{\mathcal{P}X_{1}},\top_{\mathcal{P}X_{2}}]\circ
g_{X_{1},X_{2}})(X^{\prime})$
$\displaystyle=\bot_{\mathcal{P}X_{1}}(X^{\prime}\cap X_{1})$
$\displaystyle=\bot$ $\displaystyle=\sup(\bot_{X_{1}}[X^{\prime}\cap X_{1}])$
$\displaystyle=\sup(\bot_{X_{1}}[X^{\prime}\cap
X_{1}]\cup\top_{X_{2}}[X^{\prime}\cap X_{2}])$
$\displaystyle=(\sup\circ\mathcal{P}[\bot_{X_{1}},\top_{X_{2}}])(X^{\prime})$

    * –

If $X^{\prime}=\emptyset$, then

$\displaystyle([\bot_{\mathcal{P}X_{1}},\top_{\mathcal{P}X_{2}}]\circ
g_{X_{1},X_{2}})(X^{\prime})$
$\displaystyle=\top_{\mathcal{P}X_{2}}(\emptyset)$ $\displaystyle=\top$
$\displaystyle=\sup(\emptyset)$
$\displaystyle=(\sup\circ\mathcal{P}[\bot_{X_{1}},\top_{X_{2}}])(\emptyset)$
$\displaystyle=(\sup\circ\mathcal{P}[\bot_{X_{1}},\top_{X_{2}}])(X^{\prime})$

    * –

If $X^{\prime}\cap X_{2}\neq\emptyset$, hence $X^{\prime}\subseteq X_{2}$. We
can assume that $X^{\prime}\neq\emptyset$.

$\displaystyle([\bot_{\mathcal{P}X_{1}},\top_{\mathcal{P}X_{2}}]\circ
g_{X_{1},X_{2}})(X^{\prime})$
$\displaystyle=\top_{\mathcal{P}X_{2}}(X^{\prime}\cap X_{2})$
$\displaystyle=\top$ $\displaystyle=\sup(\top_{X_{2}}(X^{\prime}\cap X_{2}))$
$\displaystyle=\sup(\bot_{X_{1}}[X^{\prime}\cap
X_{1}]\cup\top_{X_{2}}[X^{\prime}\cap X_{2}])$
$\displaystyle=(\sup\circ\mathcal{P}[\bot_{X_{1}},\top_{X_{2}}])(X^{\prime})$

Let $T=\mathcal{S}$ be the subdistribution monad where
$\mathcal{S}(X)=\\{p\colon X\to[0,1]\mid\sum_{x\in X}p(x)\leq 1\\}$. Assume
that its evaluation map is $\mathit{ev}_{T}=\mathbb{E}$ for quantale
$\mathcal{V}={[0,\infty]_{\oplus}}$ (where we assume that
$p\cdot\infty=\infty$ if $p>0$ and $0$ otherwise). Then $g_{X_{1},X_{2}}$
below is a natural transformation that is compatible with unit and
multiplication of $T$ and is well-behaved.

$g_{X_{1},X_{2}}\colon\mathcal{S}(X_{1}+X_{2})\to\mathcal{S}X_{1}+\mathcal{S}X_{2}\qquad
g_{X_{1},X_{2}}(p)=\begin{cases}p|_{X_{1}}&\mbox{if $\textrm{supp}(p)\cap
X_{1}\neq\emptyset$}\\\ p|_{X_{2}}&\mbox{otherwise}\end{cases}$

######  Proof 5.10.

We have to prove the following properties of $g$:

naturality:

let $f_{i}\colon X_{i}\to Y_{i}$, $p\in\mathcal{S}(X_{1}+X_{1})$. We
distinguish the following cases: if $\textrm{supp}(p)\cap X_{1}\neq\emptyset$,
then for all $y\in Y_{1}$ we have that

$\displaystyle\left((\mathcal{S}(f_{1})+\mathcal{S}(f_{2}))\circ
g_{X_{1},X_{2}}(p)\right)(y)$
$\displaystyle=\left((\mathcal{S}(f_{1})+\mathcal{S}(f_{2}))(p|_{X_{1}})\right)(y)$
$\displaystyle=\left(\mathcal{S}(f_{1})(p|_{X_{1}})\right)(y)$
$\displaystyle=\sum_{y=f_{1}(x)}p|_{X_{1}}(x)$
$\displaystyle=\sum_{y=(f_{1}+f_{2})(x)}p|_{X_{1}}(x)$
$\displaystyle=\left(\mathcal{S}(f_{1}+f_{2})(p|_{X_{1}})\right)(y)$
$\displaystyle=\left(\mathcal{S}(f_{1}+f_{2})(p)\right)(y)$
$\displaystyle=(\mathcal{S}(f_{1}+f_{2})(p))|_{Y_{1}}(y)$
$\displaystyle=\left(g_{Y_{1},Y_{2}}\circ\mathcal{S}(f_{1}+f_{2})(p)\right)(y)$

For the remaining case, we have that for all $y\in Y_{2}$

$\displaystyle\left((\mathcal{S}(f_{1})+\mathcal{S}(f_{2}))\circ
g_{X_{1},X_{2}}(p)\right)(y)$
$\displaystyle=\mathcal{S}(f_{2})(p|_{X_{2}})(y)$
$\displaystyle=\sum_{y=f_{2}(x)}p|_{X_{2}}(x)$
$\displaystyle=\sum_{y=(f_{1}+f_{2})(x)}p_{X_{2}}(x)$
$\displaystyle=\left(\mathcal{S}(f_{1}+f_{2})(p|_{X_{2}})\right)(y)$
$\displaystyle=\left(\mathcal{S}(f_{1}+f_{2})(p)\right)(y)$
$\displaystyle=(\mathcal{S}(f_{1}+f_{2})(p))|_{Y_{2}}(y)$
$\displaystyle=\left(g_{Y_{1},Y_{2}}\circ\mathcal{S}(f_{1}+f_{2})(p)\right)(y)$

compatibility with $\eta$:

$g_{X_{1},X_{2}}\circ\eta_{X_{1}+X_{2}}=\eta_{X_{1}}+\eta_{X_{2}}$. Since
$g_{X_{1},X_{2}}$ is an identity when applied to Dirac distributions, we have
that:

$g_{X_{1},X_{2}}\circ\eta_{X_{1}+X_{2}}(x)=g_{X_{1},X_{2}}(\delta_{x})=\delta_{x}=\eta_{X_{1}}(x)$

compatibility with $\mu$:

$g_{X_{1},X_{2}}\circ\mu_{X_{1}+X_{2}}=(\mu_{X_{1}}+\mu_{X_{2}})\circ
g_{\mathcal{S}X_{1},\mathcal{S}X_{2}}\circ\mathcal{S}g_{X_{1},X_{2}}$. Let
$p\in\mathcal{S}\mathcal{S}(X_{1}+X_{2})$. Note that we can partition
$\textrm{supp}(p)=\mathcal{X}_{1}\cup\mathcal{X}_{2}$ in a way that
$\mathcal{X}_{1}=\\{\nu\in\mathcal{S}(X_{1}+X_{2})\mid\textrm{supp}(\nu)\cap
X_{1}\neq\emptyset\\}$ and
$\mathcal{X}_{2}=\\{\nu\in\mathcal{S}(X_{1}+X_{2})\mid\textrm{supp}(\nu)\cap
X_{1}=\emptyset\\}$. We consider two cases: if $\mathcal{X}_{1}\neq\emptyset$,
then $\textrm{supp}(\mu_{X_{1}+X_{2}}(p))\cap X_{1}\neq\emptyset$ and hence
for all $x\in X_{1}$, we have that:

$\displaystyle\left((g_{X_{1},X_{2}}\circ\mu_{X_{1}+X_{2}})(p)\right)(x)$
$\displaystyle=(\mu_{X_{1}+X_{2}}(p))|_{X_{1}}(x)$
$\displaystyle=\sum_{\nu\in\mathcal{S}(X_{1}+X_{2})}p(\nu)\nu|_{X_{1}}(x)$
$\displaystyle=\sum_{\nu\in\mathcal{X}_{1}}p(\nu)\nu|_{X_{1}}(x)$
$\displaystyle=\sum_{\nu\in\mathcal{X}_{1}}\left(\mathcal{S}(g_{X_{1},X_{2}})(p)\right)(\nu)\nu(x)$
$\displaystyle=\sum_{\nu\in\mathcal{S}(X_{1}+X_{2})}\left(\mathcal{S}g_{X_{1},X_{2}}(p)|_{\mathcal{S}X_{1}}\right)(\nu)\nu(x)$
$\displaystyle=\left((\mu_{X_{1}}+\mu_{X_{2}})\circ
g_{\mathcal{S}X_{1},\mathcal{S}X_{2}}\circ\mathcal{S}g_{X_{1},X_{2}}(p)\right)(x)$

Now, consider the case when $\textrm{supp}(\mu_{X_{1}+X_{2}}(p))\cap
X_{1}=\emptyset$. For all $x\in X_{2}$ we have that:

$\displaystyle\left((g_{X_{1},X_{2}}\circ\mu_{X_{1}+X_{2}})(p)\right)(x)$
$\displaystyle=(\mu_{X_{1}+X_{2}}(p))|_{X_{2}}(x)$
$\displaystyle=\sum_{\nu\in\mathcal{S}(X_{1}+X_{2})}p(\nu)\nu|_{X_{2}}(x)$
$\displaystyle=\sum_{\nu\in\mathcal{X}_{2}}p(\nu)\nu|_{X_{2}}(x)$
$\displaystyle=\sum_{\nu\in\mathcal{X}_{2}}p(\nu)\nu(x)$
$\displaystyle=\sum_{\nu\in\mathcal{X}_{2}}\left(\mathcal{S}(g_{X_{1},X_{2}})(p)\right)(\nu)\nu(x)$
$\displaystyle=\sum_{\nu\in\mathcal{S}(X_{1}+X_{2})}\left(\mathcal{S}(g_{X_{1},X_{2}})(p)|_{\mathcal{S}X_{2}}\right)(\nu)\nu(x)$
$\displaystyle=\sum_{\nu\in\mathcal{S}(X_{1}+X_{2})}\left(\mathcal{S}(g_{X_{1},X_{2}})(p)|_{\mathcal{S}X_{2}}\right)(\nu)\nu(x)$
$\displaystyle=\left((\mu_{X_{1}}+\mu_{X_{2}})\circ
g_{\mathcal{S}X_{1},\mathcal{S}X_{2}}\circ\mathcal{S}g_{X_{1},X_{2}}(p)\right)(x)$

well-behavedness:

First, note that here $\top=0$ and $\bot=\infty$.

  * •

$[\mathbb{E}\circ{\mathcal{S}}f_{1},\top_{{\mathcal{S}}X_{2}}]\circ
g_{X_{1},X_{2}}=\mathbb{E}\circ{\mathcal{S}}[f_{1},\top_{X_{2}}]$: Let $p\in
S(X_{1}+X_{2})$. We first consider the case when $\textrm{supp}(p)\cap
X_{1}\neq\emptyset$. We have that:

$\displaystyle[\mathbb{E}\circ{\mathcal{S}}f_{1},\top_{{\mathcal{S}}X_{2}}]\circ
g_{X_{1},X_{2}}(p)$
$\displaystyle=[\mathbb{E}\circ{\mathcal{S}}f_{1},\top_{{\mathcal{S}}X_{2}}](p|_{X_{1}})$
$\displaystyle=\mathbb{E}\circ{\mathcal{S}}f_{1}(p|_{X_{1}})$
$\displaystyle=\sum_{y\in\mathcal{V}}y\left(\sum_{y=f_{1}(x)}p(x)\right)$
$\displaystyle=\left(\sum_{y\in\mathcal{V}}y\left(\sum_{y=f_{1}(x)}p(x)\right)\right)+0\left(\sum_{0=\top_{X_{2}}(x)}p(x)\right)$
$\displaystyle=\sum_{y\in\mathcal{V}}y\left(\sum_{y=[f_{1},\top_{X_{2}}](x)}p(x)\right)$
$\displaystyle=\mathbb{E}\circ\mathcal{S}[f_{1},\top_{X_{2}}]$

Now, consider the case when $\textrm{supp}(p)=\emptyset$. We have that:

$\displaystyle[\mathbb{E}\circ{\mathcal{S}}f_{1},\top_{{\mathcal{S}}X_{2}}]\circ
g_{X_{1},X_{2}}(p)$
$\displaystyle=[\mathbb{E}\circ{\mathcal{S}}f_{1},\top_{{\mathcal{S}}X_{2}}](p|_{X_{2}})$
$\displaystyle=\top$ $\displaystyle=0$
$\displaystyle=\mathbb{E}\circ\mathcal{S}[f_{1},\top_{X_{2}}](p)$

Finally, consider the case when $\textrm{supp}(p)\cap X_{1}=\emptyset$, but
$\textrm{supp}(p)\neq\emptyset$. We have that:

$\displaystyle[\mathbb{E}\circ{\mathcal{S}}f_{1},\top_{{\mathcal{S}}X_{2}}]\circ
g_{X_{1},X_{2}}(p)$
$\displaystyle=[\mathbb{E}\circ{\mathcal{S}}f_{1},\top_{{\mathcal{S}}X_{2}}](p|_{X_{2}})$
$\displaystyle=\top$ $\displaystyle=0$
$\displaystyle=\sum_{y\in\mathcal{V}}y\left(\sum_{y=\top_{X_{2}}(x)}p(x)\right)$
$\displaystyle=\mathbb{E}\circ\mathcal{S}(\top_{X_{2}})(p)$
$\displaystyle=\mathbb{E}\circ\mathcal{S}[f_{1},\top_{X_{2}}](p)$

  * •

$[\bot_{\mathcal{S}X_{1}},\mathbb{E}\circ\mathcal{S}f_{2}]\circ
g_{X_{1},X_{2}}=\mathbb{E}\circ\mathcal{S}[\bot_{X_{1}},f_{2}]$: Let $p\in
S(X_{1}+X_{2})$. Firstly, consider the case when $\textrm{supp}(p)\cap
X_{1}\neq\emptyset$. In such a case, we have

$\displaystyle[\bot_{\mathcal{S}X_{1}},\mathbb{E}\circ\mathcal{S}f_{2}]\circ
g_{X_{1},X_{2}}(p)$
$\displaystyle=[\bot_{\mathcal{S}X_{1}},\mathbb{E}\circ\mathcal{S}f_{2}](p|_{X_{1}})$
$\displaystyle=\bot$ $\displaystyle=\infty$
$\displaystyle=\infty+\left(\sum_{y\in\mathbb{R}}y\left(\sum_{y=[\bot_{X_{1}},f_{2}](x)}p(x)\right)\right)$
$\displaystyle=\left(\sum_{\infty=[\bot_{X_{1}},f_{2}](x)}p(x)\right)+\left(\sum_{y\in\mathbb{R}}y\left(\sum_{y=[\bot_{X_{1}},f_{2}](x)}p(x)\right)\right)$
$\displaystyle=\sum_{y\in[0,+\infty]}y\left(\sum_{y=[\bot_{X_{1}},f_{2}](x)}p(x)\right)$
$\displaystyle=\mathbb{E}\circ\mathcal{S}[\bot_{X_{1}},f_{2}](p)$

If $\textrm{supp}(p)=\emptyset$, then we have that

$\displaystyle[\bot_{\mathcal{S}X_{1}},\mathbb{E}\circ\mathcal{S}f_{2}]\circ
g_{X_{1},X_{2}}(p)$
$\displaystyle=[\bot_{\mathcal{S}X_{1}},\mathbb{E}\circ\mathcal{S}f_{2}](p|_{X_{2}})$
$\displaystyle=\mathbb{E}\circ\mathcal{S}f_{2}(p|_{X_{2}})$ $\displaystyle=0$
$\displaystyle=\mathbb{E}\circ\mathcal{S}[\bot_{X_{1}},f_{2}](p)$

Finally, consider the case when $\textrm{supp}(p)\cap X_{1}=\emptyset$, but
$\textrm{supp}(p)\neq\emptyset$. Then, we have that

$\displaystyle[\bot_{\mathcal{S}X_{1}},\mathbb{E}\circ\mathcal{S}f_{2}]\circ
g_{X_{1},X_{2}}(p)$
$\displaystyle=[\bot_{\mathcal{S}X_{1}},\mathbb{E}\circ\mathcal{S}f_{2}](p|_{X_{2}})$
$\displaystyle=\mathbb{E}\circ\mathcal{S}f_{2}(p|_{X_{2}})$
$\displaystyle=\sum_{y\in\mathcal{V}}y\left(\sum_{y=f_{2}(x)}p|_{X_{2}}(x)\right)$
$\displaystyle=\sum_{y\in\mathcal{V}}y\left(\sum_{y=[\bot_{X_{1}},f_{2}](x)}p(x)\right)$
$\displaystyle=\mathbb{E}\circ\mathcal{S}[\bot_{X_{1}},f_{2}](p)$

  * •

$[\bot_{\mathcal{S}X_{1}},\top_{\mathcal{S}X_{2}}]\circ
g_{X_{1},X_{2}}=\mathbb{E}\circ\mathcal{S}[\bot_{X_{1}},\top_{X_{2}}]$: Let
$p\in\mathcal{S}(X_{1}+X_{2})$. First, consider the case when
$\textrm{supp}(p)\cap X_{1}\neq\emptyset$. We have that

$\displaystyle[\bot_{\mathcal{S}X_{1}},\top_{\mathcal{S}X_{2}}]\circ
g_{X_{1},X_{2}}(p)$
$\displaystyle=[\bot_{\mathcal{S}X_{1}},\top_{\mathcal{S}X_{2}}](p|_{X_{1}})$
$\displaystyle=\bot_{\mathcal{S}X_{1}}(p|_{X_{1}})$ $\displaystyle=\infty$
$\displaystyle=\infty+0$
$\displaystyle=\left(\sum_{\infty=[\bot_{X_{1}},\top_{X_{2}}](x)}p(x)\right)+\left(\sum_{0=[\bot_{X_{1}},\top_{X_{2}}](x)}p(x)\right)$
$\displaystyle=\sum_{y\in[0,+\infty]}y\left(\sum_{y=[\bot_{X_{1}},\top_{X_{2}}](x)}p(x)\right)$
$\displaystyle=\mathbb{E}\circ\mathcal{S}[\bot_{X_{1}},\top_{X_{2}}](p)$

Then, consider a case when $\textrm{supp}(p)=\emptyset$.

$\displaystyle[\bot_{\mathcal{S}X_{1}},\top_{\mathcal{S}X_{2}}]\circ
g_{X_{1},X_{2}}(p)$
$\displaystyle=[\bot_{\mathcal{S}X_{1}},\top_{\mathcal{S}X_{2}}](p|_{X_{2}})$
$\displaystyle=\top_{\mathcal{S}X_{2}}(p|_{X_{2}})$ $\displaystyle=0$
$\displaystyle=\mathbb{E}\circ\mathcal{S}[\bot_{X_{1}},\top_{X_{2}}](p)$

Finally, consider a case when $\textrm{supp}(p)\cap X_{1}=\emptyset$ and
$\textrm{supp}(p)\cap X_{2}\neq\emptyset$. We have that

$\displaystyle[\bot_{\mathcal{S}X_{1}},\top_{\mathcal{S}X_{2}}]\circ
g_{X_{1},X_{2}}(p)$
$\displaystyle=[\bot_{\mathcal{S}X_{1}},\top_{\mathcal{S}X_{2}}](p|_{X_{2}})$
$\displaystyle=\top_{\mathcal{S}X_{2}}(p|_{X_{2}})$ $\displaystyle=0$
$\displaystyle=\left(\sum_{y=[\bot_{X_{1}},\top_{X_{2}}](x)}p(x)\right)$
$\displaystyle=\mathbb{E}\circ\mathcal{S}[\bot_{X_{1}},\top_{X_{2}}](p)$

It is left to show that the EM-law $\zeta\colon FT\Rightarrow FT$ lifts to
$\zeta\colon\overline{F}\,\overline{T}\Rightarrow\overline{T}\,\overline{F}$,
where $\overline{F}=K_{\Lambda^{F}}$, $\overline{T}=K_{\Lambda^{T}}$ where
$\Lambda^{T}=\\{\mathit{ev}_{T}\\}$, where the evaluation maps are obtained as
described earlier. We namely prove that its components are all non-expansive,
i.e., $\mathcal{V}\textrm{-}\mathsf{Graph}$-morphisms, commutativity is
already known. Using the previous results we obtain:

$\overline{F}\,\overline{T}\stackrel{{\scriptstyle(1)}}{{\sqsubseteq}}\overline{TF}\stackrel{{\scriptstyle(2)}}{{\Rightarrow}}\overline{FT}\stackrel{{\scriptstyle(3)}}{{=}}\overline{F}\,\overline{T}$

(1)

follows from the inequality in Section 4.2. This implies that the identity
$\mathrm{id}_{TFX}\colon\overline{T}\,\overline{F}X\to\overline{TF}X$ is non-
expansive (a $\mathcal{V}\textrm{-}\mathsf{Graph}$-morphism), resulting in the
natural transformation
$\overline{T}\,\overline{F}\stackrel{{\scriptstyle\mathrm{id}}}{{\Rightarrow}}\overline{TF}$.

(2)

is implied by the results of this section (Section 5.2, Section 5.2)

(3)

is guaranteed by the fact that $\overline{FT}=\overline{F}\,\overline{T}$ if
$F$ is polynomial (and we have suitable evaluation maps), hence
compositionality holds (4.6)

##  6 Case Studies

We now consider two case studies and show how up-to techniques can help
concretely to show upper bounds for behavioural distances via appropriate
witnesses. Note that both case studies rely on a set of evaluation maps
$\Lambda^{F}$ as opposed to a singleton evaluation map and would hence not be
directly realizable in the Wasserstein approach [bkp:up-to-behavioural-
metrics-fibrations-journal].

We will now show a property of the up-to function $u$ that is closely related
to the fact that under certain conditions the Kantorovich lifting is always
bounded by the Wasserstein lifting, as shown in [bbkk:coalgebraic-behavioral-
metrics]. The requirement is part of the notion of a well-behaved evaluation
function introduced there.

######  Proposition 6.1.

Let $(Y,a,c)$ be a bialgebra for $F,T$, $\mathit{ev}_{T}$ an evaluation map
for $T$ and let $u$ be the up-to function (as in Section 5.1). Furthermore
assume that $\colon Y\times Y\to\mathcal{V}$ is an object of
$\mathcal{V}\textrm{-}\mathsf{Graph}$ and $t\in T(Y\times Y)$. Then:

$u(d)(a(T\pi_{1}(t),a(T\pi_{2}(t)))\sqsupseteq\mathit{ev}_{T}\circ Td(t)$

whenever

$d_{\mathcal{V}}\circ(\mathit{ev}_{T}\times\mathit{ev}_{T})\circ\langle
T\pi^{\prime}_{1},T\pi^{\prime}_{2}\rangle\sqsupseteq\mathit{ev}_{T}\circ
Td_{\mathcal{V}}.$ (4)

where $\pi_{i}\colon Y\times Y\to Y$ and
$\pi^{\prime}_{i}\colon\mathcal{V}\times\mathcal{V}\to\mathcal{V}$.

######  Proof 6.2.

$\displaystyle u(d)(a(T\pi_{1}(t),a(T\pi_{2}(t)))$ $\displaystyle=$
$\displaystyle\bigsqcup_{a(t_{i})=a(T\pi_{i}(t))}\overline{T}(d)(t_{1},t_{2})$
$\displaystyle\sqsupseteq$
$\displaystyle\overline{T}(d)(T\pi_{1}(t),T\pi_{1}(t))$ $\displaystyle=$
$\displaystyle\bigsqcap_{f\in\gamma_{Y}(d)}d_{\mathcal{V}}(\mathit{ev}_{T}\circ
Tf\circ T\pi_{1}(t),\mathit{ev}_{T}\circ Tf\circ T\pi_{2}(t))$
$\displaystyle\sqsupseteq$ $\displaystyle\mathit{ev}_{T}\circ Td(t)$

The last inequality follows directly from [bbkk:coalgebraic-behavioral-
metrics, Lemma 5.25] whenever Condition (4) holds. Note that in
[bbkk:coalgebraic-behavioral-metrics] the quantale is $\mathcal{V}$ and
$d_{\mathcal{V}}$ (called $d_{e}$ there) is assumed to be symmetric, but
neither assumption is used in the proof.

######  Corollary 6.3.

In the setting of Proposition 6.1 assume that $Y=TX$, $a=\mu_{X}$ and
$\mathcal{V}=[0,1]$. Furthermore consider the monad $T=\mathcal{P}$
($T=\mathcal{D}$). Then the evaluation map $\mathit{ev}_{T}=\sup$
($\mathit{ev}_{T}=\mathbb{E}$) satisfies Condition (4) and hence we obtain:

  * •

$T=\mathcal{P}$:

$u(d)(\bigcup_{i\in I}X_{i},\bigcup_{i\in I}Y_{i})\leq\sup_{i\in
I}d(X_{i},Y_{i})$

whenever $X_{i},Y_{i}\subseteq X$, $i\in I$.

  * •

$T=\mathcal{D}$:

$u(d)(\sum_{i\in I}r_{i}\cdot p_{i},\sum_{i\in I}r_{i}\cdot
q_{i})\leq\sum_{i\in I}r_{i}\cdot d(p_{i},q_{i})$

whenever $p_{i},q_{i}\in\mathcal{D}(X)$, $i\in I$.

######  Proof 6.4.

We first prove Condition (4) in both cases ($T=\mathcal{P}$, $T=\mathcal{D}$):

  * •

$T=\mathcal{P}$: Let $t\in T(\mathcal{V}\times\mathcal{V})$, i.e.,
$t\subseteq[0,1]\times[0,1]$ respectively $t=\\{(s_{i},r_{i})\mid i\in
I,r_{i},s_{i}\in[0,1]\\}$. Then

$\displaystyle
d_{\mathcal{V}}\circ(\mathit{ev}_{T}\times\mathit{ev}_{T})\circ\langle
T\pi^{\prime}_{1},T\pi^{\prime}_{2}\rangle(t)$ $\displaystyle=$ $\displaystyle
d_{\mathcal{V}}(\mathit{ev}_{T}(T\pi^{\prime}_{1}(t)),\mathit{ev}_{T}(T\pi^{\prime}_{2}(t)))$
$\displaystyle=$ $\displaystyle\sup_{i\in I}r_{i}\ominus\sup_{i\in I}s_{i}$
$\displaystyle\leq$ $\displaystyle\sup_{i\in I}(r_{i}\ominus s_{i})$
$\displaystyle=$ $\displaystyle\mathit{ev}_{T}\circ Td_{\mathcal{V}}(t).$

  * •

$T=\mathcal{D}$: Let $t\in T(\mathcal{V}\times\mathcal{V})$, i.e.,
$t\colon[0,1]\times[0,1]\to[0,1]$ is a probability distribution respectively
$t=\sum_{i\in I}p_{i}\cdot(s_{i},r_{i})$, written as a formal sum where
$p_{i},r_{i},s_{i}\in[0,1]$ and $\sum_{i\in I}p_{i}=1$. Then

$\displaystyle
d_{\mathcal{V}}\circ(\mathit{ev}_{T}\times\mathit{ev}_{T})\circ\langle
T\pi^{\prime}_{1},T\pi^{\prime}_{2}\rangle(t)$ $\displaystyle=$ $\displaystyle
d_{\mathcal{V}}(\mathit{ev}_{T}(T\pi^{\prime}_{1}(t)),\mathit{ev}_{T}(T\pi^{\prime}_{2}(t)))$
$\displaystyle=$ $\displaystyle\sum_{i\in I}p_{i}\cdot r_{i}\ominus\sum_{i\in
I}p_{i}\cdot s_{i}$ $\displaystyle\leq$ $\displaystyle\sum_{i\in
I}p_{i}\cdot(r_{i}\ominus s_{i})$ $\displaystyle=$
$\displaystyle\mathit{ev}_{T}\circ Td_{\mathcal{V}}(t).$

Finally, we spell out the inequalities:

  * •

$T=\mathcal{P}$: Let $t\in T(TX\times TX)$, i.e.,
$t\subseteq\mathcal{P}(X)\times\mathcal{P}(X)$ respectively
$t=\\{(X_{i},Y_{i})\mid i\in I,X_{i},Y_{i}\subseteq X\\}$. Then

$\displaystyle u(d)(\bigcup_{i\in I}X_{i},\bigcup_{i\in I}Y_{i})$
$\displaystyle=$ $\displaystyle
u(d)(\mu_{X}(T\pi_{1}(t)),\mu_{X}(T\pi_{2}(t)))$ $\displaystyle\leq$
$\displaystyle\mathit{ev}_{T}\circ Td(t)$ $\displaystyle=$
$\displaystyle\sup_{i\in I}d(X_{i},Y_{i})$

  * •

$T=\mathcal{D}$: Let $t\in T(TX\times TX)$, i.e.,
$t\colon\mathcal{D}(X)\times\mathcal{D}(X)\to[0,1]$ is a probability
distribution respectively $t=\sum_{i\in I}r_{i}\cdot(p_{i},q_{i})$, written as
a formal sum where $r_{i}\in[0,1]$ with $\sum_{i\in I}r_{i}=1$,
$p_{i},q_{i}\in\mathcal{D}(X)$. Then

$\displaystyle u(d)(\sum_{i\in I}r_{i}\cdot p_{i},\sum_{i\in I}r_{i}\cdot
q_{i})$ $\displaystyle=$ $\displaystyle
u(d)(\mu_{X}(T\pi_{1}(t)),\mu_{X}(T\pi_{2}(t)))$ $\displaystyle\leq$
$\displaystyle\mathit{ev}_{T}\circ Td(t)$ $\displaystyle=$
$\displaystyle\sup_{i\in I}r_{i}\cdot d(p_{i},q_{i})$

###  6.1 Probabilistic Automata

We consider a standard directed trace metrics for probabilistic automata as
introduced in [jss:trace-determinization-journal]. We take the functor
$F=[0,1]\times\\_^{A}$ (“machine functor”), monad $T=\mathcal{D}$ and quantale
$\mathcal{V}={[0,1]_{\oplus}}$. Furthermore we use expectation ($\mathbb{E}$)
as evaluation map for $T$ and as evaluation maps for the functor $F$ we take
$\mathit{ev}_{*}$ mapping to the first component and $\mathit{ev}_{a}$ (for
each $a\in A$) with $\mathit{ev}_{a}(r,g)=g(a)$. These evaluation maps are of
the type described in Section 4.3.

Given an Eilenberg-Moore coalgebra $c\colon X\to FTX$ (more concretely:
$c\colon X\to[0,1]\times\mathcal{D}X^{A}$) and its determinization
$c^{\\#}\colon TX\to FTX$, the behavioural distance on $TX$ arises as the
greatest fixpoint (in the quantale order) of the map
$\textrm{beh}=(c^{\\#})^{*}\circ\bar{F}$ defined in Section 5.1.

By unravelling the fixpoint equation one can see that it coincides with the
directed trace metric on probability distributions that is defined as follows:
for each state $x\in X$ let $\mathit{tr}_{x}\colon A^{*}\to[0,1]$ be a map
that assigns to each word (trace) $w\in A^{*}$ the expected payoff for this
word when read from $x$, where the payoff of a state $x^{\prime}$ is
$\pi_{1}(c(x^{\prime}))$. Then

$\nu\textrm{beh}(p,q)=\sup_{w\in A^{*}}\big{(}\sum\nolimits_{x\in
X}\mathit{tr}_{x}(w)\cdot q(x)\ominus\sum\nolimits_{x\in
X}\mathit{tr}_{x}(w)\cdot p(x)\big{)}$

If $p,q$ are Dirac distributions $\delta_{x},\delta_{y}$, we have:
$\nu\textrm{beh}(\delta_{x},\delta_{y})=\sup_{w\in
A^{*}}(\mathit{tr}_{y}(w)\ominus\mathit{tr}_{x}(w))$.

The proof techniques elaborated in Section 5.1 apply and we explain how they
can be exploited via an example.

######  Example 6.5.

For this concrete example we fix the label set as a singleton: $A=\\{a\\}$.
Consider the coalgebra with states $X=\\{x,x^{\prime},y\\}$ drawn below on the
left. The payoff is written next to each state.

$y$$\nicefrac{{1}}{{2}}$$\bullet$$x$$\nicefrac{{1}}{{2}}$$\bullet$$x^{\prime}$$1$$\bullet$$a$$1$$a$$\nicefrac{{1}}{{2}}$$\nicefrac{{1}}{{2}}$$a$$1$

$\epsilon$ $a$ $aa$ $aaa$ … $x$ $\nicefrac{{1}}{{2}}$ $\nicefrac{{3}}{{4}}$
$\nicefrac{{7}}{{8}}$ $\nicefrac{{15}}{{16}}$ … $y$ $\nicefrac{{1}}{{2}}$
$\nicefrac{{1}}{{2}}$ $\nicefrac{{1}}{{2}}$ $\nicefrac{{1}}{{2}}$ …

Here, the trace map has the values for states $x,y$ given in the table above
on the right, leading to the behavioural distance
$\nu\mathrm{beh}(\delta_{x},\delta_{y})=\nicefrac{{1}}{{2}}$ (the supremum of
all differences).

Determinizing the probabilistic automaton above leads to an automaton with
infinite state space, even if we only consider the reachable states (which are
probability distributions):

$1\cdot y$$\nicefrac{{1}}{{2}}$$a$$1\cdot
x$$\nicefrac{{1}}{{2}}$$\nicefrac{{1}}{{2}}\cdot x+\nicefrac{{1}}{{2}}\cdot
x^{\prime}$$\nicefrac{{3}}{{4}}$$\nicefrac{{1}}{{4}}\cdot
x+\nicefrac{{3}}{{4}}\cdot x^{\prime}$$\nicefrac{{7}}{{8}}$$\dots$$a$$a$$a$

Our aim is now to define a witness distance of type $d\colon TX\times
TX\to[0,1]$ that is a post-fixpoint up-to in the quantale order and a pre-
fixpoint for the order on the reals ($d\geq\mathrm{beh}(u(d))$). From this we
can infer that $\nu\mathrm{beh}\leq d$, obtaining an upper bound. We set
$d(1\cdot x,1\cdot y)=\nicefrac{{1}}{{2}}$, $d(1\cdot x^{\prime},1\cdot
y)=\nicefrac{{1}}{{2}}$ and $d(p,q)=1$ for all other pairs of probability
distributions $p,q$. We now show that $d$ is a pre-fixpoint of $\mathrm{beh}$
in the order on the reals, i.e., our aim is to prove for all $p,q$ that
$d(p,q)\geq\mathrm{beh}(u(d))(p,q)$. This is obvious for the cases where
$d(p,q)=1$, hence only two cases remain:

  * •

If $p=1\cdot x$, $q=1\cdot y$, we have:

$\displaystyle\mathrm{beh}(u(d))(1\cdot x,1\cdot y)$
$\displaystyle=\max\\{u(d)(\nicefrac{{1}}{{2}}\cdot x+\nicefrac{{1}}{{2}}\cdot
x^{\prime},y),|\nicefrac{{1}}{{2}}-\nicefrac{{1}}{{2}}|\\}$
$\displaystyle=u(d)(\nicefrac{{1}}{{2}}\cdot x+\nicefrac{{1}}{{2}}\cdot
x^{\prime},y)$ $\displaystyle\leq\nicefrac{{1}}{{2}}\cdot d(1\cdot x,1\cdot
y)+\nicefrac{{1}}{{2}}\cdot d(1\cdot x^{\prime},1\cdot y)$
$\displaystyle=\nicefrac{{1}}{{2}}\cdot\nicefrac{{1}}{{2}}+\nicefrac{{1}}{{2}}\cdot\nicefrac{{1}}{{2}}=\nicefrac{{1}}{{2}}=d(1\cdot
x,1\cdot y)$

  * •

The case $p=1\cdot x^{\prime}$, $q=1\cdot y$ can be shown analogously.

We are using the following inequalities: (i) $u(d)(p,q)\leq d(p,q)$ (follows
from the definition of $u$); (ii) $u(d)(r_{1}\cdot p_{1}+r_{2}\cdot
p_{2},r_{1}\cdot q_{1}+r_{2}\cdot q_{2})\leq r_{1}\cdot
d(p_{1},q_{1})+r_{2}\cdot d(p_{2},q_{2})$ (metric congruence, Corollary 6.3 in
the appendix). This concludes the argument.

Note that here up-to techniques in fact allow us to consider finitary
witnesses for bounds for behavioural distances, even when the determinized
coalgebra has an infinite state space.

###  6.2 Transition Systems with Exceptions

Next, we consider a case study involving the coproduct, in particular the
polynomial functor $F=[0,1]+(-)^{A}$ and the monad $T=\mathcal{P}$ with
evaluation map $\sup$. In a coalgebra of type $c\colon X\to FTX$ a state can
either perform transitions or terminate with some output value taken from the
interval $[0,1]$, in applications this value could for example be considered
as the severity of the error encountered upon terminating a computation. Hence
the (directed) distance of two states $x,y$ can intuitively be interpreted as
measuring how much worse the errors reached from a state $y$ are compared to
the errors from $x$.

Note that a state can also terminate without an exception by transitioning to
the empty set. Due to the asymmetry in the distributive law for the coproduct,
a state $X_{0}\in\mathcal{P}(X)$ in the determinized automaton $c^{\\#}$ will
throw an exception as long as one of the elements $x\in X_{0}$ throws an
exception ($c[X_{0}]\cap[0,1]\neq\emptyset$). In this case
$c^{\\#}(X_{0})=\sup c[X_{0}]\cap[0,1]$. And it performs a transition if all
states in $X_{0}$ do so in the original coalgebra.

The behavioural distance on $TX$ obtained as the greatest fixpoint (in the
quantale order) of $\mathrm{beh}$ can be characterized as follows: for a set
of states $X_{0}\subseteq X$ and a word $w\in A^{*}$ let $\emph{ec}(X_{0},w)$
be the length of the least prefix which causes an exception when starting in
$X_{0}$ (undefined if there are no exceptions) and let
$E(X_{0},w)\subseteq[0,1]$ be the set of exception values reached by that
prefix. We define a distance
$d^{E}_{w}\colon\mathcal{P}X\times\mathcal{P}X\to[0,1]$ as
$d^{E}_{w}(X_{1},X_{2})=0$ if $\emph{ec}(X_{2},w)$ is undefined,
$d^{E}_{w}(X_{1},X_{2})=1$ if $\emph{ec}(X_{1},w)$ is undefined and
$\emph{ec}(X_{2},w)$ defined. In the case where both are defined we set