theoremTheorem[section] lemma[theorem]Lemma definition[theorem]Definition
proposition[theorem]Proposition corollary[theorem]Corollary
example[theorem]Example remark[theorem]Remark

# A Monoidal View on Fixpoint Checks

Paolo Baldan  Università di Padova, Italy<EMAIL_ADDRESS>,  Richard
Eggert  Universität Duisburg-Essen, Germany<EMAIL_ADDRESS>,
Barbara König  Universität Duisburg-Essen, Germany<EMAIL_ADDRESS>,  Timo Matt  Universität Duisburg-Essen, Germany  and  Tommaso Padoan
Università di Trieste, Italy<EMAIL_ADDRESS>
###### Abstract.

Fixpoints are ubiquitous in computer science as they play a central role in
providing a meaning to recursive and cyclic definitions. Bisimilarity,
behavioural metrics, termination probabilities for Markov chains and
stochastic games are defined in terms of least or greatest fixpoints. Here we
show that our recent work which proposes a technique for checking whether the
fixpoint of a function is the least (or the largest) admits a natural
categorical interpretation in terms of gs-monoidal categories. The technique
is based on a construction that maps a function to a suitable approximation.
The compositionality properties of this mapping are naturally interpreted as a
gs-monoidal functor. This guides the development of a tool, called UDEfix that
allows us to build functions (and their approximations) like a circuit out of
basic building blocks and subsequently perform the fixpoints checks. We also
show that a slight generalisation of the theory allows one to treat a new
relevant case study: coalgebraic behavioural metrics based on Wasserstein
liftings.

Partially supported by the DFG project SpeQt (project number 434050016) and by
the Ministero dell’Universtà e della Ricerca Scientifica of Italy, under Grant
No. 201784YSZ5, PRIN2017 – ASPRA, and by project iNEST, No. J43C22000320006.

##  1\. Introduction

inline]B: Review 3 $\leadsto$ “To overcome this potential problem the
connection to graphs and graph transformations should be made more clear by
the authors in the paper.” B: I added a few sentences to the beginning of the
introduction.

Graph compositionality has always been an important part of the theory of
graph rewriting. For instance, one way to explain the double-pushout approach
[eps:gragra-algebraic] is to view the graph to be rewritten as a composition
of a left-hand side and a context, then compose the context with the right-
hand side to obtain the result of the rewriting step.

Several algebras have been proposed for a compositional view on graphs, see
for instance [bc:graph-expressions, k:hypergraph-construction-journal,
bk:axiomatization-graphs]. For the compositional modelling of graphs and
graph-like structures it has in particular proven useful to use the notion of
monoidal categories [ml:categories], i.e., categories equipped with a tensor
product. There are several variants of such categories, such as gs-monoidal
categories, that have been shown to be suitable for specifying term graph
rewriting (see e.g. [g:concurrent-term-rewriting, gh:inductive-graph]). In
essence gs-monoidal categories describe graph-like structures with dedicated
input and output interfaces, operators for disjoint union (tensor),
duplication and termination of wires, quotiented by the axioms satisfied by
these operators. Particularly useful are gs-monoidal functors that preserve
such operators and hence naturally describe compositional operations.

We show that gs-monoidal categories and the composition concepts that come
with them can be fruitfully used in a scenario that – at first sight – might
seem quite unrelated: methods for fixpoints checks. In particular, we build
upon [bekp:fixpoint-theory-upside-down, BEKP:FTUD-journal] where a theory is
proposed for checking whether a fixpoint of a given function is the least
(greatest) fixpoint. The theory applies to a variety of fairly diverse
application scenarios, such as bisimilarity [s:bisimulation-coinduction],
behavioural metrics [dgjp:metrics-labelled-markov, b:prob-bisimilarity-
distances, cbw:complexity-prob-bisimilarity, bbkk:coalgebraic-behavioral-
metrics], termination probabilities for Markov chains [bk:principles-mc] and
simple stochastic games [c:algorithms-ssg]. Such theory applies to non-
expansive functions of the kind $f\colon\mathbb{M}^{Y}\to\mathbb{M}^{Y}$,
where $\mathbb{M}$ is a set of values and $Y$ is a finite set. More precisely,
$\mathbb{M}$ is an MV-chain, i.e., a totally ordered complete lattice endowed
with suitable operations of sum and complement, a prototypical example being
the interval $[0,1]$ with truncated sum.

The rough idea consists in mapping such functions to corresponding
approximations, whose fixpoints can be computed effectively and give
information on the fixpoints of the original function.

Here we show that the approximation framework and its compositionality
properties can be naturally interpreted in categorical terms. This is done by
introducing two gs-monoidal categories in which the concrete functions
respectively their approximations live as arrows, together with a gs-monoidal
functor, called $\\#$, mapping one to the other. Besides shedding further
light on the theoretical approximation framework of [BEKP:FTUD-journal], this
view guided the realisation of a tool, called UDEfix that allows to build
functions (and their approximations) like a circuit out of basic building
blocks and subsequently perform the fixpoints checks.

The function characterising the system to be checked is viewed as a
(hyper)graph whose edges represent some basic building blocks. On the one
hand, the graphical interpretation naturally combines with the underlying
theory which builds the approximation of a complex function compositionally
out of the approximation of the basic components. On the other hand, it leads
to an intuitive visual representation which inspires the development of the
tool UDEfix.

We also show that the functor $\\#$ can be extended to deal with functions
$f\colon\mathbb{M}^{Y}\to\mathbb{M}^{Y}$, where $Y$ is not necessarily finite,
becoming a union of lax functors. We prove some properties of this functor
that enable us to give a recipe for finding approximations for a special type
of functions: predicate liftings that have been introduced for coalgebraic
modal logic [p:coalgebraic-logic, s:coalg-logics-limits-beyond-journal]. This
recipe allows us to include a new case study in the machinery for fixpoint
checking: coalgebraic behavioural metrics, based on Wasserstein liftings.

The paper is organized as follows: In Section 2 we give some high-level
motivation, while in Section 3 we review the theory from [BEKP:FTUD-journal].
Subsequently in Section 4 we introduce two (gs-monoidal) categories
$\mathbb{C}$, $\mathbb{A}$ (of concrete and abstract functions), investigate
the properties of the approximation map $\\#$ between these categories. We
then show how to handle predicate liftings (Section 5) and behavioural metrics
(Section 6) in that setting. Next, for the finitary case, we show that the
categories $\mathbb{C}$, $\mathbb{A}$ are indeed gs-monoidal and $\\#$ is gs-
monoidal functor (Section 7) and lastly discuss the tool UDEfix in Section 8.
We end by drawing some conclusions (Section 9).

This article is an extended version of the paper [BEKMP:MVFPC] presented at
ICGT ’23. With respect to the conference version, the present paper contains
additional explanations and examples and full proofs of the results.

##  2\. Motivation

We start with some motivations for our theory and the tool UDEfix, which is
based on it, via a case study on behavioural metrics. We consider
probabilistic transition systems (Markov chains) with labelled states. These
are given by a finite set of states $X$, a function $\eta\colon
X\to\mathcal{D}(X)$ mapping each state $x\in X$ to a probability distribution
on $X$ and a labelling function $\ell\colon X\to\Lambda$, where $\Lambda$ is a
fixed set of labels (for examples see Figure 1). Our aim is to determine the
behavioural distance of two states, whose definition is based on the so-called
Kantorovich or Wasserstein lifting [v:optimal-transport] that measures the
distance of two probability distributions on $X$, based on a distance $d\colon
X\times X\to[0,1]$. In more detail: given $d$, we define
$d^{\mathcal{D}}\colon\mathcal{D}(X)\times\mathcal{D}(X)\to[0,1]$ as

$d^{\mathcal{D}}(p_{1},p_{2})=\inf\\{\sum_{x_{1},x_{2}\in
X}d(x_{1},x_{2})\cdot t(x_{1},x_{2})\mid t\in\Gamma(p_{1},p_{2})\\}$

where $\Gamma(p_{1},p_{2})$ is the set of couplings of $p_{1},p_{2}$ (i.e.,
distributions $t\colon X\times X\to[0,1]$ such that $\sum_{x_{2}\in
X}t(x_{1},x_{2})=p_{1}(x_{1})$ and $\sum_{x_{1}\in
X}t(x_{1},x_{2})=p_{2}(x_{2})$). The Wasserstein lifting gives in fact the
solution of a transport problem, where we interpret $p_{1},p_{2}$ as the
supply respectively demand at each point $x\in X$. Transporting a unit from
$x_{1}$ to $x_{2}$ costs $d(x_{1},x_{2})$ and $t$ is a transport plan (=
coupling) whose marginals are $p_{1},p_{2}$. In other words
$d^{\mathcal{D}}(p_{1},p_{2})$ can be seen as the cost of the optimal
transport plan, moving the supply $p_{1}$ to the demand $p_{2}$.

$1$$A$$3$$B$$4$$C$$2$$A$$\nicefrac{{1}}{{2}}$$\nicefrac{{1}}{{2}}$$\nicefrac{{1}}{{3}}$$\nicefrac{{2}}{{3}}$$1$$1$

$1$$A$$2$$A$$1$$1$

Figure 1. Two probabilistic transition systems.

The behavioural metric is then defined as the least fixpoint of the function
$\mathcal{W}\colon[0,1]^{X\times X}\to[0,1]^{X\times X}$ where
$\mathcal{W}(d)(x_{1},x_{2})=1$ if $\ell(x_{1})\neq\ell(x_{2})$ and
$\mathcal{W}(d)(x_{1},x_{2})=d^{\mathcal{D}}(\eta(x_{1}),\eta(x_{2}))$
otherwise. For instance, the best transport plan for the system on the left-
hand side of Figure 1 and the distributions $\eta(1),\eta(2)$ is $t$ with
$t(3,3)=\nicefrac{{1}}{{3}}$, $t(3,4)=\nicefrac{{1}}{{6}}$,
$t(4,4)=\nicefrac{{1}}{{2}}$ and $0$ otherwise.

One can observe that the function $\mathcal{W}$ can be decomposed as

$\mathcal{W}=\max\nolimits_{\rho}\circ(c_{k}\otimes(\eta\times\eta)^{*}\circ\min\nolimits_{u}\circ\tilde{\mathcal{D}}),$

where $\otimes$ stands for disjoint union (on functions) and we use the
functions given in Table 1. Note that the operators can be generalised to the
case in which the underlying sets are infinite, by replacing $\min$ and $\max$
with $\inf$ and $\sup$. More concretely, the types of the components and the
parameters $k,u,\rho$ are given as follows, where $Y=X\times X$:

  * •

$c_{k}\colon[0,1]^{\emptyset}\to[0,1]^{Y}$ where $k(x,x^{\prime})=1$ if
$\ell(x)\neq\ell(x^{\prime})$ and $0$ otherwise.

  * •

$\tilde{\mathcal{D}}\colon[0,1]^{Y}\to[0,1]^{\mathcal{D}(Y)}$.

  * •

$\min\nolimits_{u}\colon[0,1]^{\mathcal{D}(Y)}\to[0,1]^{\mathcal{D}(X)\times\mathcal{D}(X)}$
where $u\colon\mathcal{D}(Y)\to\mathcal{D}(X)\times\mathcal{D}(X)$,
$u(t)=(p,q)$ with $p(x)=\sum_{x^{\prime}\in X}t(x,x^{\prime})$,
$q(x)=\sum_{x^{\prime}\in X}t(x^{\prime},x)$.

  * •

$(\eta\times\eta)^{*}\colon[0,1]^{\mathcal{D}(X)\times\mathcal{D}(X)}\to[0,1]^{Y}$.

  * •

$\max\nolimits_{\rho}\colon[0,1]^{Y+Y}\to[0,1]^{Y}$ where $\rho\colon Y+Y\to
Y$ is the obvious map from the coproduct (disjoint union of sets) $Y+Y$ to
$Y$.

Function | $c_{k}$ | $g^{*}$ | $\min_{u}$ | $\max_{u}$ |  $\mathrm{av}_{D}=\tilde{\mathcal{D}}$
---|---|---|---|---|---
| $k\colon Z\to\mathbb{M}$ | $g\colon Z\to Y$ | $u\colon Y\to Z$ | $u\colon Y\to Z$ |  $\mathbb{M}=[0,1]$, $Z=\mathcal{D}(Y)$
Name | constant | reindexing | minimum | maximum | expectation
$a\mapsto\dots$ | $k$ | $a\circ g$ | $\lambda z.\min\limits_{u(y)=z}a(y)$ | $\lambda z.\max\limits_{u(y)=z}a(y)$ |  $\lambda z.\sum\limits_{y\in Y}z(y)\cdot a(y)$
Table 1. Basic functions of type $\mathbb{M}^{Y}\to\mathbb{M}^{Z}$, $a\colon
Y\to\mathbb{M}$.

In fact, this decomposition can be depicted diagrammatically, as in Figure 2.

$c_{k}$$\tilde{\mathcal{D}}$$\min\nolimits_{u}$$(\eta\times\eta)^{*}$$\max\nolimits_{\rho}$$[0,1]^{Y}$$[0,1]^{Y}$$[0,1]^{\mathcal{D}(Y)}$$[0,1]^{\mathcal{D}(X)\times\mathcal{D}(X)}$$[0,1]^{Y}$$+$$[0,1]^{Y}$
Figure 2. Decomposition of the fixpoint function $\mathcal{W}$ for computing
behavioural metrics.

The function $\mathcal{W}$ is a monotone function on a complete lattice, hence
it has a least fixpoint by Knaster-Tarski’s fixpoint theorem [t:lattice-fixed-
point], which is the behavioural metric. By giving a transport plan as above,
it is possible to provide an upper bound for the Wasserstein lifting and hence
there are strategy iteration algorithms that can approach a fixpoint from
above. The problem with these algorithms is that they might get stuck at a
fixpoint that is not the least. Hence, it is essential to be able to determine
whether a given fixpoint is indeed the smallest one (cf. [bblmtb:prob-bisim-
distance-automata-journal]).

Consider for instance the transition system in Figure 1 on the right. It
contains two states $1,2$ on a cycle. In fact these two states should be
indistinguishable and hence, if $d=\mu\mathcal{W}$ is the least fixpoint of
$\mathcal{W}$, then $d(1,2)=d(2,1)=0$. However, the metric $a$ with
$a(1,2)=a(2,1)=1$ ($0$ otherwise) is also a fixpoint and the question is how
to determine that it is not the least.

For this, we use the techniques developed in [BEKP:FTUD-journal] that require,
in particular, that $\mathcal{W}$ is non-expansive (i.e., given two metrics
$d_{1},d_{2}$, the sup-distance of $\mathcal{W}(d_{1}),\mathcal{W}(d_{2})$ is
smaller or equal than the sup-distance of $d_{1},d_{2}$). In this case we can
associate $\mathcal{W}$ with an approximation $\mathcal{W}_{\\#}^{a}$ on
subsets of $X\times X$ such that, given $Y^{\prime}\subseteq X\times X$, the
set $\mathcal{W}_{\\#}^{a}(Y^{\prime})$ intuitively contains all pairs
$(x_{1},x_{2})$ such that, decreasing function $a$ by some value $\delta$ over
$Y^{\prime}$, resulting in a function $b$ (defined as
$b(x_{1},x_{2})=a(x_{1},x_{2})-\delta$ if $(x_{1},x_{2})\in Y^{\prime}$ and
$b(x_{1},x_{2})=a(x_{1},x_{2})$ otherwise) and applying $\mathcal{W}$, we
obtain a function $\mathcal{W}(b)$, where the same decrease takes place at
$(x_{1},x_{2})$ (i.e.,
$\mathcal{W}(b)(x_{1},x_{2})=\mathcal{W}(a)(x_{1},x_{2})-\delta$). Concretely,
here $\mathcal{W}_{\\#}^{a}(\\{(1,2)\\})=\\{(2,1)\\}$, since a decrease at
$(1,2)$ will cause a decrease at $(2,1)$ in the next iteration. In fact the
greatest fixpoint of $\mathcal{W}_{\\#}^{a}$, which here is
$\\{(1,2),(2,1)\\}$, gives us those elements that have a potential for
decrease (intuitively there is “slack” or “wiggle room”) and form a vicious
cycle as above. It holds that $a$ is the least fixpoint of $\mathcal{W}$ iff
the the greatest fixpoint of $\mathcal{W}_{\\#}^{a}$ is the empty set, a non-
trivial result proved in [BEKP:FTUD-journal].

The importance of the decomposition stems from the fact that the approximation
is compositional, that is $\mathcal{W}_{\\#}^{a}$ can be built out of the
approximations of $\max\nolimits_{\rho}$, $c_{k}$, $(\delta\times\delta)^{*}$,
$\min\nolimits_{u}$, $\tilde{\mathcal{D}}=\mathrm{av}_{D}$, which can be
easily determined (see Table 2).

The function $\tilde{\mathcal{D}}$ can be obtained as the predicate lifting of
the distribution functor $\mathcal{D}$ (see Section 5). But for general
functors, beyond $\mathcal{D}$, the characterization is still missing and will
be provided in this paper.

We anticipate that in our tool UDEfix we can draw a diagram as in Figure 2,
from which the approximation and its greatest fixpoint is automatically
computed in a compositional way, allowing us to perform such fixpoint checks.

##  3\. Preliminaries

This section reviews some background used throughout the paper. This includes
the basics of lattices and MV-algebras, where the functions of interest take
values. We also recap some results from [BEKP:FTUD-journal] useful for
detecting if a fixpoint of a given function is the least (or greatest).

We will also need some standard notions from _category theory_ , in particular
categories, functors and natural transformations. The definition of (strict)
gs-monoidal categories is spelled out in detail later in Definition 7.1.

For sets $X,Y$, we denote by $\mathcal{P}(X)$ the powerset of $X$ and
$\mathcal{P}_{f}(X)$ the set of finite subsets of $X$. The set of functions
from $X$ to $Y$ is denoted by $Y^{X}$.

A partially ordered set $(P,\sqsubseteq)$ is often denoted simply as $P$,
omitting the order relation. For $x,y\in P$, we write $x\sqsubset y$ when
$x\sqsubseteq y$ and $x\neq y$. For a function $f:X\to P$, we will write
$\arg\min_{x\in X}f(x)$ to denote the set of elements where $f$ reaches the
minimum, i.e., $\\{x\in X\mid\forall y\in X.\,f(x)\sqsubseteq f(y)\\}$ and,
abusing the notation, we will write $z=\arg\min_{x\in X}f(x)$ instead of
$z\in\arg\min_{x\in X}f(x)$. The _join_ and the _meet_ of a subset $X\subseteq
P$ (if they exist) are denoted $\bigsqcup X$ and $\bigsqcap X$.

A _complete lattice_ is a partially ordered set $(\mathbb{L},\sqsubseteq)$
such that each subset $X\subseteq\mathbb{L}$ admits a join $\bigsqcup X$ and a
meet $\bigsqcap X$. A complete lattice $(\mathbb{L},\sqsubseteq)$ always has a
least element $\bot=\bigsqcap\mathbb{L}$ and a greatest element
$\top=\bigsqcup\mathbb{L}$.

A function $f:\mathbb{L}\to\mathbb{L}$ is _monotone_ if for all
$l,l^{\prime}\in\mathbb{L}$, if $l\sqsubseteq l^{\prime}$ then
$f(l)\sqsubseteq f(l^{\prime})$. By Knaster-Tarski’s theorem [t:lattice-fixed-
point, Theorem 1], any monotone function on a complete lattice has a least
fixpoint $\mu f$ and a greatest fixpoint $\nu f$, characterised as the meet of
all pre-fixpoints $\mu f=\bigsqcap\\{l\mid f(l)\sqsubseteq l\\}$ and, dually,
a greatest fixpoint $\nu f=\bigsqcup\\{l\mid l\sqsubseteq f(l)\\}$,
characterised as the join of all post-fixpoints. We denote by
$\mathit{Fix}(f)$ the set of all fixpoints of $f$.

For a set $Y$ and a complete lattice $\mathbb{L}$, the set of functions
$\mathbb{L}^{Y}=\\{f\mid f:Y\to\mathbb{L}\\}$ with pointwise order (for
$a,b\in\mathbb{L}^{Y}$, $a\sqsubseteq b$ if $a(y)\sqsubseteq b(y)$ for all
$y\in Y$), is a complete lattice.

We are also interested in the set of finitely supported probability
distributions $\mathcal{D}(Y)\subseteq[0,1]^{Y}$, i.e., functions
$\beta:Y\to[0,1]$ with finite support such that $\sum_{y\in Y}\beta(y)=1$.

######  Definition 3.1 (MV-algebra).

An _MV-algebra_ [Mun:MV] is a tuple
$\mathbb{M}=(M,\oplus,0,\overline{(\cdot)})$ where $(M,\oplus,0)$ is a
commutative monoid and $\overline{(\cdot)}:M\to M$ maps each element to its
_complement_ , such that, if we define $1=\overline{0}$ and _subtraction_
$x\ominus y=\overline{\overline{x}\oplus y}$, then for all $x,y\in M$ it holds
that

  1. (1)

$\overline{\overline{x}}=x$;

  2. (2)

$x\oplus 1=1$;

  3. (3)

$(x\ominus y)\oplus y=(y\ominus x)\oplus x$.

MV-algebras are endowed with a partial order, the so-called _natural order_ ,
defined for $x,y\in M$, by $x\sqsubseteq y$ if $x\oplus z=y$ for some $z\in
M$. When $\sqsubseteq$ is total, $\mathbb{M}$ is called an _MV-chain_. We will
often write $\mathbb{M}$ instead of $M$.

The natural order gives an MV-algebra a lattice structure where $\bot=0$,
$\top=1$, $x\sqcup y=(x\ominus y)\oplus y$ and $x\sqcap
y=\overline{\overline{x}\sqcup\overline{y}}=x\ominus(x\ominus y)$. We call the
MV-algebra _complete_ if it is a complete lattice, which is not true in
general, e.g., $([0,1]\cap\mathbb{Q},\leq)$.

######  Example 3.2.

A prototypical MV-algebra is $([0,1],\oplus,0,\overline{(\cdot)})$ where
$x\oplus y=\min\\{x+y,1\\}$, $\overline{x}=1-x$ and $x\ominus
y=\max\\{0,x-y\\}$ for $x,y\in[0,1]$. The natural order is $\leq$ (less or
equal) on the reals. Another example is
$K=(\\{0,\dots,k\\},\oplus,0,\overline{(\cdot)})$ where $n\oplus
m=\min\\{n+m,k\\}$, $\overline{n}=k-n$ and $n\ominus m=\max\\{n-m,0\\}$ for
$n,m\in\\{0,\dots,k\\}$. Both MV-algebras are complete and MV-chains.

We next briefly recap the theory from [BEKP:FTUD-journal] which will be
helpful in the paper for checking whether a fixpoint is the least or the
greatest fixpoint of some underlying endo-function. For the purposes of the
present paper we actually need a generalisation of the theory which provides
the approximation also for functions with an infinite domain (while the theory
in [BEKP:FTUD-journal] was restricted to finite sets). Hence in the following,
sets $Y$ and $Z$ are possibly infinite.

Given $a\in\mathbb{M}^{Y}$ we define its _norm_ as
$|\\!|{a}|\\!|=\sup\\{a(y)\mid y\in Y\\}$. A function
$f:\mathbb{M}^{Y}\to\mathbb{M}^{Z}$ is _non-expansive_ if for all
$a,b\in\mathbb{M}^{Y}$ it holds $|\\!|{f(b)\ominus
f(a)}|\\!|\sqsubseteq|\\!|{b\ominus a}|\\!|$. It can be seen that non-
expansive functions are monotone. A number of standard operators are non-
expansive (e.g., constants, reindexing, max and min over a relation, average
in Table 1), and non-expansiveness is preserved by composition and disjoint
union (see [BEKP:FTUD-journal, Theorem 5.2]). Given $Y^{\prime}\subseteq Y$
and $\delta\in\mathbb{M}$, we write $\delta_{Y^{\prime}}$ for the function
defined by $\delta_{Y^{\prime}}(y)=\delta$ if $y\in Y^{\prime}$ and
$\delta_{Y^{\prime}}(y)=0$, otherwise.

Let $f:\mathbb{M}^{Y}\to\mathbb{M}^{Y}$, $a\in\mathbb{M}^{Y}$ and
$0\sqsubset\delta\in\mathbb{M}$. For a non-expansive endo-function
$f:\mathbb{M}^{Y}\to\mathbb{M}^{Y}$ and $a\in\mathbb{M}^{Y}$, the theory in
[BEKP:FTUD-journal] provides a so-called $a$-approximation $f_{\\#}^{a}$ of
$f$, which is an endo-function over a suitable subset of $\mathcal{P}(Y)$.
More precisely, for $a,b\in\mathbb{M}^{Y}$, let
$[a,b]=\\{c\in\mathbb{M}^{Y}\mid a\sqsubseteq c\sqsubseteq b\\}$ and let
$[Y]^{a}=\\{y\in Y\mid a(y)\neq 0\\}$. Consider the functions
$\alpha^{a,\delta}:\mathcal{P}([{Y}]^{a})\to[{a\ominus\delta},{a}]$ and
$\gamma^{a,\delta}:[{a\ominus\delta},{a}]\to\mathcal{P}([{Y}]^{a})$, defined,
for $Y^{\prime}\in\mathcal{P}([{Y}]^{a})$ and $b\in[{a\ominus\delta},{a}]$, by

$\alpha^{a,\delta}(Y^{\prime})=a\ominus\delta_{Y^{\prime}}\qquad\qquad\gamma^{a,\delta}(b)=\\{y\in[{Y}]^{a}\mid
a(y)\ominus b(y)\sqsupseteq\delta\\}.$

For a non-expansive function $f:\mathbb{M}^{Y}\to\mathbb{M}^{Z}$ and
$\delta\in\mathbb{M}$, define
$f^{a,\delta}_{\\#}\colon\mathcal{P}([{Y}]^{a})\to\mathcal{P}([{Z}]^{f(a)})$
as $f_{\\#}^{a,\delta}=\gamma^{f(a),\delta}\circ f\circ\alpha^{a,\delta}$. The
function $f_{\\#}^{a,\delta}$ is antitone in the parameter $\delta$ and we
define the _$a$ -approximation_ of $f$ as

$f_{\\#}^{a}=\bigcup_{\delta\sqsupset 0}f_{\\#}^{a,\delta}.$

For finite sets $Y$ and $Z$ there exists a suitable value
$\iota_{f}^{a}\sqsupset 0$, such that all functions $f_{\\#}^{a,\delta}$ for
$0\sqsubset\delta\sqsubseteq\iota_{f}^{a}$ are equal. Here, the
$a$-approximation is given by $f_{\\#}^{a}=f_{\\#}^{a,\delta}$ for
$\delta={\iota_{f}^{a}}$.

Let $\delta_{a}=\min\\{a(y)\mid y\in[Y]^{a}\\}$ be the least non-zero value
assumed by a function $a$. When $\delta\sqsubseteq\delta_{a}$, the pair
$\langle\alpha^{a,\delta},\gamma^{a,\delta}\rangle$ is a (contra-variant)
Galois connection, a notion at the heart of abstract interpretation [cc:ai-
unified-lattice-model, CC:TLA], and
$f^{a,\delta}_{\\#}=\gamma^{f(a),\delta}\circ f\circ\alpha^{a,\delta}$ is the
best correct approximation of $f$.

Intuitively, given some $Y^{\prime}$, the set $f_{\\#}^{a}(Y^{\prime})$
contains the points where a decrease of the values of $a$ on the points in
$Y^{\prime}$ “propagates” through the function $f$. The greatest fixpoint of
$f_{\\#}^{a}$ gives us the subset of $Y$ where such a decrease is propagated
in a cycle (a so-called “vicious cycle”). Whenever $\nu f_{\\#}^{a}$ is non-
empty, one can argue that $a$ cannot be the least fixpoint of $f$ since we can
decrease the value in all elements of $\nu f_{\\#}^{a}$, obtaining a smaller
pre-fixpoint. Interestingly, for non-expansive functions, also the converse
holds, i.e., emptiness of the greatest fixpoint of $f_{\\#}^{a}$ implies that
$a$ is the least fixpoint.

######  Theorem 3.3 (soundness and completeness for fixpoints).

Let $\mathbb{M}$ be a complete MV-chain, $Y$ a finite set and
$f:\mathbb{M}^{Y}\to\mathbb{M}^{Y}$ be a non-expansive function. Let
$a\in\mathbb{M}^{Y}$ be a fixpoint of $f$. Then $\nu f^{a}_{\\#}=\emptyset$ if
and only if $a=\mu f$.

If $a$ is not the least fixpoint and thus $\nu f^{a}_{\\#}\neq\emptyset$ then
there is $0\sqsubset\delta\in\mathbb{M}$ such that $a\ominus\delta_{\nu
f^{a}_{\\#}}$ is a pre-fixpoint of $f$.

Using the above theorem we can check whether some fixpoint $a$ of $f$ is the
least fixpoint. Whenever $a$ is a fixpoint, but not yet the least fixpoint of
$f$, it can be decreased by a fixed value in $\mathbb{M}$ (see [BEKP:FTUD-
journal, Proposition 4.5] for the details) on the points in $\nu f^{a}_{\\#}$
to obtain a smaller pre-fixpoint. In this way we obtain $a^{\prime}\sqsubset
a$ such that $f(a^{\prime})\sqsubseteq a^{\prime}$.

This results in the following complete proof rule, where “complete” means that
it can be used in both directions.

$\frac{a=f(a)\qquad\nu f_{\\#}^{a}=\emptyset}{a=\mu f}$

Whenever $a\in\mathbb{M}^{Y}$ is not a fixpoint, but a post-fixpoint of $f$
(i.e., $a\sqsubseteq f(a)$), one can still consider a restriction of the
$a$-approximation of $f$ and obtain a sound, but not complete rule.

######  Lemma 3.4 (soundness for post-fixpoints).

Let $\mathbb{M}$ be a complete MV-chain, $Y$ a finite set and
$f:\mathbb{M}^{Y}\to\mathbb{M}^{Y}$ a non-expansive function,
$a\in\mathbb{M}^{Y}$ such that $a\sqsubseteq f(a)$. Define
$[{Y}]^{a=f(a)}=\\{y\in[{Y}]^{a}\mid a(y)=f(a)(y)\\}$ and restrict the
abstraction $f^{a}_{\\#}:\mathcal{P}([{Y}]^{a})\to\mathcal{P}([{Y}]^{f(a)})$
to an endo-function $f_{*}^{a}:[{Y}]^{a=f(a)}\to[{Y}]^{a=f(a)}$ by letting
$f_{*}^{a}(Y^{\prime})=f^{a}_{\\#}(Y^{\prime})\cap[{Y}]^{a=f(a)}$. If $\nu
f^{a}_{*}=\emptyset$ then $a\sqsubseteq\mu f$.

Written more compactly, we obtain the following (incomplete) proof rule:

$\frac{a\sqsubseteq f(a)\qquad\nu f_{*}^{a}=\emptyset}{a\sqsubseteq\mu f}$

The above theory can be easily be dualised to checking greatest fixpoints.

Some basic functions which can be used as basic building blocks for
constructing non-expansive functions have already been given in Table 1. In
Table 2 these basic non-expansive functions are listed together with their
approximations. Note that for $\min$ and $\max$ we slightly generalize and
allow relations instead of functions as parameters. Note, in particular, that
the approximation of reindexing is given by the inverse image, a fact that
will be often used in the paper.

function $f$ |  definition of $f$ | $f_{\\#}^{a}(Y^{\prime})$
---|---|---
$c_{k}$ | $f(a)=k$ | $\emptyset$
($k\in\mathbb{M}^{Z}$) |  |
$u^{*}$ | $f(a)=a\circ u$ | $u^{-1}(Y^{\prime})$
($u\colon Z\to Y$) |  |
$\min\nolimits_{\mathcal{R}}$ | $f(a)(z)=\min\limits_{y\mathcal{R}z}a(y)$ |  $\\{z\in[{Z}]^{f(a)}\mid\ \arg\min\limits_{y\in\mathcal{R}^{-1}(z)}a(y)\cap Y^{\prime}\neq\emptyset\\}$
($\mathcal{R}\subseteq Y\times Z$) |  |
$\max\nolimits_{\mathcal{R}}$ | $f(a)(z)=\max\limits_{y\mathcal{R}z}a(y)$ |  $\\{z\in[{Z}]^{f(a)}\mid\ \arg\max\limits_{y\in\mathcal{R}^{-1}(z)}a(y)\subseteq Y^{\prime}\\}$
($\mathcal{R}\subseteq Y\times Z$) |  |
$\tilde{\mathcal{D}}$ ($\mathbb{M}=[0,1]$, | $f(a)(p)=\sum\limits_{y\in Y}p(y)\cdot a(y)$ | $\\{p\in[{D}]^{f(a)}\mid\mathit{supp}(p)\subseteq Y^{\prime}\\}$
$Z=D\subseteq\mathcal{D}(Y)$) |  |
Table 2. Basic functions $f\colon\mathbb{M}^{Y}\to\mathbb{M}^{Z}$ (constant,
reindexing, minimum, maximum, average) and the corresponding approximations
$f^{a}_{\\#}\colon\mathcal{P}([{Y}]^{a})\to\mathcal{P}([{Z}]^{f(a)})$.
_Notation:_ $\mathcal{R}^{-1}(z)=\\{y\in Y\mid y\,\mathcal{R}\,z\\}$;
$\mathit{supp}(p)=\\{y\in Y\mid p(y)>0\\}$ for $p\in\mathcal{D}(Y)$;
$\arg\min_{y\in Y^{\prime}}a(y)$, resp. $\arg\max_{y\in Y^{\prime}}a(y)$ are
the sets of elements where $a|_{Y^{\prime}}$ reaches the minimum, resp. the
maximum, for $Y^{\prime}\subseteq Y$ and $a\in\mathbb{M}^{Y}$.

In Section 2 we already gave a motivating example for fixpoint checks. Here we
consider another example instantiating the framework.

######  Example 3.5.

We consider (unlabelled) Markov chains given by $(S,T,\eta)$, where $S$ is a
set of states, $T\subseteq S$ is a set of terminal states and $\eta\colon
S\backslash T\to\mathcal{D}(S)$ assigns to each non-terminal state a
probability distribution over its successors. We are interested in the
termination probability of a given state of the Markov chain, which can be
computed by taking the least fixpoint of a function
$\mathcal{T}\colon[0,1]^{S}\to[0,1]^{S}$:

$\displaystyle\mathcal{T}:[0,1]^{S}\to[0,1]^{S}$
$\displaystyle\mathcal{T}(t)(s)=\left\\{\begin{array}[]{ll}1&\mbox{if $s\in
T$}\\\ \sum\limits_{s^{\prime}\in S}\eta(s)(s^{\prime})\cdot
t(s^{\prime})&\mbox{otherwise}\end{array}\right.$

As an example we consider the Markov chain in Figure 3 with state set
$S=\\{x,y,u,z\\}$, where $u$ is the only terminal state. Let $p_{s}=\eta(s)$
be the probability distribution associated with state $s$. The least fixpoint
$\mu\mathcal{T}$ of $\mathcal{T}$ is given in Figure 3 in green (left) and the
greatest fixpoint $\nu\mathcal{T}$ in red (right). These are two of infinitely
many fixpoints of $\mathcal{T}$. The cycle on the left (including $y,z$) can
be seen as some kind of vicious cycle, where $y,z$ convince each other that
they terminate with a probability that might be too high.

$x$$\nicefrac{{1}}{{2}}$/$1$$u$$1$/$1$$y$$0$/$1$$z$$0$/$1$$\nicefrac{{1}}{{2}}$$\nicefrac{{1}}{{2}}$$1$$1$
Figure 3. A Markov chain with two fixpoints of $\mathcal{T}$ (right)

Now let $a=\nu\mathcal{T}$ be the greatest fixpoint of $\mathcal{T}$, i.e.,
the function $S\to[0,1]$ that maps every state to $1$. All states still have
“wiggle room” and can be decreased, hence $[{S}]^{a}=S$. Given
$S^{\prime}\subseteq S$, the approximation $\mathcal{T}_{\\#}^{a}$ is as
follows:

$\mathcal{T}_{\\#}^{a}(S^{\prime})=\\{s\in[{S}]^{\mathcal{T}(a)}\mid s\notin
T\land\mathit{supp}(\eta(s))\subseteq S^{\prime}\\}.$

where $\mathit{supp}(p)$ denoted the _support_ of a probability distribution
$p\colon S\to[0,1]$, i.e., the set of states $v$ for which $p(v)>0$.

Intuitively, if we decide to decrease the $a$-values of all states in
$S^{\prime}$ by some fixed amount $\delta$, the states in
$\mathcal{T}_{\\#}^{a}(S^{\prime})$ will also decrease their $a$-values by
$\delta$. This is true for all states that are not terminal and whose
successors are _all_ included in $S$.

In the example $\mathcal{T}_{\\#}^{a}(\\{y,z\\})=\\{y,z\\}$ and $\\{y,z\\}$ is
indeed the greatest fixpoint of the approximation. Since it is non-empty, we
can deduce that $a$ is not the least fixpoint. Furthermore we could now
subtract a small value (for details on how to obtain this value see
[BEKP:FTUD-journal, Proposition 4.5]) from $a(y)$, $a(z)$ to obtain a smaller
pre-fixpoint, from where one can continue to iterate to the least fixpoint
(see also [bekp:lattice-strategy-iteration]).

##  4\. A Categorical View of the Approximation Framework

The framework from [BEKP:FTUD-journal], summarized in the previous section, is
not based on category theory, but – as we shall see – it can be naturally
reformulated in a categorical setting. In particular, casting the
compositionality results into a monoidal structure (see Section 7) is a
valuable basis for our tool. The starting point for this section is the
observation that the operation of mapping a function $f$ to its approximation
$f_{\\#}^{a}$ (given a fixpoint $a$ of $f$) is compositional: it respects
(under some constraints) function composition and disjoint union, making it a
monoidal functor.

We however have to take care to choose adequate categories and fix an
appropriate setting, to obtain the desired results. First, we will show how
the operation $\\#$ of taking the $a$-approximation of a function can be seen
as a union of lax functors between two categories: a concrete category
$\mathbb{C}$ whose arrows are the non-expansive functions for which we seek
the least (or greatest) fixpoint and an abstract category $\mathbb{A}$ whose
arrows are the corresponding approximations.

More precisely, recall that, as discussed in the previous section, given a
non-expansive function $f:\mathbb{M}^{Y}\to\mathbb{M}^{Z}$, the approximation
of $f$ is relative to a fixed map $a\in\mathbb{M}^{Y}$. Hence we let objects
in $\mathbb{C}$ be elements $a\in\mathbb{M}^{Y}$ and an arrow from
$a\in\mathbb{M}^{Y}$ to $b\in\mathbb{M}^{Z}$ is a non-expansive function
$f:\mathbb{M}^{Y}\to\mathbb{M}^{Z}$ required to map $a$ into $b$. The
approximations instead live in a different category $\mathbb{A}$. Recall that
the approximation $f^{a}_{\\#}$ is of type
$\mathcal{P}([Y]^{a})\to\mathcal{P}([Z]^{b})$. Since the domain and codomain
are again dependent on maps $a$ and $b$, we still employ elements of
$\mathbb{M}^{Y}$ as objects, but arrows are functions between powersets.

######  Definition 4.1 (concrete and abstract categories).

We define two categories, the _concrete category_ $\mathbb{C}$ and the
_abstract category_ $\mathbb{A}$ and a functor
$\\#\colon\mathbb{C}\to\mathbb{A}$. The concrete category $\mathbb{C}$ has as
objects maps $a\in\mathbb{M}^{Y}$ where $Y$ is a (possibly infinite) set.
Given $a\in\mathbb{M}^{Y}$, $b\in\mathbb{M}^{Z}$ an arrow $f:a\dashrightarrow
b$ is a non-expansive function $f\colon\mathbb{M}^{Y}\to\mathbb{M}^{Z}$, such
that $f(a)=b$.

The abstract category $\mathbb{A}$ has again maps $a\in\mathbb{M}^{Y}$ as
objects. Given $a\in\mathbb{M}^{Y}$, $b\in\mathbb{M}^{Z}$ an arrow
$f:a\dashrightarrow b$ is a monotone (wrt. inclusion) function
$f\colon\mathcal{P}([Y]^{a})\to\mathcal{P}([Z]^{b})$. Arrow composition and
identities are the obvious ones.

The approximation maps $\\#\colon\mathbb{C}\to\mathbb{A}$ and
$\\#^{\delta}\colon\mathbb{C}\to\mathbb{A}$ (for $\delta\sqsupset 0$) are
defined as follows: for an object $a\in\mathbb{M}^{Y}$, we let
$\\#(a)=\\#^{\delta}(a)=a$ and, given an arrow $f:a\dashrightarrow b$, we let
$\\#^{\delta}(f)=f_{\\#}^{a,\delta}$ and $\\#(f)=\bigcup_{\delta\sqsupset
0}\\#^{\delta}(f)=f_{\\#}^{\delta}$.

Note that formal arrows are dashed ($\dashrightarrow$), while the underlying
functions are represented by standard arrows ($\to$).

[well-definedness] The categories $\mathbb{C}$ and $\mathbb{A}$ are well-
defined and the $\\#^{\delta}$ are lax functors, i.e., identities are
preserved and $\\#^{\delta}(f)\circ\\#^{\delta}(g)\subseteq\\#^{\delta}(f\circ
g)$ for composable arrows $f,g$ in $\mathbb{C}$.

######  Proof 4.2.

  1. (1)

_$\mathbb{C}$ is a well-defined category_: Given arrows $f\colon
a\dashrightarrow b$ and $g\colon b\dashrightarrow c$ then $g\circ f$ is non-
expansive (since non-expansiveness is preserved by composition) and $(g\circ
f)(a)=g(b)=c$, thus $g\circ f\colon a\dashrightarrow c$. Associativity holds
and the identities are the units of composition as for standard function
composition.

  2. (2)

_$\mathbb{A}$ is a well-defined category_: Given arrows $f\colon
a\dashrightarrow b$ and $g\colon b\dashrightarrow c$ then $g\circ f$ is
monotone (since monotonicity is preserved by composition) and hence $g\circ
f\colon a\dashrightarrow c$.

Again associativity and the fact that the identities are units is immediate.

  3. (3)

_$\\#^{\delta}\colon\mathbb{C}\to\mathbb{A}$ is a lax functor_: we first check
that identities are preserved. Let $U\subseteq[Y]^{a}$, then

$\displaystyle\\#^{\delta}(\mathit{id}_{a})(U)$
$\displaystyle=(\mathit{id}_{a})^{a,\delta}_{\\#}(U)$
$\displaystyle=\\{y\in[Y]^{\mathit{id}_{a}(a)}\mid\mathit{id}_{a}(a)(y)\ominus\mathit{id}_{a}(a\ominus\delta_{U})(y)\sqsupseteq\delta\\}$
$\displaystyle=\\{y\in[Y]^{a}\mid
a(y)\ominus(a\ominus\delta_{U})(y)\sqsupseteq\delta\\}$
$\displaystyle=U=\mathit{id}_{a}(U)=\mathit{id}_{\\#^{\delta}(a)}(U).$

where in the second last line we use the fact that $U\subseteq[Y]^{a}$.

Let $a\in\mathbb{M}^{Y}$, $b\in\mathbb{M}^{Z}$, $c\in\mathbb{M}^{V}$, $f\colon
a\dashrightarrow b$, $g\colon b\dashrightarrow c$ be arrows in $\mathbb{C}$
and $Y^{\prime}\subseteq[Y]^{a}$. Then

$\displaystyle(\\#^{\delta}(g)\circ\\#^{\delta}(f))(Y^{\prime})$
$\displaystyle=g_{\\#}^{b,\delta}(f_{\\#}^{a,\delta}(Y^{\prime}))$
$\displaystyle=(\gamma^{c,\delta}\circ
g\circ\alpha^{b,\delta}\circ\gamma^{b,\delta}\circ
f\circ\alpha^{a,\delta})(Y^{\prime})$
$\displaystyle\subseteq(\gamma^{g(f(a)),\delta}\circ g\circ
f\circ\alpha^{a,\delta})(Y^{\prime})$ $\displaystyle=(g\circ
f)_{\\#}^{a,\delta}(Y^{\prime})$ $\displaystyle=\\#^{\delta}(g\circ
f)(Y^{\prime})$

The inequality holds since for $c\in\mathbb{M}^{Z}$:

$\alpha^{b,\delta}(\gamma^{b,\delta}(c))=\alpha^{b,\delta}(\\{y\in Y\mid
b(y)\ominus c(y)\sqsupseteq\delta\\})=b\ominus\delta_{\\{y\in Y\mid
b(y)\ominus c(y)\sqsupseteq\delta\\}}\sqsupseteq c.$

Then the inequality follows from the antitonicity of $\gamma^{c,\delta}$.
(Remember that we are working with a contra-variant Galois connection.)

Note that while $\\#$ clearly also preserves identities, the question whether
it is a lax functor (or even a proper functor) is currently open. It is
however the union of lax functors.

Hence in the following it will be convenient to restrict to the subcategory of
$\mathbb{C}$ where arrows are reindexings and to subcategories of
$\mathbb{C}$, $\mathbb{A}$ with maps on finite sets.

######  Definition 4.3 (reindexing subcategory).

We denote by $\mathbb{C}^{*}$ the lluf 111A _lluf sub-category_ is a sub-
category that contains all objects. sub-category of $\mathbb{C}$ where arrows
are reindexing, i.e., given objects $a\in\mathbb{M}^{Y}$, $b\in\mathbb{M}^{Z}$
we consider only arrows $f:a\dashrightarrow b$ such that $f=g^{*}$ for some
$g\colon Z\to Y$ (hence, in particular, $b=g^{*}(a)=a\circ g$).

We prove the following auxiliary lemma that basically shows that reindexings
are preserved by $\alpha,\gamma$:

######  Lemma 4.4.

Given $a\in\mathbb{M}^{Y}$, $g\colon Z\to Y$ and
$0\sqsubset\delta\in\mathbb{M}$, then we have

  1. (1)

$\alpha^{a\circ g,\delta}\circ g^{-1}=g^{*}\circ\alpha^{a,\delta}$

  2. (2)

$\gamma^{a\circ g,\delta}\circ g^{*}=g^{-1}\circ\gamma^{a,\delta}$

This implies that for two $\mathbb{C}$-arrows $f\colon a\dashrightarrow b$,
$h\colon b\dashrightarrow c$, it holds that $\\#(h\circ f)=\\#(h)\circ\\#(f)$
whenever $f$ or $h$ is a reindexing, i.e., is contained in $\mathbb{C}^{*}$.
Hence $\\#\colon\mathbb{C}^{*}\to\mathbb{A}$ is a functor.

######  Proof 4.5.

  1. (1)

Let $Y^{\prime}\subseteq[{Y}]^{a}$. Then

$\displaystyle g^{*}(\alpha^{a,\delta}(Y^{\prime}))$
$\displaystyle=g^{*}(a\ominus\delta_{Y^{\prime}})=(a\ominus\delta_{Y^{\prime}})\circ
g=a\circ g\ominus\delta_{Y^{\prime}}\circ g$ $\displaystyle=a\circ
g\ominus\delta_{g^{-1}(Y^{\prime})}=\alpha^{a\circ
g,\delta}(g^{-1}(Y^{\prime}))$

where we use that $(\delta_{Y^{\prime}}\circ g)(z)=\delta$ if $g(z)\in
Y^{\prime}$, equivalent to $z\in g^{-1}(Y^{\prime})$, and $0$ otherwise. Hence
$\delta_{Y^{\prime}}\circ g=\delta_{g^{-1}(Y^{\prime})}$.

  2. (2)

Let $b\in\mathbb{M}^{Y}$ with $a\ominus\delta\sqsubseteq b\sqsubseteq a$. Then

$\displaystyle\gamma^{a\circ g,\delta}\circ g^{*}(b)$ $\displaystyle=\\{z\in
Z\mid a(g(z))\ominus b(g(z))\sqsupseteq\delta\\}=\\{z\in Z\mid
g(z)\in\gamma^{a,\delta}(b)\\}$ $\displaystyle=g^{-1}(\gamma^{a,\delta}(b))$

It is left to show that $\\#(h\circ f)=\\#(h)\circ\\#(f)$ whenever $f$ or $h$
is a reindexing. Recall that on reindexings it holds that $\\#(g^{*})=g^{-1}$.

Let $a\in\mathbb{M}^{Y}$, $b\in\mathbb{M}^{Z}$, $c\in\mathbb{M}^{W}$ and
assume first that $f$ is a reindexing, i.e., $f=g^{*}$ for some $g\colon Z\to
Y$. Let $Y^{\prime}\subseteq[Y]^{a}$, then

$\displaystyle\\#(h\circ f)$ $\displaystyle=(h\circ
f)_{\\#}^{a}=\bigcup_{\delta\sqsupset 0}(\gamma^{h(f(a)),\delta}\circ h\circ
f\circ\alpha^{a,\delta})(Y^{\prime})$ $\displaystyle=\bigcup_{\delta\sqsupset
0}(\gamma^{h(f(a)),\delta}\circ h\circ
g^{*}\circ\alpha^{a,\delta})(Y^{\prime})$
$\displaystyle=\bigcup_{\delta\sqsupset 0}(\gamma^{h(f(a)),\delta}\circ
h\circ\alpha^{a\circ g,\delta})(g^{-1}(Y^{\prime}))$ $\displaystyle(1)$
$\displaystyle=\bigcup_{\delta\sqsupset 0}(\gamma^{h(f(a)),\delta}\circ
h\circ\alpha^{f(a),\delta})(\\#(g^{*})(Y^{\prime}))$
$\displaystyle=(\\#(h)\circ\\#(f))(Y^{\prime})$

Now we assume that $h$ is a reindexing, i.e., $h=g^{*}$ for some $g\colon W\to
Z$. Let again $Y^{\prime}\subseteq[Y]^{a}$, then:

$\displaystyle\\#(h\circ f)$ $\displaystyle=(h\circ
f)_{\\#}^{a}=\bigcup_{\delta\sqsupset 0}(\gamma^{h(f(a)),\delta}\circ h\circ
f\circ\alpha^{a,\delta})(Y^{\prime})$ $\displaystyle=\bigcup_{\delta\sqsupset
0}(\gamma^{f(a)\circ g,\delta}\circ g^{*}\circ
f\circ\alpha^{a,\delta})(Y^{\prime})$ $\displaystyle=\bigcup_{\delta\sqsupset
0}g^{-1}((\gamma^{f(a),\delta}\circ f\circ\alpha^{a,\delta})(Y^{\prime}))$ (2)
$\displaystyle=g^{-1}(\bigcup_{\delta\sqsupset 0}(\gamma^{f(a),\delta}\circ
f\circ\alpha^{a,\delta})(Y^{\prime}))$ [preimage preserves union]
$\displaystyle=\\#(g^{*})(\bigcup_{\delta\sqsupset
0}(\gamma^{f(a),\delta}\circ f\circ\alpha^{a,\delta})(Y^{\prime}))$
$\displaystyle=(\\#(h)\circ\\#(f))(Y^{\prime})$

######  Definition 4.6 (finite subcategories).

We denote by $\mathbb{C}_{f}$, $\mathbb{A}_{f}$ the full sub-categories of
$\mathbb{C},\mathbb{A}$ where objects are of the kind $a\in\mathbb{M}^{Y}$ for
a _finite_ set $Y$.

The approximation map $\\#\colon\mathbb{C}\to\mathbb{A}$ restricts to
$\\#\colon\mathbb{C}_{f}\to\mathbb{A}_{f}$, which is a (proper) functor.

######  Proof 4.7.

Clearly the restriction to categories based on finite sets is well-defined.

We show that $\\#$ is a (proper) functor. Let $a\in\mathbb{M}^{Y}$,
$b\in\mathbb{M}^{Z}$, $c\in\mathbb{M}^{V}$, $f\colon a\dashrightarrow b$,
$g\colon b\dashrightarrow c$ and $Y^{\prime}\subseteq[Y]^{a}$. Then

$\displaystyle\\#(g\circ f)=(g\circ f)_{\\#}^{a}=g_{\\#}^{f(a)}\circ
f_{\\#}^{a}=g_{\\#}^{b}\circ f_{\\#}^{a}=\\#(g)\circ\\#(f),$

The second inequality above is a consequence of the compositionality result in
[BEKP:FTUD-journal, Proposition D.3]. This requires finiteness of the sets
$Y,Z,V$.

The rest follows from Lemma 4.1.

We will later show in Theorem 7.3 that $\\#$ also respects the monoidal
operation $\otimes$ (disjoint union of functions). Using this knowledge, we
can now apply the framework to an example.

######  Example 4.8.

We revisit Example 3.5 and observe that the function $\mathcal{T}$, whose
least fixpoint is termination probability, can be be decomposed as follows:

$\mathcal{T}=(\eta^{*}\circ\tilde{\mathcal{D}})\otimes c_{k}$

For the Markov chain in Figure 3 these parameters instantiate as follows (cf.
Table 1):

  * •

$c_{k}\colon[0,1]^{\emptyset}\to[0,1]^{T}$, $k\colon T\to[0,1]$ with $k(u)=1$

  * •

$\tilde{\mathcal{D}}\colon[0,1]^{S}\to[0,1]^{D}$, where $D$ is a suitable
finite subset of $\mathcal{D}(S)$ (to ensure compositionality).

  * •

$\eta^{*}\colon[0,1]^{D}\to[0,1]^{S\setminus T}$ where $\eta\colon S\setminus
T\to D$ with $\eta(s)=p_{s}$, where $p_{x}(y)=p_{x}(u)=\nicefrac{{1}}{{2}}$,
$p_{y}(z)=p_{z}(y)=1$ and all other values are $0$. The set $D$ has to contain
at least $p_{x},p_{y},p_{z}$.

Now given the greatest fixpoint $a=\nu\mathcal{T}$, we can compute
$\mathcal{T}_{\\#}^{a}$ compositionally. We instantiate the results of this
section and consider $\mathcal{T}\colon a\dashrightarrow a$ as an arrow living
in $\mathbb{C}_{f}$. The subfunctions of $\mathcal{T}$ given above can also be
considered as arrows in $\mathbb{C}_{f}$ for appropriate domains and
codomains, which we refrain from spelling out explicitly.

Now:

$\mathcal{T}_{\\#}^{a}=\\#\mathcal{T}=\\#((\eta^{*}\circ\tilde{\mathcal{D}})\otimes
c_{k})=\\#(\eta^{*})\circ\\#(\tilde{\mathcal{D}})\otimes\\#(c_{k})$

This knowledge enables us to obtain an approximation $\mathcal{T}_{\\#}^{a}$
compositionally out of the approximations of the subfunctions.

##  5\. Predicate Liftings

In this section we discuss how predicate liftings [p:coalgebraic-logic,
s:coalg-logics-limits-beyond-journal] can be integrated into our theory. In
this context the idea is to view a map in $\mathbb{M}^{Y}$ as a predicate over
$Y$ with values in $\mathbb{M}$ (e.g., if $\mathbb{M}=\\{0,1\\}$ we obtain
Boolean predicates). Then, given a functor $F$, a predicate lifting transforms
a predicate over $Y$ (a map in $\mathbb{M}^{Y}$), to a predicate over $FY$ (a
map in $\mathbb{M}^{FY}$). Predicate liftings have been studied for arbitrary
quantales, for instance, in [bkp:up-to-behavioural-metrics-fibrations] and one
can show that every complete MV-algebra is a quantale with respect to $\oplus$
and the inverse of the natural order. The result can be easily derived from
[di05:_algeb_lukas]. Below we provide an explicit proof.

###  5.1. Quantales

Recall that a _quantale_ is a complete lattice with an associative operator
that distributes over arbitrary joins. It is called _unital_ if its
associative operator has a neutral element (unit).

######  Lemma 5.1 (complete MV-algebras are quantales).

Let $\mathbb{M}$ be a complete MV-algebra. Then
$(\mathbb{M},\oplus,\supseteq)$ is a unital commutative quantale.

######  Proof 5.2.

We know $\mathbb{M}$ is a complete lattice. Binary meets are given by

$x\sqcap y=\overline{\overline{x\oplus\overline{y}}\oplus\overline{y}}.$ (2)

Moreover $\oplus$ is associative and commutative, with $0$ as neutral element.

It remains to show that $\oplus$ distributes with respect to $\sqcap$ (note
that $\sqcap$ is the join for the reverse order), i.e., that for all
$X\subseteq\mathbb{M}$ and $a\in\mathbb{M}$, it holds

$a\oplus\bigsqcap X=\bigsqcap\\{a\oplus x\mid x\in X\\}$

Clearly, since $\bigsqcap X\leq x$ for all $x\in X$ and $\oplus$ is monotone,
we have $a\oplus\bigsqcap X\sqsubseteq\bigsqcap\\{a\oplus x\mid x\in X\\}$. In
order to show that $a\oplus\bigsqcap X$ is the greatest lower bound, let $z$
be another lower bound for $\\{a\oplus x\mid x\in X\\}$, i.e., $z\sqsubseteq
a\oplus x$ for all $x\in X$. Then observe that for $x\in X$, using (2), we get

$x\sqsupseteq x\sqcap\overline{a}=\overline{\overline{(x\oplus a)}\oplus
a}\sqsupseteq\overline{\overline{z}\oplus a}=z\ominus a$

Therefore $\bigsqcap X\sqsupseteq z\ominus a$ and thus

$a\oplus\bigsqcap X\sqsupseteq a\oplus(z\ominus a)\sqsupseteq z$

as desired.

###  5.2. Predicate Liftings and their Properties

We now define predicate liftings and then first characterise which predicate
liftings are non-expansive and second, derive their approximations. We will
address both these issues in this section and then use predicate liftings to
define behavioural metrics in Section 6.

The fact that there are some functors $F$, for which $FY$ is infinite, even if
$Y$ is finite, is the reason why the categories $\mathbb{C}$ and $\mathbb{A}$
also include infinite sets. However note that the resulting fixpoint function
will be always defined for finite sets, although intermediate functions might
not conform to this.

######  Definition 5.3 (predicate lifting).

Given a functor $F\colon\mathbf{Set}\to\mathbf{Set}$, a _predicate lifting_ is
a family of functions $\tilde{F}_{Y}\colon\mathbb{M}^{Y}\to\mathbb{M}^{FY}$
(where $Y$ is a set), such that for all $g\colon Z\to Y$, $a\colon
Y\to\mathbb{M}$ it holds that
$(Fg)^{*}(\tilde{F}_{Y}(a))=\tilde{F}_{Z}(g^{*}(a))$.

That is, predicate liftings must commute with reindexings. The index $Y$ will
be omitted if clear from the context. Such predicate liftings are in one-to-
one correspondence to so called _evaluation maps_ $\mathit{ev}\colon
F\mathbb{M}\to\mathbb{M}$. (This follows from the Yoneda lemma, see e.g.
[ml:categories].) Given $\mathit{ev}$, we define the corresponding lifting to
be $\tilde{F}(a)=\mathit{ev}\circ Fa\colon FY\to\mathbb{M}$, where $a\colon
Y\to\mathbb{M}$.

In the sequel we will only consider well-behaved liftings [bbkk:coalgebraic-
behavioral-metrics, bkp:up-to-behavioural-metrics-fibrations], i.e., we
require that (i) $\tilde{F}$ is monotone; (ii) $\tilde{F}(0_{Y})=0_{FY}$ where
$0$ is the constant $0$-function; (iii) $\tilde{F}(a\oplus
b)\sqsubseteq\tilde{F}(a)\oplus\tilde{F}(b)$ for $a,b\colon Y\to\mathbb{M}$;
(iv) $F$ preserves weak pullbacks.

We aim to have not only monotone, but non-expansive liftings.

[non-expansive predicate lifting] Let $\mathit{ev}\colon
F\mathbb{M}\to\mathbb{M}$ be an evaluation map and assume that its
corresponding lifting $\tilde{F}\colon\mathbb{M}^{Y}\to\mathbb{M}^{FY}$ is
well-behaved. Then $\tilde{F}$ is non-expansive iff for all
$\delta\in\mathbb{M}$ it holds that
$\tilde{F}\delta_{Y}\sqsubseteq\delta_{FY}$.

######  Proof 5.4.

The proof is inspired by [ws:metrics-fuzzy-lax-journal, Lemma 3.9] and uses
the fact that a monotone function $f\colon\mathbb{M}^{Y}\to\mathbb{M}^{Z}$ is
non-expansive iff $f(a\oplus\delta)\sqsubseteq f(a)\oplus\delta$ for all
$a,\delta$.

($\Rightarrow$) Fix a set $Y$ and assume that
$\tilde{F}\colon\mathbb{M}^{Y}\to\mathbb{M}^{FY}$ is non-expansive. Then

$\tilde{F}(\delta)=\tilde{F}(0\oplus\delta)\sqsubseteq\tilde{F}(0)\oplus\delta\sqsubseteq
0\oplus\delta=\delta$

($\Leftarrow$) Now assume that $\tilde{F}(\delta)\sqsubseteq\delta$. Then,
using the lemma referenced above,

$\tilde{F}(a\oplus\delta)\sqsubseteq\tilde{F}(a)\oplus\tilde{F}(\delta)\sqsubseteq\tilde{F}(a)\oplus\delta$

Above we write $\delta$ for both $\delta_{Y}$, $\delta_{FY}$ and both
deductions rely on the fact that $\tilde{F}$ is well-behaved.

######  Example 5.5 (Finitely supported distributions).

We consider the (finitely supported) distribution functor $\mathcal{D}$ that
maps a set $X$ to all maps $p\colon X\to[0,1]$ that have finite support and
satisfy $\sum_{x\in X}p(x)=1$. (Here $\mathbb{M}=[0,1]$.) A possible
evaluation map is $\mathit{ev}\colon\mathcal{D}[0,1]\to[0,1]$ defined by
$\mathit{ev}(p)=\sum_{r\in[0,1]}r\cdot p(r)$, where $p$ is a distribution on
$[0,1]$ (expectation). It is easy to see that $\tilde{\mathcal{D}}$ is well-
behaved and non-expansive. The latter follows from
$\tilde{\mathcal{D}}(\delta_{Y})=\delta_{\mathcal{D}Y}$.

######  Example 5.6 (Finite powerset).

Another example is given by the finite powerset functor $\mathcal{P}_{f}$. We
are given the evaluation map
$\mathit{ev}\colon\mathcal{P}_{f}\mathbb{M}\to\mathbb{M}$, defined for finite
$S\subseteq\mathbb{M}$ as $\mathit{ev}(S)=\max S$, where $\max\emptyset=0$.
The lifting $\tilde{\mathcal{P}}_{f}$ is well-behaved (see [bbkk:coalgebraic-
behavioral-metrics]) and non-expansive. To show the latter, observe that
$\tilde{\mathcal{P}}_{f}(\delta_{Y})=\delta_{\mathcal{P}_{f}(Y)\backslash\\{\emptyset\\}}\sqsubseteq\delta_{\mathcal{P}_{f}(Y)}$.

Non-expansive predicate liftings can be seen as functors
$\tilde{F}\colon\mathbb{C}^{*}\to\mathbb{C}^{*}$. To be more precise,
$\tilde{F}$ maps an object $a\in\mathbb{M}^{Y}$ to
$\tilde{F}(a)\in\mathbb{M}^{FY}$ and an arrow $g^{*}:a\dashrightarrow a\circ
g$, , where $g\colon Z\to Y$, to
$(Fg)^{*}:\tilde{F}a\dashrightarrow\tilde{F}(a\circ g)$.

###  5.3. Approximations of Predicate Liftings

We now study approximations of predicate liftings, where we first investigate
an auxiliary natural transformation. It involves the approximation functor
$\\#\colon\mathbb{C}^{*}\to\mathbb{A}$ (restricted to $\mathbb{C}^{*}$) and
the predicate lifting $\tilde{F}\colon\mathbb{C}^{*}\to\mathbb{C}^{*}$
introduced before.

Let $\tilde{F}$ be a (non-expansive) predicate lifting. There is a natural
transformation $\beta\colon\\#\Rightarrow\\#\tilde{F}$ between functors
$\\#,\\#\tilde{F}\colon\mathbb{C}^{*}\to\mathbb{A}$, whose components, for
$a\in\mathbb{M}^{Y}$, are $\beta_{a}\colon a\dashrightarrow\tilde{F}(a)$ in
$\mathbb{A}$, defined by $\beta_{a}(U)=\tilde{F}^{a}_{\\#}(U)$ for
$U\subseteq[Y]^{a}$.

That is, the following diagrams commute for every $g\colon Z\to Y$ (the
diagram on the left indicates the formal arrows, while the one on the right
reports the underlying functions).

$\\#(a)$
---
$\\#(a\circ g)$
---
$\\#(\tilde{F}a)$
---
$\\#(\tilde{F}(a\circ g))$
---
$\\#(g^{*})$$\beta_{a}$$\beta_{a\circ g}$$\\#(\tilde{F}(g^{*}))$
$\mathcal{P}([Y]^{a})$
---
$\mathcal{P}([Z]^{a\circ g})$
---
$\mathcal{P}([FY]^{\tilde{F}(a)})$
---
$\mathcal{P}([FZ]^{\tilde{F}(a\circ g)})$
---
$g^{-1}$$\tilde{F}^{a}_{\\#}$$\tilde{F}^{a\circ g}_{\\#}$$(Fg)^{-1}$

######  Proof 5.7.

We first define a natural transformation
$\eta\colon\mathrm{Id}_{\mathbb{C}^{*}}\Rightarrow\tilde{F}$ (between the
identity functor and $\tilde{F}$) with components $\eta_{a}\colon
a\dashrightarrow\tilde{F}(a)$ (for $a\in\mathbb{M}^{Y}$) by defining
$\eta_{a}(b)=\tilde{F}(b)$ for $b\in\mathbb{M}^{Y}$. The $\eta_{a}$ are non-
expansive by assumption. In addition, $\eta$ is natural due to the definition
of a predicate lifting, i.e., $(Fg)^{*}\circ\tilde{F}=\tilde{F}\circ g^{*}$
for $g\colon Z\to Y$.

Now we apply $\\#$ and use the fact that $\\#$ is functorial, even for the
full category $\mathbb{C}$, whenever one of the two arrows to which $\\#$ is
applied is a reindexing (see Lemma 4.4). Furthermore we observe that
$\beta=\\#(\eta)$. This immediately gives commutativity of the diagram on the
left. (The diagram on the right just displays the underlying functions.)

For using the above result we next characterize
$\tilde{F}^{d}_{\\#}(Y^{\prime})$. We rely on the fact that $d$ can be
decomposed into $d=\pi_{1}\circ\bar{d}$, where the projection $\pi_{1}$ is
independent of $d$ and $\bar{d}$ is dependent on $Y^{\prime}$, and exploit the
natural transformation in Proposition 5.3.

We fix $Y^{\prime}\subseteq Y=X\times X$ and $d\colon Y\to\mathbb{M}$. Let
$\pi_{1}\colon\mathbb{M}\times\\{0,1\\}\to\mathbb{M}$ be the projection to the
first component and $\bar{d}\colon Y\to\mathbb{M}\times\\{0,1\\}$ with
$\bar{d}(y)=(d(y),\chi_{Y^{\prime}}(y))$ where $\chi_{Y^{\prime}}\colon
Y\to\\{0,1\\}$ is the characteristic function of $Y^{\prime}$. Then
$\tilde{F}_{\\#}^{d}(Y^{\prime})=(F\bar{d})^{-1}(\tilde{F}_{\\#}^{\pi_{1}}((\mathbb{M}\backslash\\{0\\})\times\\{1\\}))$.

######  Proof 5.8.

Let $d\in\mathbb{M}^{Y}$ and $Y^{\prime}\subseteq[{Y}]^{d}$. Note that
$\bar{d}^{-1}((\mathbb{M}\backslash\\{0\\})\times\\{1\\})=Y^{\prime}$ and
$d=\pi_{1}\circ\bar{d}$, thus by Proposition 5.3:

$\displaystyle\tilde{F}_{\\#}^{d}(Y^{\prime})$
$\displaystyle=\tilde{F}_{\\#}^{\pi_{1}\circ\bar{d}}(\bar{d}^{-1}((\mathbb{M}\backslash\\{0\\})\times\\{1\\}))$
$\displaystyle=(F\bar{d})^{-1}(\tilde{F}_{\\#}^{\pi_{1}}((\mathbb{M}\backslash\\{0\\})\times\\{1\\}))$

Here
$\tilde{F}_{\\#}^{\pi_{1}}((\mathbb{M}\backslash\\{0\\})\times\\{1\\})\subseteq
F(\mathbb{M}\times\\{0,1\\})$ is independent of $d$ and has to be determined
only once for every predicate lifting $\tilde{F}$. We will show how this set
looks like for our example functors. We first consider the distribution
functor.

Consider the lifting of the distribution functor presented in Example 5.5 and
let $Z=[0,1]\times\\{0,1\\}$. Then we have

$\tilde{\mathcal{D}}_{\\#}^{\pi_{1}}((0,1]\times\\{1\\})=\\{p\in\mathcal{D}Z\mid\mathit{supp}(p)\in(0,1]\times\\{1\\}\\}.$

######  Proof 5.9.

Let $\delta>0$. We define

$\tilde{\pi}^{\delta}_{1}:=\alpha^{\pi_{1},\delta}((0,1]\times\\{1\\})$

where $\tilde{\pi}^{\delta}_{1}(x,0)=x$,
$\tilde{\pi}^{\delta}_{1}(x,1)=x\ominus\delta$ for $x\in[0,1]$. Note that
$[\mathcal{D}Z]^{\tilde{\mathcal{D}}\pi_{1}}=\\{p\in
DZ\mid\exists(x,b)\in\mathit{supp}(p)\text{ with }x\geq 0\\}$. Now

$\displaystyle\tilde{\mathcal{D}}_{\\#}^{\pi_{1},\delta}((0,1]\times\\{1\\})$
$\displaystyle=\\{p\in[\mathcal{D}Z]^{\tilde{\mathcal{D}}\pi_{1}}\mid\tilde{\mathcal{D}}\pi_{1}(p)\ominus\tilde{\mathcal{D}}(\tilde{\pi}^{\delta}_{1})(p)\geq\delta\\}$
$\displaystyle=\\{p\in[\mathcal{D}Z]^{\tilde{\mathcal{D}}\pi_{1}}\mid\bigl{(}\sum_{x\in[0,1]}x\cdot
p(x,0)\oplus\sum_{x\in[0,1]}x\cdot p(x,1)\bigr{)}$
$\displaystyle\qquad\quad\ominus\bigl{(}\sum_{x\in[0,1]}x\cdot
p(x,0)\oplus\sum_{x\in[0,1]}(x\ominus\delta)\cdot p(x,1)\bigr{)}\geq\delta\\}$
$\displaystyle=\\{p\in[\mathcal{D}Z]^{\tilde{\mathcal{D}}\pi_{1}}\mid\sum_{x\in[0,\delta)}x\cdot
p(x,1)+\sum_{x\in[\delta,1]}\delta\cdot p(x,1)\geq\delta\\}$
$\displaystyle=\\{p\in[\mathcal{D}Z]^{\tilde{\mathcal{D}}\pi_{1}}\mid\mathit{supp}(p)\in[\delta,1]\times\\{1\\}\\}.$

Where the second last equality uses the fact that
$x\ominus(x\ominus\delta)=\delta$ if $x\geq\delta$ and $x$ otherwise.

Now, we obtain

$\tilde{\mathcal{D}}_{\\#}^{\pi_{1}}((0,1]\times\\{1\\})=\bigcup_{\delta\sqsupset
0}\tilde{\mathcal{D}}_{\\#}^{\pi_{1},\delta}((0,1]\times\\{1\\})=\\{p\in\mathcal{D}Z\mid\mathit{supp}(p)\in(0,1]\times\\{1\\}\\}.$

This means intuitively that a decrease or “slack” can exactly be propagated
for elements whose probabilities are strictly larger than $0$.

We now turn to the powerset functor.

Consider the lifting of the finite powerset functor from Example 5.6 and let
$Z=\mathbb{M}\times\\{0,1\\}$. Then we have

$(\tilde{\mathcal{P}}_{f})_{\\#}^{\pi_{1}}((\mathbb{M}\backslash\\{0\\})\times\\{1\\})=\\{S\in[\mathcal{P}_{f}Z]^{\tilde{\mathcal{P}}_{f}\pi_{1}}\mid\exists(s,1)\in
S~{}\forall(s^{\prime},0)\in S:~{}s\sqsupset s^{\prime}\\}.$

######  Proof 5.10.

Let $\delta\sqsupset 0$ and define $\tilde{\pi}_{1}^{\delta}$ as in the proof
of Lemma 5.3. Then

$\displaystyle(\tilde{\mathcal{P}}_{f})_{\\#}^{\pi_{1},\delta}((\mathbb{M}\backslash\\{0\\})\times\\{1\\})$
$\displaystyle=\\{S\in[\mathcal{P}_{f}Z]^{\tilde{\mathcal{P}}_{f}\pi_{1}}\mid\tilde{\mathcal{P}}_{f}\pi_{1}(S)\ominus\tilde{\mathcal{P}}_{f}(\tilde{\pi}^{\delta}_{1})(S)\sqsupseteq\delta\\}$
$\displaystyle=\\{S\in[\mathcal{P}_{f}Z]^{\tilde{\mathcal{P}}_{f}\pi_{1}}\mid\max_{(s,b)\in
S}s\ominus(\max_{(s,b)\in S}s\ominus b\cdot\delta)\sqsupseteq\delta\\}$
$\displaystyle=\\{S\in[\mathcal{P}_{f}Z]^{\tilde{\mathcal{P}}_{f}\pi_{1}}\mid\exists(s,1)\in
S~{}\forall(s^{\prime},0)\in S:~{}s\ominus\delta\sqsupseteq s^{\prime}\\}$

For the last step we note that this condition ensures that the second maximum
equates to $\max_{(s,b)\in S}s\ominus\delta$ which is required for the
inequality to hold. Now, we obtain

$\displaystyle(\tilde{\mathcal{P}}_{f})_{\\#}^{\pi_{1}}((\mathbb{M}\backslash\\{0\\})\times\\{1\\})$
$\displaystyle=\bigcup_{\delta\sqsupset
0}\tilde{F}_{\\#}^{\pi_{1},\delta}((\mathbb{M}\backslash\\{0\\})\times\\{1\\})$
$\displaystyle=\\{S\in[\mathcal{P}_{f}Z]^{\tilde{\mathcal{P}}_{f}\pi_{1}}\mid\exists(s,1)\in
S~{}\forall(s^{\prime},0)\in S:~{}s\sqsupset s^{\prime}\\}.$

The idea is that the maximum of a set $S$ decreases if we decrease at least
one its values and all values which are not decreased are strictly smaller.

######  Remark 5.11.

Note that $\\#$ is a functor on the subcategory $\mathbb{C}_{f}$ (see Lemma
4), while some liftings (e.g., the one for the distribution functor) involve
infinite sets, for which we would lose compositionality. In this case, given a
finite set $Y$, we will actually focus on a finite subset $D\subseteq FY$.
(This is possible since we consider coalgebras with finite state space and
impose some extra conditions, the details are given below.) Then we consider
$\tilde{F}_{Y}\colon\mathbb{M}^{Y}\to\mathbb{M}^{FY}$ and $e\colon
D\hookrightarrow FY$ (the embedding of $D$ into $FY$). We set
$f=e^{*}\circ\tilde{F}_{Y}\colon\mathbb{M}^{Y}\to\mathbb{M}^{D}$. Given
$a\colon Y\to\mathbb{M}$, we view $f$ as an arrow
$a\dashrightarrow\tilde{F}_{Y}(a)\circ e$ in $\mathbb{C}$. The approximation
adapts to the “reduced” lifting, which can be seen as follows (cf. Lemma 4.4,
which shows that $\\#$ preserves composition if one of the arrows is a
reindexing):

$f_{\\#}^{a}=\\#(f)=\\#(e^{*}\circ\tilde{F}_{Y})=\\#(e^{*})\circ\\#(\tilde{F}_{Y})=e^{-1}\circ\\#(\tilde{F}_{Y})=\\#(\tilde{F}_{Y})\cap
D.$

##  6\. Wasserstein Lifting and Behavioural Metrics

In this section we show how the framework for fixpoint checking described
before can be used to deal with coalgebraic behavioural metrics.

We build on [bbkk:coalgebraic-behavioral-metrics], where an approach is
proposed for canonically defining a behavioural pseudo-metric for coalgebras
of a functor $F\colon\mathbf{Set}\to\mathbf{Set}$, that is, for functions of
the form $\xi\colon X\to FX$ where $X$ is a set. Intuitively $\xi$ specifies a
transition system whose branching type is given by $F$. Given such a coalgebra
$\xi$, the idea is to endow $X$ with a pseudo-metric $d_{\xi}\colon X\times
X\to\mathbb{M}$ defined as the least fixpoint of the map $d\mapsto
d^{F}\circ(\xi\times\xi)$ where $\\_^{F}$ lifts a metric $d\colon X\times
X\to\mathbb{M}$ to a metric $d^{F}\colon FX\times FX\to\mathbb{M}$. Here we
focus on the so-called Wasserstein lifting and show how approximations of the
functions involved in the definition of the pseudo-metric can be determined.

###  6.1. Wasserstein Lifting

Hereafter, $F$ denotes a fixed endo-functor on $\mathbf{Set}$ and $\xi\colon
X\to FX$ is a coalgebra over a finite set $X$. We also fix a well-behaved non-
expansive predicate lifting $\tilde{F}$.

In order to define a Wasserstein lifting, a first ingredient is that of a
coupling. Given $t_{1},t_{2}\in FX$ a _coupling_ of $t_{1}$ and $t_{2}$ is an
element $t\in F(X\times X)$, such that $F{\pi_{i}}(t)=t_{i}$ for $i=1,2$,
where $\pi_{i}\colon X\times X\to X$ are the projections. We write
$\Gamma(t_{1},t_{2})$ for the set of all such couplings.

######  Definition 6.1 (Wasserstein lifting).

The Wasserstein lifting $\\_^{F}\colon\mathbb{M}^{X\times
X}\to\mathbb{M}^{FX\times FX}$ is defined for $d\colon X\times X\to\mathbb{M}$
and $t_{1},t_{2}\in FX$ as

$\displaystyle d^{F}(t_{1},t_{2})=\inf_{t\in\Gamma(t_{1},t_{2})}\tilde{F}d(t)$

For more intuition on the Wasserstein lifting see the motivations in Section
2. Note that a coupling correspond to a transport plan. It can be shown that
for well-behaved $\tilde{F}$, the lifting preserves pseudo-metrics (see
[bbkk:coalgebraic-behavioral-metrics, bkp:up-to-behavioural-metrics-
fibrations]).

In order to make the theory for fixpoint checks effective we will need to
restrict to a subclass of liftings.

######  Definition 6.2 (finitely coupled lifting).

We call a lifting $\tilde{F}$ _finitely coupled_ if for all $X$ and
$t_{1},t_{2}\in FX$ there exists a finite
$\Gamma^{\prime}(t_{1},t_{2})\subseteq\Gamma(t_{1},t_{2})$, which can be
computed given $t_{1},t_{2}$, such that
$\inf_{t\in\Gamma(t_{1},t_{2})}\tilde{F}d(t)=\min_{t\in\Gamma^{\prime}(t_{1},t_{2})}\tilde{F}d(t)$
for all $d$.

The lifting in Example 5.6 (for the finite powerset functor) is obviously
finitely coupled. For the lifting $\mathcal{\tilde{\mathcal{D}}}$ from Example
5.5 we note that the set of couplings $t\in\Gamma(t_{1},t_{2})$ forms a
polytope with a finite number of vertices, which can be effectively computed
and $\Gamma^{\prime}(t_{1},t_{2})$ consists of these vertices. The infimum
(minimum) is obtained at one of these vertices [bblm:on-the-fly-exact-journal,
Remark 4.5].

###  6.2. Decomposing the Behavioural Metrics Function

As mentioned above, for a coalgebra $\xi\colon X\to FX$ the behavioural
pseudo-metric $d:X\times X\to\mathbb{M}$ is the least fixpoint of the
behavioural metrics function $\mathcal{W}=(\\_^{F})\circ(\xi\times\xi)$ where
$(\\_^{F})$ is the Wasserstein lifting.

The Wasserstein lifting can be decomposed as
$\\_^{F}=\min\nolimits_{u}\circ\tilde{F}$ where $\tilde{F}:\mathbb{M}^{X\times
X}\to\mathbb{M}^{F(X\times X)}$ is the predicate lifting – which we require to
be non-expansive (cf. Lemma 5.3) – and $\min_{u}$ is the minimum over the
coupling function $u\colon F(X\times X)\to FX\times FX$ defined as
$u(t)=(F{\pi_{1}}(t),F{\pi_{2}}(t))$, which means that
$\min_{u}\colon\mathbb{M}^{F(X\times X)}\to\mathbb{M}^{FX\times FX}$ (see
Table 1).

Therefore the behavioural metrics function can be expressed as

$\mathcal{W}=(\xi\times\xi)^{*}\circ\min_{u}\circ\tilde{F}$

Explicitly, for $d\in[0,1]^{X\times X}$ and $x,y\in X$,

$\displaystyle\mathcal{W}(d)(x,y)$
$\displaystyle=\min\nolimits_{u}\circ\tilde{F}(d)(\xi(x),\xi(y))=\min_{u(t)=(\xi(x),\xi(y))}\tilde{F}(d)(t)=$
$\displaystyle=\min_{t\in\Gamma(\xi(x),\xi(y))}\tilde{F}d(t)=d^{F}(\xi(x),\xi(y))$

Note that the fixpoint equation for behavioural metrics is sometimes equipped
with a discount factor that reduces the effect of deviations in the (far)
future and ensures that the fixpoint is unique by contractivity of the
function. Here we focus on the undiscounted case where the fixpoint equation
may have several solutions.

######  Example 6.3.

Note that we can recover the motivating example from Section 2 by setting
$\mathbb{M}=[0,1]$ and using the functor $FX=\Lambda\times\mathcal{D}(X)$,
where $\Lambda$ is a fixed set of labels. We observe that couplings of
$(a_{1},p_{1}),(a_{2},p_{2})\in FX$ only exist if $a_{1}=a_{2}$ and – if they
do not exist – the Wasserstein distance is the infimum of an empty set, hence
$1$. If $a_{1}=a_{2}$, couplings correspond to the usual Wasserstein couplings
of $p_{1},p_{2}$ and the least fixpoint of $\mathcal{W}$ equals the
behavioural metrics, as explained in Section 2.

###  6.3. Approximation of the Behavioural Metrics Function

The decomposition of the behavioural metrics function $\mathcal{W}$ above, can
be used to derive its $d$-approximation.

Assume that $\tilde{F}$ is non-expansive and finitely coupled and fix a
coalgebra $\xi\colon X\to FX$. Let $Y=X\times X$, where $X$ is finite. For
$d\in\mathbb{M}^{Y}$ and $Y^{\prime}\subseteq[{Y}]^{d}$ we have

$\mathcal{W}_{\\#}^{d}(Y^{\prime})=\\{(x,y)\in[{Y}]^{d}\mid\ \exists
t\in\tilde{F}_{\\#}^{d}(Y^{\prime}),u(t)=(\xi(x),\xi(y)),\tilde{F}d(t)=\mathcal{W}(d)(x,y)\\}.$

######  Proof 6.4.

We first remark that since $X$ is finite and $\tilde{F}$ is finitely coupled
it is sufficient to restrict to finite subsets of $F(X\times X)$ and $FX\times
FX$ (cf. Remark 5.11). In other words $\mathcal{W}$ can be obtained as
composition of functions living in $\mathbb{C}_{f}$, hence $\\#$ is a proper
functor and approximations can obtained compositionally. We exploit this fact
in the following.

More concretely, we restrict $u$ to $u\colon V\to W$, where $V\subseteq
F(X\times X)$, $W\subseteq FX\times FX$. We require that $W$ contains all
pairs $(\xi(x),\xi(y))$ for $x,y\in X$ and $V=\bigcup_{(t_{1},t_{2})\in
W}\Gamma^{\prime}(t_{1},t_{2})$. Hence both $V,W$ are finite.

The function $\tilde{F}$ is restricted accordingly to a map
$\mathbb{M}^{Y}\to\mathbb{M}^{V}$ as explained in Remark 5.11.

For $d\in\mathbb{M}^{Y}$ and $Y^{\prime}\subseteq[{Y}]^{d}$ we have, using the
fact that $\mathcal{W}=(\xi\times\xi)^{*}\circ\min_{u}\circ\tilde{F}$,
compositionality and the approximations listed in Table 2:

$\displaystyle\mathcal{W}_{\\#}^{d}(Y^{\prime})=\\{(x,y)\in[{Y}]^{d}\mid\ $
$\displaystyle(\xi(x),\xi(y))\in(\min\nolimits_{u})_{\\#}^{\tilde{F}(d)}(\tilde{F}^{d}_{\\#}(Y^{\prime})\cap
V)\\}$ $\displaystyle=\\{(x,y)\in[{Y}]^{d}\mid\ $ $\displaystyle\arg\min_{t\in
u^{-1}(\xi(x),\xi(y))}\tilde{F}(d)(t)\cap\tilde{F}^{d}_{\\#}(Y^{\prime})\cap
V\not=\emptyset\\}$ $\displaystyle=\\{(x,y)\in[{Y}]^{d}\mid\ $
$\displaystyle\exists t\in\tilde{F}_{\\#}^{d}(Y^{\prime})\cap
V,u(t)=(\xi(x),\xi(y)),$
$\displaystyle\tilde{F}d(t)=\min\nolimits_{t^{\prime}\in
V}\tilde{F}d(t^{\prime})\\}$ $\displaystyle=\\{(x,y)\in[{Y}]^{d}\mid\ $
$\displaystyle\exists t\in\tilde{F}_{\\#}^{d}(Y^{\prime})\cap
V,u(t)=(\xi(x),\xi(y)),$
$\displaystyle\tilde{F}d(t)=\min\nolimits_{t^{\prime}\in\Gamma^{\prime}(\xi(x),\xi(y))}\tilde{F}d(t^{\prime})\\}$
$\displaystyle=\\{(x,y)\in[{Y}]^{d}\mid\ $ $\displaystyle\exists
t\in\tilde{F}_{\\#}^{d}(Y^{\prime}),u(t)=(\xi(x),\xi(y)),\tilde{F}d(t)=\min\nolimits_{t^{\prime}\in\Gamma^{\prime}(\xi(x),\xi(y))}\tilde{F}d(t^{\prime})\\}$
$\displaystyle=\\{(x,y)\in[{Y}]^{d}\mid\ $ $\displaystyle\exists
t\in\tilde{F}_{\\#}^{d}(Y^{\prime}),u(t)=(\xi(x),\xi(y)),\tilde{F}d(t)=\mathcal{W}(d)(x,y)\\}$

The first equality is based on Remark 5.11 and uses the fact that the
approximation for the restricted $\tilde{F}$ maps $Y^{\prime}$ to
$\tilde{F}^{d}_{\\#}(Y^{\prime})\cap V$.

The second-last inequality also needs explanation, in particular, we have to
show that the set on the second-last line is included in the one on the
previous line, although we omitted the intersection with $V$.

Hence let $(x,y)\in[{Y}]^{d}$ such that there exists
$s\in\tilde{F}^{d}_{\\#}(Y^{\prime})$, $u(s)=(\xi(x),\xi(y))$ and
$\tilde{F}d(s)=\min\nolimits_{t^{\prime}\in\Gamma^{\prime}(\xi(x),\xi(y))}\tilde{F}d(t^{\prime})$.
We have to show that there exists a $t$ with the same properties that is also
included in $V$.

The fact that $s\in\tilde{F}^{d}_{\\#}(Y^{\prime})$ implies that
$\tilde{F}(d)(s)\ominus\tilde{F}(d\ominus\delta_{Y^{\prime}})(s)\sqsupseteq\delta$
for small enough $\delta$, using the fact that
$\tilde{F}_{\\#}^{d}=\gamma^{\tilde{F}(d),\delta}\circ\tilde{F}\circ\alpha^{d,\delta}$
(for an appropriate value $\delta$).

Since the minimum of the Wasserstein lifting is always reached in
$\Gamma^{\prime}(\xi(x),\xi(y))$, independently of the argument, there exists
$t\in\Gamma^{\prime}(\xi(x),\xi(y))\subseteq V$ (hence
$u(t)=(\xi(x),\xi(y))$), such that

$\tilde{F}(d\ominus\delta_{Y^{\prime}})(t)=\min\nolimits_{t^{\prime}\in\Gamma(\xi(x),\xi(y))}\tilde{F}(d\ominus\delta_{Y^{\prime}})(t^{\prime}).$

This implies that
$\tilde{F}(d\ominus\delta_{Y^{\prime}})(t)\sqsubseteq\tilde{F}(d\ominus\delta_{Y^{\prime}})(s)$
(since $s\in\Gamma(\xi(x),\xi(y))$). From the assumption
$\tilde{F}d(s)=\min\nolimits_{t^{\prime}\in\Gamma^{\prime}(\xi(x),\xi(y))}\tilde{F}d(t^{\prime})$
we obtain $\tilde{F}d(s)\sqsubseteq\tilde{F}d(t)$. Hence, using the fact that
$\ominus$ is monotone in the first and antitone in the second argument, we
have:

$\delta\sqsubseteq\tilde{F}(d)(s)\ominus\tilde{F}(d\ominus\delta_{Y^{\prime}})(s)\sqsubseteq\tilde{F}(d)(t)\ominus\tilde{F}(d\ominus\delta_{Y^{\prime}})(t)\sqsubseteq\delta.$

The last inequality follows from non-expansiveness. Hence

$\tilde{F}(d)(s)\ominus\tilde{F}(d\ominus\delta_{Y^{\prime}})(s)=\tilde{F}(d)(t)\ominus\tilde{F}(d\ominus\delta_{Y^{\prime}})(t)=\delta,$

which in particular implies that $t\in\tilde{F}^{d}_{\\#}(Y^{\prime})$.

In order to conclude we have to show that
$\tilde{F}d(t)=\min\nolimits_{t^{\prime}\in\Gamma^{\prime}(\xi(x),\xi(y))}\tilde{F}d(t^{\prime})$.
We first observe that in an MV-chain $\mathbb{M}$, whenever $x\sqsubseteq y$
(for $x,y\in\mathbb{M}$) we can infer that $(y\ominus x)\oplus x=y$ (this
follows for instance from Lemma 2.4(6) in [BEKP:FTUD-journal] and duality).
The inequality $\tilde{F}(d\ominus\delta_{Y^{\prime}})\sqsubseteq\tilde{F}(d)$
holds by monotonicity and we can conclude that

$\displaystyle\tilde{F}d(t)$
$\displaystyle=(\tilde{F}(d)(t)\ominus\tilde{F}(d\ominus\delta_{Y^{\prime}})(t))\oplus\tilde{F}(d\ominus\delta_{Y^{\prime}})(t))$
$\displaystyle=(\tilde{F}(d)(s)\ominus\tilde{F}(d\ominus\delta_{Y^{\prime}})(s))\oplus\tilde{F}(d\ominus\delta_{Y^{\prime}})(t))$
$\displaystyle\sqsubseteq(\tilde{F}(d)(s)\ominus\tilde{F}(d\ominus\delta_{Y^{\prime}})(s))\oplus\tilde{F}(d\ominus\delta_{Y^{\prime}})(s))=\tilde{F}(d)(s).$

The other inequality $\tilde{F}d(s)\sqsubseteq\tilde{F}d(t)$ holds anyway and
hence $\tilde{F}d(t)=\tilde{F}d(s)$. This finally implies, as desired, that

$\tilde{F}d(t)=\tilde{F}d(s)=\min\nolimits_{t^{\prime}\in\Gamma^{\prime}(\xi(x),\xi(y))}\tilde{F}d(t^{\prime}).$

inline]B: this proof was too sloppy and was missing an argument

Intuitively the statement of Proposition 6.3 means that the optimal coupling
which reaches the minimum in the Wasserstein lifting must be contained in
$\tilde{F}_{\\#}^{d}(Y^{\prime})$. Note that $\tilde{F}_{\\#}^{d}$ has already
been characterized earlier in Section 5.3.

###  6.4. Examples on Behavioural Metrics

We now consider two examples involving coalgebras over the distribution and
powerset functor.

######  Example 6.5.

We start with an example involving probabilistic transition systems. Let
$X=\\{x,y,z\\}$. We define a coalgebra $\xi\colon
X\to\Lambda\times\mathcal{D}X$ via $\xi(x)(x)=1$,
$\xi(y)(y)=\xi(y)(z)=\nicefrac{{1}}{{2}}$ and $\xi(z)(z)=1$. All other
distances are $0$. Assume that all states have the same label (not indicated).

$y$$x$$z$$\nicefrac{{1}}{{2}}$$\nicefrac{{1}}{{2}}$$1$$1$

Since all states have the same label, they are in fact probabilistically
bisimilar and hence have behavioural distance $0$, given by the least fixpoint
of $\mathcal{W}$. Now consider the pseudo-metric $d\colon X\times X\to[0,1]$
with $d(x,y)=d(x,z)=d(y,z)=1$ and $0$ for the reflexive pairs. This is a also
a fixpoint of $\mathcal{W}$ ($d=\mathcal{W}(d)$), but it clearly over-
estimates the true behavioural metric.

We can detect this by computing the greatest fixpoint of
$\mathcal{W}_{\\#}^{d}$, which is

$Y^{\prime}=\\{(x,y),(y,x),(x,z),(z,x),(y,z),(z,y)\\}\neq\emptyset,$

containing the pairs that still have slack in $d$ and whose distances can be
reduced. We explain why $Y^{\prime}=\mathcal{W}_{\\#}^{d}(Y^{\prime})$ by
focussing on the example pair $(x,y)$ and check that
$(x,y)\in\mathcal{W}_{\\#}^{d}(Y^{\prime})$. For this we use the definition of
$\mathcal{W}_{\\#}^{d}$ given in Proposition 6.3.

A valid coupling $t\in\mathcal{D}(X\times X)$ of $\xi(x),\xi(y)$ is given by
$t(x,y)=t(x,z)=\nicefrac{{1}}{{2}}$. It satisfies $u(t)=(\xi(x),\xi(y))$ and
is optimal since it is the only one. We obtain the Wasserstein lifting

$\mathcal{W}(d)(x,y)=d^{\mathcal{D}}(\xi(x),\xi(y))=\min_{t^{\prime}\in\Gamma(\xi(x),\xi(y))}\tilde{\mathcal{D}}d(t^{\prime})=\tilde{\mathcal{D}}d(t)=\nicefrac{{1}}{{2}}\cdot
1+\nicefrac{{1}}{{2}}\cdot 1=1.$

It is left to show that $t\in\tilde{\mathcal{D}}_{\\#}^{d}(Y^{\prime})$, for
which we use the characterization in Proposition 5.3. We have
$\bar{d}(x,y)=\bar{d}(x,z)=(1,1)$ where

$\mathcal{D}\bar{d}(t)=p\in\mathcal{D}Z\text{ with
}p(1,1)=\nicefrac{{1}}{{2}}+\nicefrac{{1}}{{2}}=1.$

From Lemma 5.3 we obtain
$p\in\tilde{\mathcal{D}}_{\\#}^{\pi_{1}}((0,1]\times\\{1\\})$ and by
definition $t\in(\mathcal{D}\bar{d})^{-1}(p)$, i.e.
$t\in\tilde{\mathcal{D}}_{\\#}^{d}(Y^{\prime})$. So we can conclude that
$(x,y)\in\mathcal{W}_{\\#}^{d}(Y^{\prime})$.

######  Example 6.6.

We now consider an example in the non-deterministic setting. Let $X=\\{x,y\\}$
and a coalgebra $\xi\colon X\to\mathcal{P}X$ be given by $\xi(x)=\\{x,y\\}$,
$\xi(y)=\\{x\\}$.

$y$$x$

Since all states have successors, they are in fact bisimilar and hence have
behavioural distance $0$, given by the least fixpoint of $\mathcal{W}$. Now
consider the pseudo-metric $d\colon X\times X\to[0,1]$ with
$d(x,y)=d(y,x)=\nicefrac{{1}}{{2}}$ and $0$ for the reflexive pairs. This is a
also a fixpoint of $\mathcal{W}$ ($d=\mathcal{W}(d)$), but it clearly over-
estimates the true behavioural metric.

We can detect this by computing the greatest fixpoint of
$\mathcal{W}_{\\#}^{d}$, which is

$Y^{\prime}=\\{(x,y),(y,x)\\}\neq\emptyset,$

containing the pairs that still have slack in $d$ and whose distances can be
reduced. We explain why $Y^{\prime}=\mathcal{W}_{\\#}^{d}(Y^{\prime})$ by
focussing on the example pair $(x,y)$ and check that
$(x,y)\in\mathcal{W}_{\\#}^{d}(Y^{\prime})$. For this we use the definition of
$\mathcal{W}_{\\#}^{d}$ given in Proposition 6.3.

A valid (and optimal) coupling $t\in\mathcal{P}(X\times X)$ of $\xi(x),\xi(y)$
is given by $t=\\{(x,x),(y,x)\\}$. It satisfies $u(t)=(\xi(x),\xi(y))$. We
obtain the Wasserstein lifting

$\mathcal{W}(d)(x,y)=d^{\mathcal{P}}(\xi(x),\xi(y))=\min_{t\in\Gamma(\xi(x),\xi(y))}\tilde{\mathcal{P}}d(t)=\tilde{\mathcal{P}}d(t)=\max\\{0,\nicefrac{{1}}{{2}}\\}=\nicefrac{{1}}{{2}}.$

It is left to show that $t\in\tilde{\mathcal{P}}_{\\#}^{d}(Y^{\prime})$, for
which we use the characterization in Proposition 5.3. We have
$\bar{d}(x,x)=\bar{d}(y,y)=(0,0)$,
$\bar{d}(x,y)=\bar{d}(y,x)=(\nicefrac{{1}}{{2}},1)$ and

$\mathcal{P}\bar{d}(t)=S=\\{(0,0),(\nicefrac{{1}}{{2}},1)\\}$

From Lemma 5.3 we obtain
$S\in\tilde{\mathcal{P}}_{\\#}^{\pi_{1}}((\mathbb{M}\backslash\\{0\\})\times\\{1\\})$
and $t\in(\mathcal{P}\bar{d})^{-1}(S)$, i.e.
$t\in\tilde{\mathcal{P}}_{\\#}^{d}(Y^{\prime})$. So we can conclude that
$(x,y)\in\mathcal{W}_{\\#}^{d}(Y^{\prime})$.

##  7\. GS-Monoidality

We will now show that the categories $\mathbb{C}_{f}$ and $\mathbb{A}_{f}$ can
be turned into gs-monoidal categories, making $\\#$ a gs-monoidal functor.
This will give us a way to assemble functions and their approximations
compositionally and this will form the basis for the tool. We first define gs-
monoidal categories in detail (cf. [gh:inductive-graph, Definition 7] and
[fgtc:gs-monoidal-oplax]).

######  Definition 7.1 (gs-monoidal categories).

A _strict gs-monoidal category_ is a strict symmetric monoidal category, where
$\otimes$ denotes the tensor and $e$ its unit and symmetries are given by
$\rho_{a,b}\colon a\otimes b\to b\otimes a$. For every object $a$ there exist
morphisms $\nabla_{a}\colon a\to a\times a$ (_duplicator_) and $!_{a}\colon
a\to e$ (_discharger_) satisfying the axioms given below. (See also their
visualizations as string diagrams in Figure 4.)

  1. (1)

functoriality of tensor:

     * •

$(g\otimes g^{\prime})\circ(f\otimes f^{\prime})=(g\circ
f)\otimes(g^{\prime}\circ f^{\prime})$

     * •

$\mathit{id}_{a\otimes b}=\mathit{id}_{a}\otimes\mathit{id}_{b}$

  2. (2)

monoidality:

     * •

$(f\otimes g)\otimes h=f\otimes(g\otimes h)$

     * •

$f\otimes\mathit{id}_{e}=f=\mathit{id}_{e}\otimes f$

  3. (3)

naturality:

     * •

$(f^{\prime}\otimes
f)\circ\rho_{a,a^{\prime}}=\rho_{b,b^{\prime}}\circ(f\otimes f^{\prime})$

  4. (4)

symmetry:

     * •

$\rho_{e,e}=\mathit{id}_{e}$

     * •

$\rho_{b,a}\circ\rho_{a,b}=\mathit{id}_{a\otimes b}$

     * •

$\rho_{a\otimes
b,c}=(\rho_{a,c}\otimes\mathit{id}_{b})\circ(\mathit{id}_{a}\otimes\rho_{b,c})$

  5. (5)

gs-monoidality:

     * •

$!_{e}=\nabla_{e}=\mathit{id}_{e}$

     * •

coherence axioms:

       * –

$(\mathit{id}_{a}\otimes\nabla_{a})\circ\nabla_{a}=(\nabla_{a}\otimes\mathit{id}_{a})\circ\nabla_{a}$

       * –

$\mathit{id}_{a}=(\mathit{id}_{a}\otimes!_{a})\circ\nabla_{a}$

       * –

$\rho_{a,a}\circ\nabla_{a}=\nabla_{a}$

     * •

monoidality axioms:

       * –

$!_{a\otimes b}=!_{a}\otimes!_{b}$

       * –

$(\mathit{id}_{a}\otimes\rho_{a,b}\otimes\mathit{id}_{b})\circ(\nabla_{a}\otimes\nabla_{b})=\nabla_{a\otimes
b}$

(or, equivalently,
$\nabla_{a}\otimes\nabla_{b}=(\mathit{id}_{a}\otimes\rho_{b,a}\otimes\mathit{id}_{b})\circ\nabla_{a\otimes
b}$)

A functor $F:\mathbb{C}\to\mathbb{D}$ is _gs-monoidal_ if the following holds:

  1. (1)

$\mathbb{C}$ and $\mathbb{D}$ are gs-monoidal categories

  2. (2)

monoidality:

     * •

$F(e)=e^{\prime}$

     * •

$F(a\otimes b)=F(a)\otimes^{\prime}F(b)$

  3. (3)

symmetry:

     * •

$F(\rho_{a,b})=\rho^{\prime}_{F(a),F(b)}$

  4. (4)

gs-monoidality:

     * •

$F(!_{a})=!^{\prime}_{F(a)}$

     * •

$F(\nabla_{a})=\nabla^{\prime}_{F(a)}$

where the primed operators are from category $\mathbb{D}$, the others from
$\mathbb{C}$.

$=$$a\otimes b$$a$$b$$f$$=$$f$$=$$f$$e$$e$$f^{\prime}$$f$$=$$f$$f^{\prime}$
$e$$e$$=$$e$$a$$b$$=$$a\otimes b$$a\otimes b$$c$$=$$a$$b$$c$
$e$$=$$e$$=$$e$$a\otimes b$$=$$a$$b$$a$$b$$=$$a\otimes b$ $=$$=$$a$$a$$=$

Figure 4. String diagrams for the axioms of gs-monoidal categories.

In fact, in order to obtain strict gs-monoidal categories with disjoint union,
we will work with the skeleton categories where every finite set $Y$ is
represented by an isomorphic copy $\\{1,\dots,|Y|\\}$. This enables us to make
disjoint union strict, i.e., associativity holds on the nose and not just up
to isomorphism. In particular for finite sets $Y,Z$, we define disjoint union
as $Y+Z=\\{1,\dots,|Y|,|Y|+1,\dots,|Y|+|Z|\\}$.

[$\mathbb{C}_{f}$ is gs-monoidal] The category $\mathbb{C}_{f}$ with the
following operators is gs-monoidal:

  1. (1)

The tensor $\otimes$ on objects $a\in\mathbb{M}^{Y}$ and $b\in\mathbb{M}^{Z}$
is defined as

$a\otimes b=a+b\in\mathbb{M}^{Y+Z}$

where for $k\in Y+Z$ we have $(a+b)(k)=a(k)$ if $k\leq|Y|$ and
$(a+b)(k)=b(k-|Y|)$ if $|Y|<k\leq|Y|+|Z|$.

On arrows $f\colon a\dashrightarrow b$ and $g\colon a^{\prime}\dashrightarrow
b^{\prime}$ (with $a^{\prime}\in\mathbb{M}^{Y^{\prime}}$,
$b^{\prime}\in\mathbb{M}^{Z^{\prime}}$) tensor is given by

$f\otimes
g\colon\mathbb{M}^{Y+Y^{\prime}}\to\mathbb{M}^{Z+Z^{\prime}},\quad(f\otimes
g)(u)=f(\mathchoice{\mkern
3.0mu\reflectbox{$\displaystyle\vec{\reflectbox{$\mkern-3.0mu\displaystyle
u\mkern 3.0mu$}}$}\mkern-3.0mu}{\mkern
3.0mu\reflectbox{$\textstyle\vec{\reflectbox{$\mkern-3.0mu\textstyle u\mkern
3.0mu$}}$}\mkern-3.0mu}{\mkern
2.0mu\reflectbox{$\scriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptstyle
u\mkern 2.0mu$}}$}\mkern-2.0mu}{\mkern
2.0mu\reflectbox{$\scriptscriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptscriptstyle
u\mkern 2.0mu$}}$}\mkern-2.0mu}_{Y})+g(\vec{u}_{Y})$

for $u\in\mathbb{M}^{Y+Y^{\prime}}$ where $\mathchoice{\mkern
3.0mu\reflectbox{$\displaystyle\vec{\reflectbox{$\mkern-3.0mu\displaystyle
u\mkern 3.0mu$}}$}\mkern-3.0mu}{\mkern
3.0mu\reflectbox{$\textstyle\vec{\reflectbox{$\mkern-3.0mu\textstyle u\mkern
3.0mu$}}$}\mkern-3.0mu}{\mkern
2.0mu\reflectbox{$\scriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptstyle
u\mkern 2.0mu$}}$}\mkern-2.0mu}{\mkern
2.0mu\reflectbox{$\scriptscriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptscriptstyle
u\mkern 2.0mu$}}$}\mkern-2.0mu}_{Y}\in\mathbb{M}^{Y}$ and
$\vec{u}_{Y}\in\mathbb{M}^{Y^{\prime}}$, defined as $\mathchoice{\mkern
3.0mu\reflectbox{$\displaystyle\vec{\reflectbox{$\mkern-3.0mu\displaystyle
u\mkern 3.0mu$}}$}\mkern-3.0mu}{\mkern
3.0mu\reflectbox{$\textstyle\vec{\reflectbox{$\mkern-3.0mu\textstyle u\mkern
3.0mu$}}$}\mkern-3.0mu}{\mkern
2.0mu\reflectbox{$\scriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptstyle
u\mkern 2.0mu$}}$}\mkern-2.0mu}{\mkern
2.0mu\reflectbox{$\scriptscriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptscriptstyle
u\mkern 2.0mu$}}$}\mkern-2.0mu}_{Y}(k)=u(k)$ ($1\leq k\leq|Y|$) and
$\vec{u}_{Y}(k)=u(|Y|+k)$ ($1\leq k\leq|Y^{\prime}|$).

  2. (2)

The symmetry $\rho_{a,b}\colon a\otimes b\dashrightarrow b\otimes a$ for
$a\in\mathbb{M}^{Y}$, $b\in\mathbb{M}^{Z}$ is defined for
$u\in\mathbb{M}^{Y+Z}$ as

$\rho_{a,b}(u)=\vec{u}_{Y}+\mathchoice{\mkern
3.0mu\reflectbox{$\displaystyle\vec{\reflectbox{$\mkern-3.0mu\displaystyle
u\mkern 3.0mu$}}$}\mkern-3.0mu}{\mkern
3.0mu\reflectbox{$\textstyle\vec{\reflectbox{$\mkern-3.0mu\textstyle u\mkern
3.0mu$}}$}\mkern-3.0mu}{\mkern
2.0mu\reflectbox{$\scriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptstyle
u\mkern 2.0mu$}}$}\mkern-2.0mu}{\mkern
2.0mu\reflectbox{$\scriptscriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptscriptstyle
u\mkern 2.0mu$}}$}\mkern-2.0mu}_{Y}.$

  3. (3)

The unit $e$ is the unique mapping $e\colon\emptyset\to\mathbb{M}$.

  4. (4)

The duplicator $\nabla_{a}\colon a\dashrightarrow a\otimes a$ for
$a\in\mathbb{M}^{Y}$ is defined for $u\in\mathbb{M}^{Y}$ as

$\nabla_{a}(u)=u+u.$

  5. (5)

The discharger $!_{a}\colon a\dashrightarrow e$ for $a\in\mathbb{M}^{Y}$ is
defined for $u\in\mathbb{M}^{Y}$ as $!_{a}(u)=e$.

######  Proof 7.2.

In the following let $a\in\mathbb{M}^{Y}$,
$a^{\prime}\in\mathbb{M}^{Y^{\prime}}$, $b\in\mathbb{M}^{Z}$,
$b^{\prime}\in\mathbb{M}^{Z^{\prime}}$, $c\in\mathbb{M}^{W}$,
$c^{\prime}\in\mathbb{M}^{W^{\prime}}$ be objects in $\mathbb{C}_{f}$.

We know that $\mathbb{C}_{f}$ is a well-defined category from Lemma 4.1. We
also note that disjoint unions of non-expansive functions are non-expansive.
Moreover, given $f\colon a\dashrightarrow b$ and $g\colon
a^{\prime}\dashrightarrow b^{\prime}$, that

$\displaystyle(f\otimes g)(a\otimes a^{\prime})=(f\otimes g)(a+a^{\prime})$
$\displaystyle=f(\overleftarrow{(a+a^{\prime})}_{Y})+g(\overrightarrow{(a+a^{\prime})}_{Y})=f(a)+g(a^{\prime})$
$\displaystyle=b+b^{\prime}=b\otimes b^{\prime}.$

Thus $f\otimes g$ is a well-defined arrow $a\otimes a^{\prime}\dashrightarrow
b\otimes b^{\prime}$.

We next verify all the axioms of gs-monoidal categories given in Definition
7.1. In general the calculations are straightforward, but they are provided
here for completeness.

In the sequel we will often use the fact that $\mathchoice{\mkern
3.0mu\reflectbox{$\displaystyle\vec{\reflectbox{$\mkern-3.0mu\displaystyle
u\mkern 3.0mu$}}$}\mkern-3.0mu}{\mkern
3.0mu\reflectbox{$\textstyle\vec{\reflectbox{$\mkern-3.0mu\textstyle u\mkern
3.0mu$}}$}\mkern-3.0mu}{\mkern
2.0mu\reflectbox{$\scriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptstyle
u\mkern 2.0mu$}}$}\mkern-2.0mu}{\mkern
2.0mu\reflectbox{$\scriptscriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptscriptstyle
u\mkern 2.0mu$}}$}\mkern-2.0mu}_{Y}+\vec{u}_{Y}=u$ whenever $Y$ is a subset of
the domain of $u$.

  1. (1)

functoriality of tensor:

     * •

$\mathit{id}_{a\otimes b}=\mathit{id}_{a}\otimes\mathit{id}_{b}$

Let $u\in\mathbb{M}^{Y+Z}$. Then

$\displaystyle(\mathit{id}_{a}\otimes\mathit{id}_{b})(u)=\mathit{id}_{a}(\mathchoice{\mkern
3.0mu\reflectbox{$\displaystyle\vec{\reflectbox{$\mkern-3.0mu\displaystyle
u\mkern 3.0mu$}}$}\mkern-3.0mu}{\mkern
3.0mu\reflectbox{$\textstyle\vec{\reflectbox{$\mkern-3.0mu\textstyle u\mkern
3.0mu$}}$}\mkern-3.0mu}{\mkern
2.0mu\reflectbox{$\scriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptstyle
u\mkern 2.0mu$}}$}\mkern-2.0mu}{\mkern
2.0mu\reflectbox{$\scriptscriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptscriptstyle
u\mkern
2.0mu$}}$}\mkern-2.0mu}_{Y})+\mathit{id}_{b}(\vec{u}_{Y})=\mathchoice{\mkern
3.0mu\reflectbox{$\displaystyle\vec{\reflectbox{$\mkern-3.0mu\displaystyle
u\mkern 3.0mu$}}$}\mkern-3.0mu}{\mkern
3.0mu\reflectbox{$\textstyle\vec{\reflectbox{$\mkern-3.0mu\textstyle u\mkern
3.0mu$}}$}\mkern-3.0mu}{\mkern
2.0mu\reflectbox{$\scriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptstyle
u\mkern 2.0mu$}}$}\mkern-2.0mu}{\mkern
2.0mu\reflectbox{$\scriptscriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptscriptstyle
u\mkern 2.0mu$}}$}\mkern-2.0mu}_{Y}+\vec{u}_{Y}=u=\mathit{id}_{a\otimes b}(u)$

     * •

$(g\otimes g^{\prime})\circ(f\otimes f^{\prime})=(g\circ
f)\otimes(g^{\prime}\circ f^{\prime})$

This is required to hold when both sides are defined. Hence let $f\colon
a\dashrightarrow b$, $g\colon b\dashrightarrow c$, $f^{\prime}\colon
a^{\prime}\dashrightarrow b^{\prime}$, $g^{\prime}\colon
b^{\prime}\dashrightarrow c^{\prime}$ and $u\in\mathbb{M}^{Y+Y^{\prime}}$. We
obtain:

$\displaystyle(g\otimes g^{\prime})\circ(f\otimes f^{\prime})(u)=(g\otimes
g^{\prime})(f(\mathchoice{\mkern
3.0mu\reflectbox{$\displaystyle\vec{\reflectbox{$\mkern-3.0mu\displaystyle
u\mkern 3.0mu$}}$}\mkern-3.0mu}{\mkern
3.0mu\reflectbox{$\textstyle\vec{\reflectbox{$\mkern-3.0mu\textstyle u\mkern
3.0mu$}}$}\mkern-3.0mu}{\mkern
2.0mu\reflectbox{$\scriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptstyle
u\mkern 2.0mu$}}$}\mkern-2.0mu}{\mkern
2.0mu\reflectbox{$\scriptscriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptscriptstyle
u\mkern 2.0mu$}}$}\mkern-2.0mu}_{Y})+f^{\prime}(\vec{u}_{Y}))$
$\displaystyle=g(f(\mathchoice{\mkern
3.0mu\reflectbox{$\displaystyle\vec{\reflectbox{$\mkern-3.0mu\displaystyle
u\mkern 3.0mu$}}$}\mkern-3.0mu}{\mkern
3.0mu\reflectbox{$\textstyle\vec{\reflectbox{$\mkern-3.0mu\textstyle u\mkern
3.0mu$}}$}\mkern-3.0mu}{\mkern
2.0mu\reflectbox{$\scriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptstyle
u\mkern 2.0mu$}}$}\mkern-2.0mu}{\mkern
2.0mu\reflectbox{$\scriptscriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptscriptstyle
u\mkern
2.0mu$}}$}\mkern-2.0mu}_{Y}))+g^{\prime}(f^{\prime}(\vec{u}_{Y}))=((g\circ
f)\otimes(g^{\prime}\circ f^{\prime}))(\mathchoice{\mkern
3.0mu\reflectbox{$\displaystyle\vec{\reflectbox{$\mkern-3.0mu\displaystyle
u\mkern 3.0mu$}}$}\mkern-3.0mu}{\mkern
3.0mu\reflectbox{$\textstyle\vec{\reflectbox{$\mkern-3.0mu\textstyle u\mkern
3.0mu$}}$}\mkern-3.0mu}{\mkern
2.0mu\reflectbox{$\scriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptstyle
u\mkern 2.0mu$}}$}\mkern-2.0mu}{\mkern
2.0mu\reflectbox{$\scriptscriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptscriptstyle
u\mkern 2.0mu$}}$}\mkern-2.0mu}_{Y}+\vec{u}_{Y})$ $\displaystyle=((g\circ
f)\otimes(g^{\prime}\circ f^{\prime}))(u)$

  2. (2)

monoidality:

     * •

$f\otimes\mathit{id}_{e}=f=\mathit{id}_{e}\otimes f$

Let $f\colon a\dashrightarrow b$ and $u\in\mathbb{M}^{Y}$. It holds that:

$\displaystyle(f\otimes\mathit{id}_{e})(u)=(f\otimes\mathit{id}_{e})(u+e)=f(u)+\mathit{id}_{e}(e)$
$\displaystyle=f(u)+e=f(u)=e+f(u)$
$\displaystyle=\mathit{id}_{e}(e)+f(u)=(\mathit{id}_{e}\otimes
f)(e+u)=(\mathit{id}_{e}\otimes f)(u)$

     * •

$(f\otimes g)\otimes h=f\otimes(g\otimes h)$

Let $f\colon a\dashrightarrow a^{\prime}$, $g\colon b\dashrightarrow
b^{\prime}$ and $h\colon c\dashrightarrow c^{\prime}$ and
$u\in\mathbb{M}^{Y+Z+W}$, then

$\displaystyle((f\otimes g)\otimes h)(u)=(f\otimes g)(\mathchoice{\mkern
3.0mu\reflectbox{$\displaystyle\vec{\reflectbox{$\mkern-3.0mu\displaystyle
u\mkern 3.0mu$}}$}\mkern-3.0mu}{\mkern
3.0mu\reflectbox{$\textstyle\vec{\reflectbox{$\mkern-3.0mu\textstyle u\mkern
3.0mu$}}$}\mkern-3.0mu}{\mkern
2.0mu\reflectbox{$\scriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptstyle
u\mkern 2.0mu$}}$}\mkern-2.0mu}{\mkern
2.0mu\reflectbox{$\scriptscriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptscriptstyle
u\mkern 2.0mu$}}$}\mkern-2.0mu}_{Y+Z})+h(\vec{u}_{Y+Z})$
$\displaystyle=(f(\overleftarrow{(\mathchoice{\mkern
3.0mu\reflectbox{$\displaystyle\vec{\reflectbox{$\mkern-3.0mu\displaystyle
u\mkern 3.0mu$}}$}\mkern-3.0mu}{\mkern
3.0mu\reflectbox{$\textstyle\vec{\reflectbox{$\mkern-3.0mu\textstyle u\mkern
3.0mu$}}$}\mkern-3.0mu}{\mkern
2.0mu\reflectbox{$\scriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptstyle
u\mkern 2.0mu$}}$}\mkern-2.0mu}{\mkern
2.0mu\reflectbox{$\scriptscriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptscriptstyle
u\mkern
2.0mu$}}$}\mkern-2.0mu}_{Y+Z})}_{Y})+g(\overrightarrow{(\mathchoice{\mkern
3.0mu\reflectbox{$\displaystyle\vec{\reflectbox{$\mkern-3.0mu\displaystyle
u\mkern 3.0mu$}}$}\mkern-3.0mu}{\mkern
3.0mu\reflectbox{$\textstyle\vec{\reflectbox{$\mkern-3.0mu\textstyle u\mkern
3.0mu$}}$}\mkern-3.0mu}{\mkern
2.0mu\reflectbox{$\scriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptstyle
u\mkern 2.0mu$}}$}\mkern-2.0mu}{\mkern
2.0mu\reflectbox{$\scriptscriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptscriptstyle
u\mkern 2.0mu$}}$}\mkern-2.0mu}_{Y+Z})}_{Y}))+h(\vec{u}_{Y+Z})$
$\displaystyle=f(\mathchoice{\mkern
3.0mu\reflectbox{$\displaystyle\vec{\reflectbox{$\mkern-3.0mu\displaystyle
u\mkern 3.0mu$}}$}\mkern-3.0mu}{\mkern
3.0mu\reflectbox{$\textstyle\vec{\reflectbox{$\mkern-3.0mu\textstyle u\mkern
3.0mu$}}$}\mkern-3.0mu}{\mkern
2.0mu\reflectbox{$\scriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptstyle
u\mkern 2.0mu$}}$}\mkern-2.0mu}{\mkern
2.0mu\reflectbox{$\scriptscriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptscriptstyle
u\mkern
2.0mu$}}$}\mkern-2.0mu}_{Y})+(g(\overleftarrow{(\vec{u}_{Y})}_{Z})+h(\overrightarrow{(\vec{u}_{Y})}_{Z}))$
$\displaystyle=f(\mathchoice{\mkern
3.0mu\reflectbox{$\displaystyle\vec{\reflectbox{$\mkern-3.0mu\displaystyle
u\mkern 3.0mu$}}$}\mkern-3.0mu}{\mkern
3.0mu\reflectbox{$\textstyle\vec{\reflectbox{$\mkern-3.0mu\textstyle u\mkern
3.0mu$}}$}\mkern-3.0mu}{\mkern
2.0mu\reflectbox{$\scriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptstyle
u\mkern 2.0mu$}}$}\mkern-2.0mu}{\mkern
2.0mu\reflectbox{$\scriptscriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptscriptstyle
u\mkern 2.0mu$}}$}\mkern-2.0mu}_{Y})+(g\otimes
h)(\vec{u}_{Y})=(f\otimes(g\otimes h))(u)$

where we use the fact that $\overrightarrow{(\mathchoice{\mkern
3.0mu\reflectbox{$\displaystyle\vec{\reflectbox{$\mkern-3.0mu\displaystyle
u\mkern 3.0mu$}}$}\mkern-3.0mu}{\mkern
3.0mu\reflectbox{$\textstyle\vec{\reflectbox{$\mkern-3.0mu\textstyle u\mkern
3.0mu$}}$}\mkern-3.0mu}{\mkern
2.0mu\reflectbox{$\scriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptstyle
u\mkern 2.0mu$}}$}\mkern-2.0mu}{\mkern
2.0mu\reflectbox{$\scriptscriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptscriptstyle
u\mkern
2.0mu$}}$}\mkern-2.0mu}_{Y+Z})}_{Y}=\overleftarrow{(\vec{u}_{Y})}_{Z}$.

  3. (3)

naturality:

     * •

$(f^{\prime}\otimes
f)\circ\rho_{a,a^{\prime}}=\rho_{b,b^{\prime}}\circ(f\otimes f^{\prime})$

Let $f\colon a\dashrightarrow b$ and $f^{\prime}\colon
a^{\prime}\dashrightarrow b^{\prime}$. Then for
$u\in\mathbb{M}^{Y+Y^{\prime}}$

$\displaystyle(\rho_{b,b^{\prime}}\circ(f\otimes
f^{\prime}))(u)=\rho_{b,b^{\prime}}(f(\mathchoice{\mkern
3.0mu\reflectbox{$\displaystyle\vec{\reflectbox{$\mkern-3.0mu\displaystyle
u\mkern 3.0mu$}}$}\mkern-3.0mu}{\mkern
3.0mu\reflectbox{$\textstyle\vec{\reflectbox{$\mkern-3.0mu\textstyle u\mkern
3.0mu$}}$}\mkern-3.0mu}{\mkern
2.0mu\reflectbox{$\scriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptstyle
u\mkern 2.0mu$}}$}\mkern-2.0mu}{\mkern
2.0mu\reflectbox{$\scriptscriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptscriptstyle
u\mkern 2.0mu$}}$}\mkern-2.0mu}_{Y})+f^{\prime}(\vec{u}_{Y}))$
$\displaystyle=f^{\prime}(\vec{u}_{Y})+f(\mathchoice{\mkern
3.0mu\reflectbox{$\displaystyle\vec{\reflectbox{$\mkern-3.0mu\displaystyle
u\mkern 3.0mu$}}$}\mkern-3.0mu}{\mkern
3.0mu\reflectbox{$\textstyle\vec{\reflectbox{$\mkern-3.0mu\textstyle u\mkern
3.0mu$}}$}\mkern-3.0mu}{\mkern
2.0mu\reflectbox{$\scriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptstyle
u\mkern 2.0mu$}}$}\mkern-2.0mu}{\mkern
2.0mu\reflectbox{$\scriptscriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptscriptstyle
u\mkern 2.0mu$}}$}\mkern-2.0mu}_{Y})=(f^{\prime}\otimes
f)(\vec{u}_{Y}+\mathchoice{\mkern
3.0mu\reflectbox{$\displaystyle\vec{\reflectbox{$\mkern-3.0mu\displaystyle
u\mkern 3.0mu$}}$}\mkern-3.0mu}{\mkern
3.0mu\reflectbox{$\textstyle\vec{\reflectbox{$\mkern-3.0mu\textstyle u\mkern
3.0mu$}}$}\mkern-3.0mu}{\mkern
2.0mu\reflectbox{$\scriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptstyle
u\mkern 2.0mu$}}$}\mkern-2.0mu}{\mkern
2.0mu\reflectbox{$\scriptscriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptscriptstyle
u\mkern 2.0mu$}}$}\mkern-2.0mu}_{Y})=((f^{\prime}\otimes
f)\circ\rho_{a,a^{\prime}})(u)$

  4. (4)

symmetry:

     * •

$\rho_{e,e}=\mathit{id}_{e}$

We note that $e$ is the unique function from $\emptyset$ to $\mathbb{M}$ and
furthermore $e\otimes e=e+e=e$. Then

$\rho_{e,e}(e)=\rho_{e,e}(e+e)=e+e=e=\mathit{id}_{e}(e)$

     * •

$\rho_{b,a}\circ\rho_{a,b}=\mathit{id}_{a\otimes b}$

Let $u\in\mathbb{M}^{Y+Z}$, then:

$(\rho_{b,a}\circ\rho_{a,b})(u)=\rho_{b,a}(\vec{u}_{Y}+\mathchoice{\mkern
3.0mu\reflectbox{$\displaystyle\vec{\reflectbox{$\mkern-3.0mu\displaystyle
u\mkern 3.0mu$}}$}\mkern-3.0mu}{\mkern
3.0mu\reflectbox{$\textstyle\vec{\reflectbox{$\mkern-3.0mu\textstyle u\mkern
3.0mu$}}$}\mkern-3.0mu}{\mkern
2.0mu\reflectbox{$\scriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptstyle
u\mkern 2.0mu$}}$}\mkern-2.0mu}{\mkern
2.0mu\reflectbox{$\scriptscriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptscriptstyle
u\mkern 2.0mu$}}$}\mkern-2.0mu}_{Y})=\mathchoice{\mkern
3.0mu\reflectbox{$\displaystyle\vec{\reflectbox{$\mkern-3.0mu\displaystyle
u\mkern 3.0mu$}}$}\mkern-3.0mu}{\mkern
3.0mu\reflectbox{$\textstyle\vec{\reflectbox{$\mkern-3.0mu\textstyle u\mkern
3.0mu$}}$}\mkern-3.0mu}{\mkern
2.0mu\reflectbox{$\scriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptstyle
u\mkern 2.0mu$}}$}\mkern-2.0mu}{\mkern
2.0mu\reflectbox{$\scriptscriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptscriptstyle
u\mkern 2.0mu$}}$}\mkern-2.0mu}_{Y}+\vec{u}_{Y}=u=\mathit{id}_{a\otimes b}(u)$

     * •

$\rho_{a\otimes
b,c}=(\rho_{a,c}\otimes\mathit{id}_{b})\circ(\mathit{id}_{a}\otimes\rho_{b,c})$

Let $u\in\mathbb{M}^{Y+Z+W}$, then:

$\displaystyle((\rho_{a,c}\otimes\mathit{id}_{b})\circ(\mathit{id}_{a}\otimes\rho_{b,c}))(u)$
$\displaystyle=(\rho_{a,c}\otimes\mathit{id}_{b})(\mathit{id}_{a}(\mathchoice{\mkern
3.0mu\reflectbox{$\displaystyle\vec{\reflectbox{$\mkern-3.0mu\displaystyle
u\mkern 3.0mu$}}$}\mkern-3.0mu}{\mkern
3.0mu\reflectbox{$\textstyle\vec{\reflectbox{$\mkern-3.0mu\textstyle u\mkern
3.0mu$}}$}\mkern-3.0mu}{\mkern
2.0mu\reflectbox{$\scriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptstyle
u\mkern 2.0mu$}}$}\mkern-2.0mu}{\mkern
2.0mu\reflectbox{$\scriptscriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptscriptstyle
u\mkern 2.0mu$}}$}\mkern-2.0mu}_{Y})+\rho_{b,c}(\vec{u}_{Y}))$
$\displaystyle=(\rho_{a,c}\otimes\mathit{id}_{b})(\mathchoice{\mkern
3.0mu\reflectbox{$\displaystyle\vec{\reflectbox{$\mkern-3.0mu\displaystyle
u\mkern 3.0mu$}}$}\mkern-3.0mu}{\mkern
3.0mu\reflectbox{$\textstyle\vec{\reflectbox{$\mkern-3.0mu\textstyle u\mkern
3.0mu$}}$}\mkern-3.0mu}{\mkern
2.0mu\reflectbox{$\scriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptstyle
u\mkern 2.0mu$}}$}\mkern-2.0mu}{\mkern
2.0mu\reflectbox{$\scriptscriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptscriptstyle
u\mkern
2.0mu$}}$}\mkern-2.0mu}_{Y}+\overrightarrow{(\vec{u}_{Y})}_{Z}+\overleftarrow{(\vec{u}_{Y})}_{Z})$
$\displaystyle=\rho_{a,c}(\mathchoice{\mkern
3.0mu\reflectbox{$\displaystyle\vec{\reflectbox{$\mkern-3.0mu\displaystyle
u\mkern 3.0mu$}}$}\mkern-3.0mu}{\mkern
3.0mu\reflectbox{$\textstyle\vec{\reflectbox{$\mkern-3.0mu\textstyle u\mkern
3.0mu$}}$}\mkern-3.0mu}{\mkern
2.0mu\reflectbox{$\scriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptstyle
u\mkern 2.0mu$}}$}\mkern-2.0mu}{\mkern
2.0mu\reflectbox{$\scriptscriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptscriptstyle
u\mkern
2.0mu$}}$}\mkern-2.0mu}_{Y}+\vec{u}_{Y+Z})+\mathit{id}_{b}(\overleftarrow{(\vec{u}_{Y})}_{Z})=\vec{u}_{Y+Z}+\mathchoice{\mkern
3.0mu\reflectbox{$\displaystyle\vec{\reflectbox{$\mkern-3.0mu\displaystyle
u\mkern 3.0mu$}}$}\mkern-3.0mu}{\mkern
3.0mu\reflectbox{$\textstyle\vec{\reflectbox{$\mkern-3.0mu\textstyle u\mkern
3.0mu$}}$}\mkern-3.0mu}{\mkern
2.0mu\reflectbox{$\scriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptstyle
u\mkern 2.0mu$}}$}\mkern-2.0mu}{\mkern
2.0mu\reflectbox{$\scriptscriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptscriptstyle
u\mkern 2.0mu$}}$}\mkern-2.0mu}_{Y}+\overrightarrow{(\mathchoice{\mkern
3.0mu\reflectbox{$\displaystyle\vec{\reflectbox{$\mkern-3.0mu\displaystyle
u\mkern 3.0mu$}}$}\mkern-3.0mu}{\mkern
3.0mu\reflectbox{$\textstyle\vec{\reflectbox{$\mkern-3.0mu\textstyle u\mkern
3.0mu$}}$}\mkern-3.0mu}{\mkern
2.0mu\reflectbox{$\scriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptstyle
u\mkern 2.0mu$}}$}\mkern-2.0mu}{\mkern
2.0mu\reflectbox{$\scriptscriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptscriptstyle
u\mkern 2.0mu$}}$}\mkern-2.0mu}_{Y+Z})}_{Y}$
$\displaystyle=\vec{u}_{Y+Z}+\mathchoice{\mkern
3.0mu\reflectbox{$\displaystyle\vec{\reflectbox{$\mkern-3.0mu\displaystyle
u\mkern 3.0mu$}}$}\mkern-3.0mu}{\mkern
3.0mu\reflectbox{$\textstyle\vec{\reflectbox{$\mkern-3.0mu\textstyle u\mkern
3.0mu$}}$}\mkern-3.0mu}{\mkern
2.0mu\reflectbox{$\scriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptstyle
u\mkern 2.0mu$}}$}\mkern-2.0mu}{\mkern
2.0mu\reflectbox{$\scriptscriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptscriptstyle
u\mkern 2.0mu$}}$}\mkern-2.0mu}_{Y+Z}=\rho_{a\otimes b,c}(u)$

where we use the fact that $\overrightarrow{(\vec{u}_{Y})}_{Z}=\vec{u}_{Y+Z}$
and $\overleftarrow{(\vec{u}_{Y})}_{Z}=\overrightarrow{(\mathchoice{\mkern
3.0mu\reflectbox{$\displaystyle\vec{\reflectbox{$\mkern-3.0mu\displaystyle
u\mkern 3.0mu$}}$}\mkern-3.0mu}{\mkern
3.0mu\reflectbox{$\textstyle\vec{\reflectbox{$\mkern-3.0mu\textstyle u\mkern
3.0mu$}}$}\mkern-3.0mu}{\mkern
2.0mu\reflectbox{$\scriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptstyle
u\mkern 2.0mu$}}$}\mkern-2.0mu}{\mkern
2.0mu\reflectbox{$\scriptscriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptscriptstyle
u\mkern 2.0mu$}}$}\mkern-2.0mu}_{Y+Z})}_{Y}$.

  5. (5)

gs-monoidality:

     * •

$!_{e}=\nabla_{e}=\mathit{id}_{e}$

Since $e$ is the unique function of type $\emptyset\to\mathbb{M}$ and $e+e=e$,
we obtain:

$!_{e}(e)=e=\mathit{id}_{e}(e)=e=e+e=\nabla_{e}(e)$

     * •

coherence axioms:

For $u\in\mathbb{M}^{Y}$, we note that
$\overleftarrow{(u+u)}_{Y}=\overrightarrow{(u+u)}_{Y}=u$.

       * –

$(\mathit{id}_{a}\otimes\nabla_{a})\circ\nabla_{a}=(\nabla_{a}\otimes\mathit{id}_{a})\circ\nabla_{a}$

Let $u\in\mathbb{M}^{Y}$, then:

$\displaystyle((\mathit{id}_{a}\otimes\nabla_{a})\circ\nabla_{a})(u)=(\mathit{id}_{a}\otimes\nabla_{a})(u+u)$
$\displaystyle=\mathit{id}_{a}(u)+\nabla_{a}(u)=u+u+u=\nabla_{a}(u)+\mathit{id}_{a}(u)$
$\displaystyle=(\nabla_{a}\otimes\mathit{id}_{a})(u+u)=(\nabla_{a}\otimes\mathit{id}_{a})(\nabla_{a}(u))$

       * –

$\mathit{id}_{a}=(\mathit{id}_{a}\otimes!_{a})\circ\nabla_{a}$

Let $u\in\mathbb{M}^{Y}$, then:

$\displaystyle((\mathit{id}_{a}\otimes!_{a})\circ\nabla_{a})(u)=(\mathit{id}_{a}\otimes!_{a})(u+u)$
$\displaystyle=\mathit{id}_{a}(u)+!_{a}(u)=\mathit{id}_{a}(u)+e=\mathit{id}_{a}(u)$

       * –

$\rho_{a,a}\circ\nabla_{a}=\nabla_{a}$

Let $u\in\mathbb{M}^{Y}$, then:

$(\rho_{a,a}\circ\nabla_{a})(u)=\rho_{a,a}(u+u)=u+u=\nabla_{a}(u)$

     * •

monoidality axioms:

       * –

$!_{a\otimes b}=!_{a}\otimes!_{b}$

Let $u\in\mathbb{M}^{Y+Z}$, then:

$!_{a\otimes b}(u)=e=e+e=!_{a}(\mathchoice{\mkern
3.0mu\reflectbox{$\displaystyle\vec{\reflectbox{$\mkern-3.0mu\displaystyle
u\mkern 3.0mu$}}$}\mkern-3.0mu}{\mkern
3.0mu\reflectbox{$\textstyle\vec{\reflectbox{$\mkern-3.0mu\textstyle u\mkern
3.0mu$}}$}\mkern-3.0mu}{\mkern
2.0mu\reflectbox{$\scriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptstyle
u\mkern 2.0mu$}}$}\mkern-2.0mu}{\mkern
2.0mu\reflectbox{$\scriptscriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptscriptstyle
u\mkern 2.0mu$}}$}\mkern-2.0mu}_{Y})+!_{b}(\vec{u}_{Y})\\\
=(!_{a}\otimes!_{b})(u)$

       * –

$\nabla_{a}\otimes\nabla_{b}=(\mathit{id}_{a}\otimes\rho_{b,a}\otimes\mathit{id}_{b})\circ\nabla_{a\otimes
b}$

Let $u\in\mathbb{M}^{Y+Z}$, then:

$\displaystyle(\mathit{id}_{a}\otimes\rho_{b,a}\otimes\mathit{id}_{b})(\nabla_{a\otimes
b}(u))=(\mathit{id}_{a}\otimes\rho_{b,a}\otimes\mathit{id}_{b})(u+u)$
$\displaystyle=(\mathit{id}_{a}\otimes\rho_{b,a}\otimes\mathit{id}_{b})(\mathchoice{\mkern
3.0mu\reflectbox{$\displaystyle\vec{\reflectbox{$\mkern-3.0mu\displaystyle
u\mkern 3.0mu$}}$}\mkern-3.0mu}{\mkern
3.0mu\reflectbox{$\textstyle\vec{\reflectbox{$\mkern-3.0mu\textstyle u\mkern
3.0mu$}}$}\mkern-3.0mu}{\mkern
2.0mu\reflectbox{$\scriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptstyle
u\mkern 2.0mu$}}$}\mkern-2.0mu}{\mkern
2.0mu\reflectbox{$\scriptscriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptscriptstyle
u\mkern 2.0mu$}}$}\mkern-2.0mu}_{Y}+\vec{u}_{Y}+\mathchoice{\mkern
3.0mu\reflectbox{$\displaystyle\vec{\reflectbox{$\mkern-3.0mu\displaystyle
u\mkern 3.0mu$}}$}\mkern-3.0mu}{\mkern
3.0mu\reflectbox{$\textstyle\vec{\reflectbox{$\mkern-3.0mu\textstyle u\mkern
3.0mu$}}$}\mkern-3.0mu}{\mkern
2.0mu\reflectbox{$\scriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptstyle
u\mkern 2.0mu$}}$}\mkern-2.0mu}{\mkern
2.0mu\reflectbox{$\scriptscriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptscriptstyle
u\mkern 2.0mu$}}$}\mkern-2.0mu}_{Y}+\vec{u}_{Y})$
$\displaystyle=\mathchoice{\mkern
3.0mu\reflectbox{$\displaystyle\vec{\reflectbox{$\mkern-3.0mu\displaystyle
u\mkern 3.0mu$}}$}\mkern-3.0mu}{\mkern
3.0mu\reflectbox{$\textstyle\vec{\reflectbox{$\mkern-3.0mu\textstyle u\mkern
3.0mu$}}$}\mkern-3.0mu}{\mkern
2.0mu\reflectbox{$\scriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptstyle
u\mkern 2.0mu$}}$}\mkern-2.0mu}{\mkern
2.0mu\reflectbox{$\scriptscriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptscriptstyle
u\mkern 2.0mu$}}$}\mkern-2.0mu}_{Y}+\mathchoice{\mkern
3.0mu\reflectbox{$\displaystyle\vec{\reflectbox{$\mkern-3.0mu\displaystyle
u\mkern 3.0mu$}}$}\mkern-3.0mu}{\mkern
3.0mu\reflectbox{$\textstyle\vec{\reflectbox{$\mkern-3.0mu\textstyle u\mkern
3.0mu$}}$}\mkern-3.0mu}{\mkern
2.0mu\reflectbox{$\scriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptstyle
u\mkern 2.0mu$}}$}\mkern-2.0mu}{\mkern
2.0mu\reflectbox{$\scriptscriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptscriptstyle
u\mkern
2.0mu$}}$}\mkern-2.0mu}_{Y}+\vec{u}_{Y}+\vec{u}_{Y}=\nabla_{a}(\mathchoice{\mkern
3.0mu\reflectbox{$\displaystyle\vec{\reflectbox{$\mkern-3.0mu\displaystyle
u\mkern 3.0mu$}}$}\mkern-3.0mu}{\mkern
3.0mu\reflectbox{$\textstyle\vec{\reflectbox{$\mkern-3.0mu\textstyle u\mkern
3.0mu$}}$}\mkern-3.0mu}{\mkern
2.0mu\reflectbox{$\scriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptstyle
u\mkern 2.0mu$}}$}\mkern-2.0mu}{\mkern
2.0mu\reflectbox{$\scriptscriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptscriptstyle
u\mkern 2.0mu$}}$}\mkern-2.0mu}_{Y})+\nabla_{b}(\vec{u}_{Y})$
$\displaystyle=(\nabla_{a}\otimes\nabla_{b})(\mathchoice{\mkern
3.0mu\reflectbox{$\displaystyle\vec{\reflectbox{$\mkern-3.0mu\displaystyle
u\mkern 3.0mu$}}$}\mkern-3.0mu}{\mkern
3.0mu\reflectbox{$\textstyle\vec{\reflectbox{$\mkern-3.0mu\textstyle u\mkern
3.0mu$}}$}\mkern-3.0mu}{\mkern
2.0mu\reflectbox{$\scriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptstyle
u\mkern 2.0mu$}}$}\mkern-2.0mu}{\mkern
2.0mu\reflectbox{$\scriptscriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptscriptstyle
u\mkern
2.0mu$}}$}\mkern-2.0mu}_{Y}+\vec{u}_{Y})=(\nabla_{a}\otimes\nabla_{b})(u)$

We now turn to the abstract category $\mathbb{A}_{f}$. Note that here
functions have as parameters sets of the form $U\subseteq[Y]^{a}\subseteq Y$.
Hence, (the cardinality of) $Y$ cannot be determined directly from $U$ and we
need extra care with the tensor.

[$\mathbb{A}_{f}$ is gs-monoidal] The category $\mathbb{A}_{f}$ with the
following operators is gs-monoidal:

  1. (1)

The tensor $\otimes$ on objects $a\in\mathbb{M}^{Y}$ and $b\in\mathbb{M}^{Z}$
is again defined as $a\otimes b=a+b$.

On arrows $f\colon a\dashrightarrow b$ and $g\colon a^{\prime}\dashrightarrow
b^{\prime}$ (where $a^{\prime}\in\mathbb{M}^{Y^{\prime}}$,
$b^{\prime}\in\mathbb{M}^{Z^{\prime}}$ and
$f\colon\mathcal{P}([Y]^{a})\to\mathcal{P}([Z]^{b^{\prime}})$,
$g\colon\mathcal{P}([Y^{\prime}]^{a^{\prime}})\to\mathcal{P}([Z^{\prime}]^{b^{\prime}})$
are the underlying functions), the tensor is given by

$f\otimes
g\colon\mathcal{P}([Y+Y^{\prime}]^{a+a^{\prime}})\to\mathcal{P}([Z+Z^{\prime}]^{b+b^{\prime}}),\quad(f\otimes
g)(U)=f(\mathchoice{\mkern
3.0mu\reflectbox{$\displaystyle\vec{\reflectbox{$\mkern-3.0mu\displaystyle
U\mkern 3.0mu$}}$}\mkern-3.0mu}{\mkern
3.0mu\reflectbox{$\textstyle\vec{\reflectbox{$\mkern-3.0mu\textstyle U\mkern
3.0mu$}}$}\mkern-3.0mu}{\mkern
2.0mu\reflectbox{$\scriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptstyle
U\mkern 2.0mu$}}$}\mkern-2.0mu}{\mkern
2.0mu\reflectbox{$\scriptscriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptscriptstyle
U\mkern 2.0mu$}}$}\mkern-2.0mu}_{Y})\mathop{\cup_{Z}}g(\vec{U}_{Y})$

where $\mathchoice{\mkern
3.0mu\reflectbox{$\displaystyle\vec{\reflectbox{$\mkern-3.0mu\displaystyle
U\mkern 3.0mu$}}$}\mkern-3.0mu}{\mkern
3.0mu\reflectbox{$\textstyle\vec{\reflectbox{$\mkern-3.0mu\textstyle U\mkern
3.0mu$}}$}\mkern-3.0mu}{\mkern
2.0mu\reflectbox{$\scriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptstyle
U\mkern 2.0mu$}}$}\mkern-2.0mu}{\mkern
2.0mu\reflectbox{$\scriptscriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptscriptstyle
U\mkern 2.0mu$}}$}\mkern-2.0mu}_{Y}=U\cap\\{1,\dots,|Y|\\}$ and
$\vec{U}_{Y}=\\{k\mid|Y|+k\in U\\}$. Furthermore:

$U\mathop{\cup_{Y}}V=U\cup\\{|Y|+k\mid k\in V\\}\quad\text{(where $U\subseteq
Y$)}$

  2. (2)

The symmetry $\rho_{a,b}\colon a\otimes b\dashrightarrow b\otimes a$ for
$a\in\mathbb{M}^{Y}$, $b\in\mathbb{M}^{Z}$ is defined for
$U\subseteq[Y+Z]^{a+b}$ as

$\rho_{a,b}(U)=\vec{U}_{Y}\mathop{\cup_{Z}}\mathchoice{\mkern
3.0mu\reflectbox{$\displaystyle\vec{\reflectbox{$\mkern-3.0mu\displaystyle
U\mkern 3.0mu$}}$}\mkern-3.0mu}{\mkern
3.0mu\reflectbox{$\textstyle\vec{\reflectbox{$\mkern-3.0mu\textstyle U\mkern
3.0mu$}}$}\mkern-3.0mu}{\mkern
2.0mu\reflectbox{$\scriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptstyle
U\mkern 2.0mu$}}$}\mkern-2.0mu}{\mkern
2.0mu\reflectbox{$\scriptscriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptscriptstyle
U\mkern 2.0mu$}}$}\mkern-2.0mu}_{Y}\subseteq[Z+Y]^{b+a}$

  3. (3)

The unit $e$ is again the unique mapping $e\colon\emptyset\to\mathbb{M}$.

  4. (4)

The duplicator $\nabla_{a}\colon a\dashrightarrow a\otimes a$ for
$a\in\mathbb{M}^{Y}$ is defined for $U\subseteq[Y]^{a}$ as

$\nabla_{a}(U)=U\mathop{\cup_{Y}}U\subseteq[Y+Y]^{a+a}.$

  5. (5)

The discharger $!_{a}\colon a\dashrightarrow e$ for $a\in\mathbb{M}^{Y}$ is
defined for $U\subseteq[Y]^{a}$ as $!_{a}(U)=\emptyset$.

######  Proof 7.3.

Let $a\in\mathbb{M}^{Y}$, $a^{\prime}\in\mathbb{M}^{Y^{\prime}}$,
$b\in\mathbb{M}^{Z}$, $b^{\prime}\in\mathbb{M}^{Z^{\prime}}$,
$c\in\mathbb{M}^{W}$, $c^{\prime}\in\mathbb{M}^{W^{\prime}}$ be objects in
$\mathbb{A}_{f}$.

We know that $\mathbb{A}_{f}$ is a well-defined category from Lemma 4.1. We
note that, disjoint unions of monotone functions are monotone, making the
tensor well-defined.

We now verify the axioms of gs-monoidal categories (see Definition 7.1). The
calculations are mostly straightforward.

In the following we will often use the fact that $\mathchoice{\mkern
3.0mu\reflectbox{$\displaystyle\vec{\reflectbox{$\mkern-3.0mu\displaystyle
U\mkern 3.0mu$}}$}\mkern-3.0mu}{\mkern
3.0mu\reflectbox{$\textstyle\vec{\reflectbox{$\mkern-3.0mu\textstyle U\mkern
3.0mu$}}$}\mkern-3.0mu}{\mkern
2.0mu\reflectbox{$\scriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptstyle
U\mkern 2.0mu$}}$}\mkern-2.0mu}{\mkern
2.0mu\reflectbox{$\scriptscriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptscriptstyle
U\mkern 2.0mu$}}$}\mkern-2.0mu}_{Y}\mathop{\cup_{Y}}\vec{U}_{Y}=U$ whenever
$U\in\mathcal{P}([Z]^{b})$ and $Y\subseteq Z$.

  1. (1)

functoriality of tensor:

     * •

$\mathit{id}_{a\otimes b}=\mathit{id}_{a}\otimes\mathit{id}_{b}$

Let $U\subseteq[Y+Z]^{a+b}$, then:

$\displaystyle(\mathit{id}_{a}\otimes\mathit{id}_{b})(U)=(\mathit{id}_{a}\otimes\mathit{id}_{b})(\mathchoice{\mkern
3.0mu\reflectbox{$\displaystyle\vec{\reflectbox{$\mkern-3.0mu\displaystyle
U\mkern 3.0mu$}}$}\mkern-3.0mu}{\mkern
3.0mu\reflectbox{$\textstyle\vec{\reflectbox{$\mkern-3.0mu\textstyle U\mkern
3.0mu$}}$}\mkern-3.0mu}{\mkern
2.0mu\reflectbox{$\scriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptstyle
U\mkern 2.0mu$}}$}\mkern-2.0mu}{\mkern
2.0mu\reflectbox{$\scriptscriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptscriptstyle
U\mkern 2.0mu$}}$}\mkern-2.0mu}_{Y}\mathop{\cup_{Y}}\vec{U}_{Y})$
$\displaystyle=\mathit{id}_{a}(\mathchoice{\mkern
3.0mu\reflectbox{$\displaystyle\vec{\reflectbox{$\mkern-3.0mu\displaystyle
U\mkern 3.0mu$}}$}\mkern-3.0mu}{\mkern
3.0mu\reflectbox{$\textstyle\vec{\reflectbox{$\mkern-3.0mu\textstyle U\mkern
3.0mu$}}$}\mkern-3.0mu}{\mkern
2.0mu\reflectbox{$\scriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptstyle
U\mkern 2.0mu$}}$}\mkern-2.0mu}{\mkern
2.0mu\reflectbox{$\scriptscriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptscriptstyle
U\mkern
2.0mu$}}$}\mkern-2.0mu}_{Y})\mathop{\cup_{Y}}\mathit{id}_{b}(\vec{U}_{Y})=\mathchoice{\mkern
3.0mu\reflectbox{$\displaystyle\vec{\reflectbox{$\mkern-3.0mu\displaystyle
U\mkern 3.0mu$}}$}\mkern-3.0mu}{\mkern
3.0mu\reflectbox{$\textstyle\vec{\reflectbox{$\mkern-3.0mu\textstyle U\mkern
3.0mu$}}$}\mkern-3.0mu}{\mkern
2.0mu\reflectbox{$\scriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptstyle
U\mkern 2.0mu$}}$}\mkern-2.0mu}{\mkern
2.0mu\reflectbox{$\scriptscriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptscriptstyle
U\mkern
2.0mu$}}$}\mkern-2.0mu}_{Y}\mathop{\cup_{Y}}\vec{U}_{Y}=U=\mathit{id}_{a\otimes
b}(U)$

     * •

$(g\otimes g^{\prime})\circ(f\otimes f^{\prime})=(g\circ
f)\otimes(g^{\prime}\circ f^{\prime})$

Let $f\colon a\dashrightarrow b$, $g\colon b\dashrightarrow c$,
$f^{\prime}\colon a^{\prime}\dashrightarrow b^{\prime}$, $g^{\prime}\colon
b^{\prime}\dashrightarrow c^{\prime}$ and $u\in\mathbb{M}^{Y+Y^{\prime}}$. We
obtain:

$\displaystyle((g\otimes g^{\prime})\circ(f\otimes f^{\prime}))(U)=(g\otimes
g^{\prime})(f(\mathchoice{\mkern
3.0mu\reflectbox{$\displaystyle\vec{\reflectbox{$\mkern-3.0mu\displaystyle
U\mkern 3.0mu$}}$}\mkern-3.0mu}{\mkern
3.0mu\reflectbox{$\textstyle\vec{\reflectbox{$\mkern-3.0mu\textstyle U\mkern
3.0mu$}}$}\mkern-3.0mu}{\mkern
2.0mu\reflectbox{$\scriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptstyle
U\mkern 2.0mu$}}$}\mkern-2.0mu}{\mkern
2.0mu\reflectbox{$\scriptscriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptscriptstyle
U\mkern 2.0mu$}}$}\mkern-2.0mu}_{Y})\mathop{\cup_{Z}}f^{\prime}(\vec{U}_{Y}))$
$\displaystyle=g(f(\mathchoice{\mkern
3.0mu\reflectbox{$\displaystyle\vec{\reflectbox{$\mkern-3.0mu\displaystyle
U\mkern 3.0mu$}}$}\mkern-3.0mu}{\mkern
3.0mu\reflectbox{$\textstyle\vec{\reflectbox{$\mkern-3.0mu\textstyle U\mkern
3.0mu$}}$}\mkern-3.0mu}{\mkern
2.0mu\reflectbox{$\scriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptstyle
U\mkern 2.0mu$}}$}\mkern-2.0mu}{\mkern
2.0mu\reflectbox{$\scriptscriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptscriptstyle
U\mkern
2.0mu$}}$}\mkern-2.0mu}_{Y}))\mathop{\cup_{W}}g^{\prime}(f^{\prime}(\vec{U}_{Y}))=((g\circ
f)\otimes(g^{\prime}\circ f^{\prime}))(\mathchoice{\mkern
3.0mu\reflectbox{$\displaystyle\vec{\reflectbox{$\mkern-3.0mu\displaystyle
U\mkern 3.0mu$}}$}\mkern-3.0mu}{\mkern
3.0mu\reflectbox{$\textstyle\vec{\reflectbox{$\mkern-3.0mu\textstyle U\mkern
3.0mu$}}$}\mkern-3.0mu}{\mkern
2.0mu\reflectbox{$\scriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptstyle
U\mkern 2.0mu$}}$}\mkern-2.0mu}{\mkern
2.0mu\reflectbox{$\scriptscriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptscriptstyle
U\mkern 2.0mu$}}$}\mkern-2.0mu}_{Y}\mathop{\cup_{Y}}\vec{U}_{Y})$
$\displaystyle=((g\circ f)\otimes(g^{\prime}\circ f^{\prime}))(U)$

  2. (2)

monoidality:

     * •

$f\otimes\mathit{id}_{e}=f=\mathit{id}_{e}\otimes f$

Let $f\colon a\dashrightarrow b$ and $U\subseteq[Y]^{a}$. It holds that:

$\displaystyle(f\otimes\mathit{id}_{e})(U)=f(\mathchoice{\mkern
3.0mu\reflectbox{$\displaystyle\vec{\reflectbox{$\mkern-3.0mu\displaystyle
U\mkern 3.0mu$}}$}\mkern-3.0mu}{\mkern
3.0mu\reflectbox{$\textstyle\vec{\reflectbox{$\mkern-3.0mu\textstyle U\mkern
3.0mu$}}$}\mkern-3.0mu}{\mkern
2.0mu\reflectbox{$\scriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptstyle
U\mkern 2.0mu$}}$}\mkern-2.0mu}{\mkern
2.0mu\reflectbox{$\scriptscriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptscriptstyle
U\mkern
2.0mu$}}$}\mkern-2.0mu}_{Y})\mathop{\cup_{Z}}\mathit{id}_{e}(\vec{U}_{Y})=f(U)\mathop{\cup_{Z}}\mathit{id}_{e}(\emptyset)=f(U)\mathop{\cup_{Z}}\emptyset$
$\displaystyle=f(U)=\emptyset\mathop{\cup_{\emptyset}}f(U)=\mathit{id}_{e}(\emptyset)\mathop{\cup_{\emptyset}}f(U)=\mathit{id}_{e}(\mathchoice{\mkern
3.0mu\reflectbox{$\displaystyle\vec{\reflectbox{$\mkern-3.0mu\displaystyle
U\mkern 3.0mu$}}$}\mkern-3.0mu}{\mkern
3.0mu\reflectbox{$\textstyle\vec{\reflectbox{$\mkern-3.0mu\textstyle U\mkern
3.0mu$}}$}\mkern-3.0mu}{\mkern
2.0mu\reflectbox{$\scriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptstyle
U\mkern 2.0mu$}}$}\mkern-2.0mu}{\mkern
2.0mu\reflectbox{$\scriptscriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptscriptstyle
U\mkern
2.0mu$}}$}\mkern-2.0mu}_{\emptyset})\mathop{\cup_{\emptyset}}f(\vec{U}_{\emptyset})$
$\displaystyle=(\mathit{id}_{e}\otimes f)(U)$

where we use $\mathchoice{\mkern
3.0mu\reflectbox{$\displaystyle\vec{\reflectbox{$\mkern-3.0mu\displaystyle
U\mkern 3.0mu$}}$}\mkern-3.0mu}{\mkern
3.0mu\reflectbox{$\textstyle\vec{\reflectbox{$\mkern-3.0mu\textstyle U\mkern
3.0mu$}}$}\mkern-3.0mu}{\mkern
2.0mu\reflectbox{$\scriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptstyle
U\mkern 2.0mu$}}$}\mkern-2.0mu}{\mkern
2.0mu\reflectbox{$\scriptscriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptscriptstyle
U\mkern 2.0mu$}}$}\mkern-2.0mu}_{Y}=U$ and $\vec{U}_{Y}=\emptyset$, since
$U\subseteq Y$, as well as $\mathchoice{\mkern
3.0mu\reflectbox{$\displaystyle\vec{\reflectbox{$\mkern-3.0mu\displaystyle
U\mkern 3.0mu$}}$}\mkern-3.0mu}{\mkern
3.0mu\reflectbox{$\textstyle\vec{\reflectbox{$\mkern-3.0mu\textstyle U\mkern
3.0mu$}}$}\mkern-3.0mu}{\mkern
2.0mu\reflectbox{$\scriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptstyle
U\mkern 2.0mu$}}$}\mkern-2.0mu}{\mkern
2.0mu\reflectbox{$\scriptscriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptscriptstyle
U\mkern 2.0mu$}}$}\mkern-2.0mu}_{\emptyset}=\emptyset$ and
$\vec{U}_{\emptyset}=U$.

     * •

$(f\otimes g)\otimes h=f\otimes(g\otimes h)$

Let $f\colon a\dashrightarrow a^{\prime}$, $g\in\colon b\dashrightarrow
b^{\prime}$ and $h\colon c\dashrightarrow c^{\prime}$ and
$U\subseteq[Y+Z+W]^{a+b+c}$. Then:

$\displaystyle((f\otimes g)\otimes h)(U)=(f\otimes g)(\mathchoice{\mkern
3.0mu\reflectbox{$\displaystyle\vec{\reflectbox{$\mkern-3.0mu\displaystyle
U\mkern 3.0mu$}}$}\mkern-3.0mu}{\mkern
3.0mu\reflectbox{$\textstyle\vec{\reflectbox{$\mkern-3.0mu\textstyle U\mkern
3.0mu$}}$}\mkern-3.0mu}{\mkern
2.0mu\reflectbox{$\scriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptstyle
U\mkern 2.0mu$}}$}\mkern-2.0mu}{\mkern
2.0mu\reflectbox{$\scriptscriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptscriptstyle
U\mkern
2.0mu$}}$}\mkern-2.0mu}_{Y+Z})\mathop{\cup_{Y^{\prime}+Z^{\prime}}}h(\vec{U}_{Y+Z})$
$\displaystyle=\big{(}f(\overleftarrow{(\mathchoice{\mkern
3.0mu\reflectbox{$\displaystyle\vec{\reflectbox{$\mkern-3.0mu\displaystyle
U\mkern 3.0mu$}}$}\mkern-3.0mu}{\mkern
3.0mu\reflectbox{$\textstyle\vec{\reflectbox{$\mkern-3.0mu\textstyle U\mkern
3.0mu$}}$}\mkern-3.0mu}{\mkern
2.0mu\reflectbox{$\scriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptstyle
U\mkern 2.0mu$}}$}\mkern-2.0mu}{\mkern
2.0mu\reflectbox{$\scriptscriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptscriptstyle
U\mkern
2.0mu$}}$}\mkern-2.0mu}_{Y+Z})}_{Y})\mathop{\cup_{Y^{\prime}}}g(\overrightarrow{(\mathchoice{\mkern
3.0mu\reflectbox{$\displaystyle\vec{\reflectbox{$\mkern-3.0mu\displaystyle
U\mkern 3.0mu$}}$}\mkern-3.0mu}{\mkern
3.0mu\reflectbox{$\textstyle\vec{\reflectbox{$\mkern-3.0mu\textstyle U\mkern
3.0mu$}}$}\mkern-3.0mu}{\mkern
2.0mu\reflectbox{$\scriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptstyle
U\mkern 2.0mu$}}$}\mkern-2.0mu}{\mkern
2.0mu\reflectbox{$\scriptscriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptscriptstyle
U\mkern
2.0mu$}}$}\mkern-2.0mu}_{Y+Z})}_{Y})\big{)}\mathop{\cup_{Y^{\prime}+Z^{\prime}}}h(\vec{U}_{Y+Z})$
$\displaystyle=\big{(}f(\mathchoice{\mkern
3.0mu\reflectbox{$\displaystyle\vec{\reflectbox{$\mkern-3.0mu\displaystyle
U\mkern 3.0mu$}}$}\mkern-3.0mu}{\mkern
3.0mu\reflectbox{$\textstyle\vec{\reflectbox{$\mkern-3.0mu\textstyle U\mkern
3.0mu$}}$}\mkern-3.0mu}{\mkern
2.0mu\reflectbox{$\scriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptstyle
U\mkern 2.0mu$}}$}\mkern-2.0mu}{\mkern
2.0mu\reflectbox{$\scriptscriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptscriptstyle
U\mkern
2.0mu$}}$}\mkern-2.0mu}_{Y})\mathop{\cup_{Y^{\prime}}}g(\overleftarrow{(\vec{U}_{Y})}_{Z})\big{)}\mathop{\cup_{Y^{\prime}+Z^{\prime}}}h(\vec{U}_{Y+Z})$
$\displaystyle=f(\mathchoice{\mkern
3.0mu\reflectbox{$\displaystyle\vec{\reflectbox{$\mkern-3.0mu\displaystyle
U\mkern 3.0mu$}}$}\mkern-3.0mu}{\mkern
3.0mu\reflectbox{$\textstyle\vec{\reflectbox{$\mkern-3.0mu\textstyle U\mkern
3.0mu$}}$}\mkern-3.0mu}{\mkern
2.0mu\reflectbox{$\scriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptstyle
U\mkern 2.0mu$}}$}\mkern-2.0mu}{\mkern
2.0mu\reflectbox{$\scriptscriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptscriptstyle
U\mkern
2.0mu$}}$}\mkern-2.0mu}_{Y})\mathop{\cup_{Y^{\prime}}}\big{(}g(\overleftarrow{(\vec{U}_{Y})}_{Z})\mathop{\cup_{Z^{\prime}}}h(\overrightarrow{(\vec{U}_{Y})}_{Z})\big{)}$
$\displaystyle=f(\mathchoice{\mkern
3.0mu\reflectbox{$\displaystyle\vec{\reflectbox{$\mkern-3.0mu\displaystyle
U\mkern 3.0mu$}}$}\mkern-3.0mu}{\mkern
3.0mu\reflectbox{$\textstyle\vec{\reflectbox{$\mkern-3.0mu\textstyle U\mkern
3.0mu$}}$}\mkern-3.0mu}{\mkern
2.0mu\reflectbox{$\scriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptstyle
U\mkern 2.0mu$}}$}\mkern-2.0mu}{\mkern
2.0mu\reflectbox{$\scriptscriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptscriptstyle
U\mkern 2.0mu$}}$}\mkern-2.0mu}_{Y})\mathop{\cup_{Y^{\prime}}}(g\otimes
h)(\vec{U}_{Y})=(f\otimes(g\otimes h))(U)$

where we use $\overleftarrow{(\mathchoice{\mkern
3.0mu\reflectbox{$\displaystyle\vec{\reflectbox{$\mkern-3.0mu\displaystyle
U\mkern 3.0mu$}}$}\mkern-3.0mu}{\mkern
3.0mu\reflectbox{$\textstyle\vec{\reflectbox{$\mkern-3.0mu\textstyle U\mkern
3.0mu$}}$}\mkern-3.0mu}{\mkern
2.0mu\reflectbox{$\scriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptstyle
U\mkern 2.0mu$}}$}\mkern-2.0mu}{\mkern
2.0mu\reflectbox{$\scriptscriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptscriptstyle
U\mkern 2.0mu$}}$}\mkern-2.0mu}_{Y+Z})}_{Y}=\mathchoice{\mkern
3.0mu\reflectbox{$\displaystyle\vec{\reflectbox{$\mkern-3.0mu\displaystyle
U\mkern 3.0mu$}}$}\mkern-3.0mu}{\mkern
3.0mu\reflectbox{$\textstyle\vec{\reflectbox{$\mkern-3.0mu\textstyle U\mkern
3.0mu$}}$}\mkern-3.0mu}{\mkern
2.0mu\reflectbox{$\scriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptstyle
U\mkern 2.0mu$}}$}\mkern-2.0mu}{\mkern
2.0mu\reflectbox{$\scriptscriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptscriptstyle
U\mkern 2.0mu$}}$}\mkern-2.0mu}_{Y}$, $\overrightarrow{(\mathchoice{\mkern
3.0mu\reflectbox{$\displaystyle\vec{\reflectbox{$\mkern-3.0mu\displaystyle
U\mkern 3.0mu$}}$}\mkern-3.0mu}{\mkern
3.0mu\reflectbox{$\textstyle\vec{\reflectbox{$\mkern-3.0mu\textstyle U\mkern
3.0mu$}}$}\mkern-3.0mu}{\mkern
2.0mu\reflectbox{$\scriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptstyle
U\mkern 2.0mu$}}$}\mkern-2.0mu}{\mkern
2.0mu\reflectbox{$\scriptscriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptscriptstyle
U\mkern 2.0mu$}}$}\mkern-2.0mu}_{Y+Z})}_{Y}=\overleftarrow{(\vec{U}_{Y})}_{Z}$
and $\vec{U}_{Y+Z}=\overrightarrow{(\vec{U}_{Y})}_{Z}$.

  3. (3)

naturality:

     * •

$(f^{\prime}\otimes
f)\circ\rho_{a,a^{\prime}}=\rho_{b,b^{\prime}}\circ(f\otimes f^{\prime})$

Let $f\colon a\dashrightarrow b$ and $f^{\prime}\colon
a^{\prime}\dashrightarrow b^{\prime}$. Then for
$U\subseteq[Y+Y^{\prime}]^{a+a^{\prime}}$ it holds that:

$\displaystyle(\rho_{b,b^{\prime}}\circ(f\otimes f^{\prime}))(U)$
$\displaystyle=\rho_{b,b^{\prime}}(f(\mathchoice{\mkern
3.0mu\reflectbox{$\displaystyle\vec{\reflectbox{$\mkern-3.0mu\displaystyle
U\mkern 3.0mu$}}$}\mkern-3.0mu}{\mkern
3.0mu\reflectbox{$\textstyle\vec{\reflectbox{$\mkern-3.0mu\textstyle U\mkern
3.0mu$}}$}\mkern-3.0mu}{\mkern
2.0mu\reflectbox{$\scriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptstyle
U\mkern 2.0mu$}}$}\mkern-2.0mu}{\mkern
2.0mu\reflectbox{$\scriptscriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptscriptstyle
U\mkern 2.0mu$}}$}\mkern-2.0mu}_{Y})\mathop{\cup_{Z}}f^{\prime}(\vec{U}_{Y}))$
$\displaystyle=\overrightarrow{(f(\mathchoice{\mkern
3.0mu\reflectbox{$\displaystyle\vec{\reflectbox{$\mkern-3.0mu\displaystyle
U\mkern 3.0mu$}}$}\mkern-3.0mu}{\mkern
3.0mu\reflectbox{$\textstyle\vec{\reflectbox{$\mkern-3.0mu\textstyle U\mkern
3.0mu$}}$}\mkern-3.0mu}{\mkern
2.0mu\reflectbox{$\scriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptstyle
U\mkern 2.0mu$}}$}\mkern-2.0mu}{\mkern
2.0mu\reflectbox{$\scriptscriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptscriptstyle
U\mkern
2.0mu$}}$}\mkern-2.0mu}_{Y})\mathop{\cup_{Z}}f^{\prime}(\vec{U}_{Y}))}_{Z}\mathop{\cup_{Z^{\prime}}}\overleftarrow{(f(\mathchoice{\mkern
3.0mu\reflectbox{$\displaystyle\vec{\reflectbox{$\mkern-3.0mu\displaystyle
U\mkern 3.0mu$}}$}\mkern-3.0mu}{\mkern
3.0mu\reflectbox{$\textstyle\vec{\reflectbox{$\mkern-3.0mu\textstyle U\mkern
3.0mu$}}$}\mkern-3.0mu}{\mkern
2.0mu\reflectbox{$\scriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptstyle
U\mkern 2.0mu$}}$}\mkern-2.0mu}{\mkern
2.0mu\reflectbox{$\scriptscriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptscriptstyle
U\mkern
2.0mu$}}$}\mkern-2.0mu}_{Y})\mathop{\cup_{Z}}f^{\prime}(\vec{U}_{Y}))}_{Z}$
$\displaystyle=f^{\prime}(\vec{U}_{Y})\mathop{\cup_{Z^{\prime}}}f(\mathchoice{\mkern
3.0mu\reflectbox{$\displaystyle\vec{\reflectbox{$\mkern-3.0mu\displaystyle
U\mkern 3.0mu$}}$}\mkern-3.0mu}{\mkern
3.0mu\reflectbox{$\textstyle\vec{\reflectbox{$\mkern-3.0mu\textstyle U\mkern
3.0mu$}}$}\mkern-3.0mu}{\mkern
2.0mu\reflectbox{$\scriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptstyle
U\mkern 2.0mu$}}$}\mkern-2.0mu}{\mkern
2.0mu\reflectbox{$\scriptscriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptscriptstyle
U\mkern 2.0mu$}}$}\mkern-2.0mu}_{Y})$
$\displaystyle=f^{\prime}(\overleftarrow{(\vec{U}_{Y}\mathop{\cup_{Y^{\prime}}}\mathchoice{\mkern
3.0mu\reflectbox{$\displaystyle\vec{\reflectbox{$\mkern-3.0mu\displaystyle
U\mkern 3.0mu$}}$}\mkern-3.0mu}{\mkern
3.0mu\reflectbox{$\textstyle\vec{\reflectbox{$\mkern-3.0mu\textstyle U\mkern
3.0mu$}}$}\mkern-3.0mu}{\mkern
2.0mu\reflectbox{$\scriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptstyle
U\mkern 2.0mu$}}$}\mkern-2.0mu}{\mkern
2.0mu\reflectbox{$\scriptscriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptscriptstyle
U\mkern
2.0mu$}}$}\mkern-2.0mu}_{Y})}_{Y^{\prime}})\mathop{\cup_{Z^{\prime}}}f(\overrightarrow{(\vec{U}_{Y}\mathop{\cup_{Y^{\prime}}}\mathchoice{\mkern
3.0mu\reflectbox{$\displaystyle\vec{\reflectbox{$\mkern-3.0mu\displaystyle
U\mkern 3.0mu$}}$}\mkern-3.0mu}{\mkern
3.0mu\reflectbox{$\textstyle\vec{\reflectbox{$\mkern-3.0mu\textstyle U\mkern
3.0mu$}}$}\mkern-3.0mu}{\mkern
2.0mu\reflectbox{$\scriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptstyle
U\mkern 2.0mu$}}$}\mkern-2.0mu}{\mkern
2.0mu\reflectbox{$\scriptscriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptscriptstyle
U\mkern 2.0mu$}}$}\mkern-2.0mu}_{Y})}_{Y^{\prime}})$
$\displaystyle=(f^{\prime}\otimes
f)(\vec{U}_{Y}\mathop{\cup_{Y^{\prime}}}\mathchoice{\mkern
3.0mu\reflectbox{$\displaystyle\vec{\reflectbox{$\mkern-3.0mu\displaystyle
U\mkern 3.0mu$}}$}\mkern-3.0mu}{\mkern
3.0mu\reflectbox{$\textstyle\vec{\reflectbox{$\mkern-3.0mu\textstyle U\mkern
3.0mu$}}$}\mkern-3.0mu}{\mkern
2.0mu\reflectbox{$\scriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptstyle
U\mkern 2.0mu$}}$}\mkern-2.0mu}{\mkern
2.0mu\reflectbox{$\scriptscriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptscriptstyle
U\mkern 2.0mu$}}$}\mkern-2.0mu}_{Y})=(f^{\prime}\otimes
f)(\rho_{a,a^{\prime}}(U))$

where we use $\overleftarrow{(U\mathop{\cup_{Y}}V)}_{Y}=U$ and
$\overrightarrow{(U\mathop{\cup_{Y}}V)}_{Y}=V$.

  4. (4)

symmetry:

     * •

$\rho_{e,e}=\mathit{id}_{e}$

Note that the only possibly argument is $\emptyset$ and hence:

$\rho_{e,e}(\emptyset)=\vec{\emptyset}_{\emptyset}\mathop{\cup_{\emptyset}}\mathchoice{\mkern
3.0mu\reflectbox{$\displaystyle\vec{\reflectbox{$\mkern-3.0mu\displaystyle\emptyset\mkern
3.0mu$}}$}\mkern-3.0mu}{\mkern
3.0mu\reflectbox{$\textstyle\vec{\reflectbox{$\mkern-3.0mu\textstyle\emptyset\mkern
3.0mu$}}$}\mkern-3.0mu}{\mkern
2.0mu\reflectbox{$\scriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptstyle\emptyset\mkern
2.0mu$}}$}\mkern-2.0mu}{\mkern
2.0mu\reflectbox{$\scriptscriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptscriptstyle\emptyset\mkern
2.0mu$}}$}\mkern-2.0mu}_{\emptyset}=\emptyset\mathop{\cup_{\emptyset}}\emptyset=\emptyset=\mathit{id}_{e}(\emptyset)$

     * •

$\rho_{b,a}\circ\rho_{a,b}=\mathit{id}_{a\otimes b}$

Let $U\subseteq[Y+Z]^{a+b}$, then:

$\displaystyle(\rho_{b,a}\circ\rho_{a,b})(U)=\rho_{b,a}(\vec{U}_{Y}\mathop{\cup_{Z}}\mathchoice{\mkern
3.0mu\reflectbox{$\displaystyle\vec{\reflectbox{$\mkern-3.0mu\displaystyle
U\mkern 3.0mu$}}$}\mkern-3.0mu}{\mkern
3.0mu\reflectbox{$\textstyle\vec{\reflectbox{$\mkern-3.0mu\textstyle U\mkern
3.0mu$}}$}\mkern-3.0mu}{\mkern
2.0mu\reflectbox{$\scriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptstyle
U\mkern 2.0mu$}}$}\mkern-2.0mu}{\mkern
2.0mu\reflectbox{$\scriptscriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptscriptstyle
U\mkern 2.0mu$}}$}\mkern-2.0mu}_{Y})$
$\displaystyle=\overrightarrow{(\vec{U}_{Y}\mathop{\cup_{Z}}\mathchoice{\mkern
3.0mu\reflectbox{$\displaystyle\vec{\reflectbox{$\mkern-3.0mu\displaystyle
U\mkern 3.0mu$}}$}\mkern-3.0mu}{\mkern
3.0mu\reflectbox{$\textstyle\vec{\reflectbox{$\mkern-3.0mu\textstyle U\mkern
3.0mu$}}$}\mkern-3.0mu}{\mkern
2.0mu\reflectbox{$\scriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptstyle
U\mkern 2.0mu$}}$}\mkern-2.0mu}{\mkern
2.0mu\reflectbox{$\scriptscriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptscriptstyle
U\mkern
2.0mu$}}$}\mkern-2.0mu}_{Y})}_{Z}\mathop{\cup_{Y}}\overleftarrow{(\vec{U}_{Y}\mathop{\cup_{Z}}\mathchoice{\mkern
3.0mu\reflectbox{$\displaystyle\vec{\reflectbox{$\mkern-3.0mu\displaystyle
U\mkern 3.0mu$}}$}\mkern-3.0mu}{\mkern
3.0mu\reflectbox{$\textstyle\vec{\reflectbox{$\mkern-3.0mu\textstyle U\mkern
3.0mu$}}$}\mkern-3.0mu}{\mkern
2.0mu\reflectbox{$\scriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptstyle
U\mkern 2.0mu$}}$}\mkern-2.0mu}{\mkern
2.0mu\reflectbox{$\scriptscriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptscriptstyle
U\mkern 2.0mu$}}$}\mkern-2.0mu}_{Y})}_{Z}=\mathchoice{\mkern