# Fibrational Bisimulations and Quantitative Reasoning

David Sprunger, Shin-Ya Katsumata, Jérémy Dubut, Ichiro Hasuo

► To cite this version:

David Sprunger, Shin-Ya Katsumata, Jérémy Dubut, Ichiro Hasuo. Fibrational Bisimulations and Quantitative Reasoning. 14th International Workshop on Coalgebraic Methods in Computer Science (CMCS), Apr 2018, Thessaloniki, Greece. pp.190-213, 10.1007/978-3-030-00389-0_11 . hal-01901092

HAL Id: hal-01901092

https://hal.science/hal-01901092

Submitted on 21 Feb 2019

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# Fibrational Bisimulations and Quantitative Reasoning

David Sprunger*¹, Shin-ya Katsumata¹, Jérémy Dubut¹,², and Ichiro Hasuo¹

¹ National Institute of Informatics, Tokyo, Japan

² Japanese-French Laboratory for Informatics, CNRS, Tokyo, Japan
{sprunger, s-katsumata, dubut, hasuo}@nii.ac.jp

**Abstract.** *Bisimulation* and *bisimilarity* are fundamental notions in comparing state-based systems. Their extensions to a variety of systems have been actively pursued in recent years, a notable direction being *quantitative* extensions. In this paper we present an abstract categorical framework for such extended (bi)simulation notions. We use coalgebras as system models and fibrations for organizing predicates— following the seminal work by Hermida and Jacobs—but our focus is on the *structural* aspect of fibrational frameworks. Specifically we use morphisms of fibrations as well as canonical liftings of functors via Kan extensions. We apply this categorical framework by deriving some known properties of the Hausdorff pseudometric and approximate bisimulation in control theory.

## 1 Introduction

In the study of transition systems, *bisimulation relations* are a fundamental concept, and their categorical study revealed the importance of *coalgebras*. One approach to characterise bisimilarity is via *liftings* of the coalgebra functor along *fibrations* [12], which are a well-established framework to attach relational structures on categories for modelling transition systems and programming languages [14].

Recently, there is emerging interest in quantitative analysis of transition systems. *Behavioural metrics* were introduced in [7,5] to refine bisimilarity for probabilistic transition systems. Metrics give a real number for each pair of states in a transition system, while a relation can only provide a bit for each pair (whether the pair is in the relation or not). Therefore a metric can indicate a degree to which the behaviour of two states differ, whereas a bisimilarity relation can only indicate whether or not those behaviours differ. From this observation, a common desideratum for behavioral metrics associated with coalgebras is that two states should have distance 0 if and only if they are bisimilar.

Bisimilarity and behavioural metrics are also analogous on a categorical level. *Behavioural metrics* were recently shown to be constructible from liftings of the coalgebra functor to categories of (pseudo)metrics [3,2], similar to how Hermida-Jacobs bisimulations are constructed from liftings of a functor to the category of relations. This type of construction is known generally as a coalgebraic predicate and can be performed when a lifting of the coalgebra functor is known.

These developments present two natural issues. The first is an open-ended quest for liftings of functors in general fibrations. These liftings are the rare ingredient in forming coalgebraic predicates, so having a variety of liftings in a variety of fibrations allows us
to express more coalgebraic predicates. The second issue is more recent and concerns
the desired relationship between behavioural metrics and bisimilarity mentioned above.
Given some liftings in different fibrations, is there a relationship between the liftings
we can use to verify a relationship between the coalgebraic predicates they define on a
given coalgebra?

The main contributions of this paper pertain to these two issues:

- We propose two methods to lift functors along fibrations, both of which generalise existing constructions. The first is the codensity lifting of endofunctors, generalising Baldan et al.'s Kantorovich lifting [3] to arbitrary fibrations. This lifting also represents a further development of the codensity lifting of monads [15]. The second is the construction of an enriched left Kan extension using the canonical symmetric monoidal closed structure [17] on the total category in fibrations. This generalises Balan et al.'s construction [2] of enriched left Kan extension for quantale-enriched small categories.

Apart from these lifting methods, we derive several methods to combine existing
liftings. Using these methods, we construct the *Hausdorff metric* as the pushforward
of the lifting of the list functor along a particular transformation.

- We propose the use of *predicate morphisms* to translate between these liftings. We use these translations to provide facilities for establishing relationships between the coalgebraic predicates provided by these liftings on coalgebras. We illustrate the utility of this approach with two examples. First, we demonstrate the translation of *approximate functions* to *ε-approximate relations*, which is the key technical tool used in control theory. Second, we translate metrics to relations to show the kernels of many behavioural metrics are bisimilarity relations.

*Outline.* In Section 2, we recall the important technical background for this work, par-
ticularly focusing on a class of fibrations where each fibre category is a lattice. In Sec-
tion 3, we recall the construction of Hermida-Jacobs bisimulations and general coalge-
braic predicates. As mentioned above, these require a lifting of a functor. Existence of
such liftings is not guaranteed, and in Section 4 we present a few generalizations of ex-
tant techniques for producing liftings in particular fibrations to our more general class
of fibrations. Finally, in Section 5, we use so-called predicate morphisms to establish
relationships between coalgebraic predicates, focusing on deriving approximate func-
tions from ε-approximate relations and deriving bisimilarity as the kernel of behavioural
metrics.

2 Background

In this paper, we are interested in finding data about a wide variety of state-based tran-
sition systems. This data comes in a variety of types: relations, unary predicates, and
pseudometrics are frequently found in the literature. Data of a particular type can also
satisfy a variety of properties. For example, we are interested in both a relation consist-
ing of the states with exactly the same behaviours, and a relation where the behaviours
of the first member in the pair is a subset of the behaviours of the second member of the
pair.
We capture these degrees of flexibility with three largely orthogonal categorical abstractions. First, we use coalgebras as a means of modeling many kinds of transition systems. Second, fibrations represent the types of data we are interested in deriving about the states of a coalgebra. Finally, functor liftings together with a property of fibrations allow us to model the different ways the same type of data may be created. We review each of these concepts separately here.

We assume familiarity with basic category theory, but not necessarily with the theory of fibrations.

## 2.1 Coalgebras

Coalgebras are our tool of choice for modeling state-based transition systems. Given a **Set** endofunctor $F$, an $F$-coalgebra is a pair $(I, f)$ consisting of a set $I$ and a function $f: I \to FI$. The set is often called the *carrier* of the coalgebra, while the function provides the *transition structure* of the coalgebra.

This pair is usually interpreted as a transition system under the following scheme. The (object part of the) functor $F$ is thought of as an operation which sends a set of states to the set of all possible transition structures on that set. The set $I$ is the set of states of a transition system. Under this interpretation, $FI$ is then set of all the possible transition structures available using the set of states $I$, so the transition structure map $f: I \to FI$ assigns one of these possible transition structures to every state in $I$.

A coalgebra morphism $\phi: (I, f) \to (J, g)$ is a function on the underlying state sets $\phi: I \to J$ which respects the transitions in the source coalgebra, meaning $g \circ \phi = F\phi \circ f$. $F$-coalgebras together with their morphisms form a category we denote by **Coalg**($F$).

By varying the functor $F$, we can capture a wide variety of transition system types, including deterministic and nondeterministic finite automata, Mealy and Moore machines, probabilistic transition systems, Markov decision processes, Segala systems and many more. For more background on the theory of coalgebra, we recommend consulting [20].

## 2.2 Fibrations

A fibration over a category $\mathcal{B}$ is a functor $\pi: \mathcal{B} \to \mathcal{B}$ with a *cartesian lifting property*. We will describe this property later, but intuitively, it allows us to take the inverse image of objects in $\mathcal{B}$ along morphisms in $\mathcal{B}$. The source category of the fibration, $\mathcal{E}$, is referred to as the “total category” and the target is the “base category”.

Often the total category of a fibration is depicted vertically above the base category and language referencing this physical configuration is common. An object or morphism $\dot{a}$ in $\mathcal{E}$ is *above* or *over* an object or morphism $a$ in $\mathcal{B}$ means $\pi\dot{a} = a$. The collection of objects and morphisms above an object $I$ and the id$_I$ morphism is called the *fibre over* $I$. Each of these fibres is itself a subcategory of $\mathcal{E}$, denoted by $\mathcal{E}_I$.

Now we discuss the cartesian lifting property. In a fibration$^3$ over $\mathcal{B}$, for every morphism $f: I \to J$ in $\mathcal{B}$ and every object $Y$ in $\mathcal{E}$ above $J$, there is a morphism $\dot{f}: f^*Y \to Y$

<footnote>$^3$ In this work we always assume that a cleavage is given to a fibration.</footnote>
such that $\dot{f}$ is above $f$ (hence $f^*Y$ is above $I$). This morphism is called a cartesian lifting of $f$ with $Y$ and is further required to satisfy the following universal property: for all morphisms $g : K \to I$ in $\mathbb{B}$ and $\dot{h} : Z \to Y$ in $\mathbb{B}$ above $f \circ g$, there is a unique morphism $\dot{g} : Z \to f^*Y$ above $g$ such that $\dot{h} = \dot{f} \circ \dot{g}$.

The operation sending $Y$ to $f^*Y$ is often called *pullback*.<fnref n="4" />

Pullback also sends morphisms in $\mathbb{E}_J$ to morphisms in $\mathbb{E}_I$ by the universal property. Straightforward checks show that the assignment $Y \mapsto f^*Y$ extends to a functor $f^* : \mathbb{E}_J \to \mathbb{E}_I$. When $g^*f^* = (f \circ g)^*$ and $\mathrm{id}_I^* = \mathrm{Id}_{\mathbb{E}_I}$ holds, we say that the fibration is *split*.

A functor $\pi$ is a cofibration if $\pi^{op} : \mathbb{E}^{op} \to \mathbb{B}^{op}$ is a fibration, and bifibration if $\pi$ and $\pi^{op}$ are fibrations. Pullback in $\pi^{op}$ is denoted by $f_*$, and called *pushforward*. In a bifibration, the pullback $f^*$ is a right adjoint to pushforward $f_*$ [14, Lemma 9.1.2].

A common scenario encountered in the study of fibrations is that each fibre $\mathbb{E}_I$ has a categorical structure, say $X$, and pullback functors preserve these fibrewise structures. When this is the case, we say that the fibration *has fibred* $X$. For instance, a fibration $\pi : \mathbb{E} \to \mathbb{B}$ has *fibred final objects* if 1) each fibre $\mathbb{E}_I$ has a final object, and 2) for any morphism $f : I \to J$, the pullback functor $f^* : \mathbb{E}_J \to \mathbb{E}_I$ preserves final objects. The fibrewise structure and the structure on the total category often have a close relationship. We state it next for the case $X = \text{"limit"}$.

**Theorem 1 ([14]).** Let $\pi : \mathbb{E} \to \mathbb{B}$ be a fibration and $\mathbb{D}$ be a category. If $\mathbb{B}$ has limits of shape $\mathbb{D}$, and $\pi$ has fibred limits of shape $\mathbb{D}$, then $\mathbb{E}$ also has limits of shape $\mathbb{D}$.

The dual version of this theorem also holds, replacing fibration with cofibration, limit with colimit and pullback with pushforward.

We also mention the preservation of fibrations by functor-category construction:

**Theorem 2.** For any fibration $\pi : \mathbb{E} \to \mathbb{B}$ and category $\mathcal{C}$, $\pi \circ - : [\mathcal{C}, \mathbb{E}] \to [\mathcal{C}, \mathbb{B}]$ is also a fibration.

In this work, we are interested in state-based transition systems. Hence, the fibrations we are most interested in have $\mathbb{B} = \text{Set}$. Indeed, most of the total categories we are interested in are sets equipped with some extra structure, such as sets with relations or sets with a metric. In these cases, the forgetful functor is usually a fibration.

**Example 3.** The forgetful functors from the following categories to Set are fibrations:

- **Pre** is the category of preorders and monotone functions between them.

- **ERel** is the category of endorelations. An object is a pair $(I, R)$ of a set $I$ and a relation $R \subseteq I \times I$. Morphisms are functions which preserve the relation, meaning $f : (I, R) \to (J, S)$ is a function $f : I \to J$ such that $i \in I, j \in J, f(i) = f(j)$.

- **RERel** is the category of $\mathbb{R}^+$-indexed endorelations.<fnref n="5" /> That is, an object is a pair $(I, R)$ of $I \in \text{Set}$ and a $\mathbb{R}^+$-indexed family $\{R_\epsilon\}_{\epsilon \in \mathbb{R}^+}$ of endorelations on $I$ monotone in the index, so $\delta \le \epsilon$ implies $R_\delta \subseteq R_\epsilon$. Morphisms are required to preserve the relation at each value $\epsilon$, meaning $i \in R_\epsilon, i' \in R_{\epsilon'}$ implies $f(i) S_\epsilon f(i')$ for all $\epsilon, \epsilon'$.

<footnote n="4">⁴ In this paper we shall use the word *pullback* in this fibralional sense. This usage generalizes the word's common meaning as a limit of a cospan in a category. Specifically, the latter gives a (fibrational) pullback in a codomain fibration. See [14].</footnote>

<footnote n="5">⁵ Throughout this paper, we write $\mathbb{R}^+ = [0, \infty[$.</footnote>
- $\pi$ is a split bifibration. (Each fibre is a poset and each pullback functor $f^* : \mathbb{E}_J \to \mathbb{E}_I$ has a left adjoint $f_* : \mathbb{E}_I \to \mathbb{E}_J$ by the adjoint functor theorem.)

- $\pi$ is faithful and has left and right adjoints, mapping $I \in \mathbf{Set}$ to the least and greatest elements in $\mathbb{E}_I$, respectively. We name the left adjoint $\Delta : \mathbf{Set} \to \mathbb{E}$. Intuitively, it constructs discrete spaces of given sets.

- $\mathbb{E}$ has small limits and colimits by Theorem 1.

- $\pi$ uniquely lifts arbitrary limits and colimits that exist in $\mathbf{Set}$, including large ones. We describe this for the case of colimits. For any diagram $F : \mathcal{D} \to \mathbb{E}$ and a colimiting cocone $\{i_D : \pi F D \to C\}_{D \in \mathcal{D}}$ of $\pi F$ in $\mathbf{Set}$, there exists a unique colimiting cocone $\{i_D : F D \to \dot{C}\}_{D \in \mathcal{D}}$ of $F$ in $\mathbb{E}$ such that $\pi i_D = i_D$. The colimit $\dot{C}$ is given as $\bigvee_{D \in \mathcal{D}} (i_D)_*(F D)$. The same statement holds for coends instead of colimits.

- The change-of-base of a $\mathbf{CLat}_\Lambda$-fibration $\pi : \mathbb{E} \to \mathbf{Set}$ along any $F : \mathbf{Set} \to \mathbf{Set}$ is again a $\mathbf{CLat}_\Lambda$-fibration.

Another less known, but important fact is that the total category $\mathbb{E}$ of any $\mathbf{CLat}_\Lambda$-fibration over $\mathbf{Set}$ carries a canonical (affine) symmetric monoidal closed (SMC for short) structure. The one on **Top** is described in [21, 4]. The following construction of the SMC structure is a reformulation of the one given in [17] using fibred category theory.

**The tensor unit** is a chosen terminal object 1.

**The tensor product** of $X, Y \in \mathbb{E}$ is constructed as follows. Let us define $\pi X \cdot Y$ to be the coproduct of $\pi X$-many copies of $Y$. We explicitly construct it above $\pi X \times \pi Y$ by

$$ \pi X \cdot Y = \bigvee_{x \in \pi X} (x, -)_* Y, $$

where $(x, -) : \pi Y \to \pi X \times \pi Y$ is the function that pairs an argument with a specified $x \in \pi X$. We similarly define $X \cdot \pi Y$ to be the coproduct of $\pi Y$-many copies of $X$, again constructed above $\pi X \times \pi Y$. We then define the tensor product of $X$ and $Y$ to be the join of these two in the fibre over $\pi X \times \pi Y$:

$$ X \otimes Y = (\pi X \cdot Y) \vee (X \cdot \pi Y). $$

This tensor product classifies bi-$\mathbb{E}$-morphisms in the following sense: a function $f$ satisfies $f : X \otimes Y \to Z$ if and only if $f(x, -) : Y \to Z$ and $f(-, y) : X \to Z$ holds for any $x \in \pi X$ and $y \in \pi Y$.

**The closed structure** of $X, Y \in \mathbb{E}$ is constructed as follows. We first construct the product $\pi X \bowtie Y$ of $\pi X$-many copies of $Y$ above $\mathbf{Set}(\pi X, \pi Y)$ by

$$ \pi X \bowtie Y = \bigwedge_{x \in \pi X} (-(x))^* Y, $$

where $-(x) : \mathbf{Set}(\pi X, \pi Y) \to \pi Y$ is the function that evaluates an argument function with a specified $x \in \pi X$. We then define the closed structure $X \to Y$ to be the pullback of $\pi X \bowtie Y$ along the morphism part $\pi_{X,Y} : \mathbb{E}(X, Y) \to \mathbf{Set}(\pi X, \pi Y)$ of $\pi$:

$$ X \to Y = \pi_{X,Y}^*(\pi X \bowtie Y). $$
We note that both $\pi : \mathbb{E} \to \mathbf{Set}$ and its left adjoint $\Delta : \mathbf{Set} \to \mathbb{E}$ are strict symmetric monoidal (for $\mathbf{Set}$ we take the cartesian monoidal structure).

**Example 4.** We illustrate the bifibrational structure of **BVal**. Let us recall the order relation in the fibre categories. The following are equivalent: (1) in the fibre **BVal**<sub>I</sub>, (I, r) ≤ (I, s) holds, (2) id<sub>I</sub> is a nonexpansive function from (I, r) to (I, s), and (3) s(x, y) ≤ r(x, y) holds for all x, y ∈ I. Note the apparent disparity between (1) and (3): though r ≤ s in the fibre order, s has smaller values than r pointwise.

Next, let $(I, r) \in \mathbf{BVal}$ and $H \xrightarrow{f} I \xrightarrow{g} J$ be functions. The pullback $(H, f^*r)$ and the pushforward $(J, g_*r)$ are given by

$$f^*r(x, y) = r(f(x), f(y)), \quad g_*r(x, y) = \inf_{\substack{g(p)=x \\ g(q)=y}} r(p, q).$$

The fibrational construction of the canonical SMC structure on **BVal** yields the following tensor product and closed structure:

$$(I, r) \otimes (J, s) = \left( I \times J, \lambda((x, y), (x', y')) \cdot \begin{cases} \infty & x \neq x' \land y \neq y' \\ s(y, y') & x = x' \land y \neq y' \\ r(x, x') & x \neq x' \land y = y' \\ \min(r(x, x'), s(y, y')) & x = x' \land y = y' \end{cases} \right)$$

$$(I, r) \to (J, s) = \left( \mathbf{BVal}((I, r), (J, s)), \lambda(f, f') \cdot \sup_{x \in I} s(\pi f(x), \pi f'(x)) \right)$$

## 2.4 Liftings

Another major object of study in this work are liftings of a functor. Given a **Set** endo-functor $F$ and two functors $\pi : \mathbb{E} \to \mathbf{Set}$ and $\rho : \mathbb{F} \to \mathbf{Set}$, a *lifting* of $F$ is a functor $\dot{F} : \mathbb{E} \to \mathbb{F}$ such that $\rho \circ \dot{F} = F \circ \pi$. In many of the cases we consider $\pi = \rho$, so $\dot{F}$ is an endofunctor on the domain of $\pi$. To emphasize this particular situation we will call such an $\dot{F}$ an *endolifting*. In [11], endoliftings were called modalities.

Obviously, we will also usually be considering a situation where $\pi$ and $\rho$ are **CLat**<sub>Λ</sub>-fibrations. In such a case, restricting a lifting to a particular fibre yields a functor between fibre categories: $\dot{F}|_I : \mathbb{E}_I \to \mathbb{F}|_I$. Some liftings also specially respect the cartesian morphisms of the fibrations they operate between. A lifting is called a *fibration morphism* if it sends cartesian morphisms in $\mathbb{E}$ to cartesian morphisms in $\mathbb{F}$.

**Notation.** We pause here to set out some notational conventions, some of which have already been used. **Set** is the category of sets and functions. Typical objects of **Set** are denoted $I$, $J$, and $K$ and typical morphisms are denoted $f$, $g$, and $h$. Generally, $F$ is a **Set** endofunctor, $C_I$ is the constant-to-$I$ **Set** endofunctor, $-^*$ is the list functor, and $P_{\text{fin}}$ is the finite (covariant) powerset functor.

Abstract categories are denoted $\mathbb{D}$, $\mathbb{E}$, and $\mathbb{F}$ and are often the total category for a **CLat**<sub>Λ</sub>-fibrations over **Set** with functors $\pi$ or $\rho$. In such a case, applying a dot or two over a **Set**-related entity denotes an entity in the total category above the named **Set**-related entity. For example, $\dot{I}$ is an object in the total category, $\dot{f}$ is a morphism in the
total category, $\times$ is the binary product in the total category, and $\tilde{F}$ is a lifting of $F$ to the total category. We will also generally use $X$, $Y$, and $Z$ as objects in a total category.

Two fibrations—**BVal** and **ERel**—are important enough to merit their own notations. Generally, $r$ and $s$ will denote the function in a **BVal** object, while $R$ and $S$ are the relation in an **ERel** object. Generally, writing a $\hat{\gamma}$ or $\tilde{\gamma}$ over a **Set**-related entity has the same meaning as a dot over that entity, but particularly for the total categories **BVal** and **ERel**, respectively.

The length of a list is denoted len and subscripts shall be used to select an element from a list at the indicated (zero-indexed) list position.

# 3 Endoliftings and invariants

In this section, we describe how **CLat**$_{\Lambda}$-fibrations and liftings of a functor $F$ to that fibration can be used to define data about every $F$-coalgebra. Perhaps the best-known instance of this construction creates Hermida-Jacobs bisimulations from the canonical relation lifting of a functor along **ERel** $\rightarrow$ **Set**. We describe this example first, particularly for polynomial functors $F$.

## 3.1 Relation Liftings Define Coalgebraic Relations

Recall from the previous section the fibration **ERel** has objects consisting of pairs $(I, R)$ where $I$ is a set and $R \subseteq I \times I$ is a relation on that set. The fibre category **ERel**$_I$ is (isomorphic to) the lattice of relations on $I$ with a vertical morphism from $(I, R)$ to $(I, S)$ if and only if $R \subseteq S$.

A consequence of the equivalence between inclusion of relations in a fibre and the existence of a vertical morphism between them is that any functor between fibre categories in **ERel** is necessarily a monotone function on relations with respect to the usual inclusion ordering.

Two important cases where we can apply this fact are (1) **ERel** liftings of functors restricted to a fibre and (2) pullbacks along **Set** functions, since these are both functors between fibre categories. If $\tilde{F}$ is an **ERel** lifting of $F$, then $\tilde{F}|_{\text{ERel}_I}$ is a monotone function $\text{ERel}_I \rightarrow \text{ERel}_{FI}$. Similarly, if $f: I \rightarrow FI$ is an $F$-coalgebra structure on $I$, pullback along $f$ is a monotone function $f^*: \text{ERel}_{FI} \rightarrow \text{ERel}_I$.

Composing the above functions yields a monotone function $f^* \circ \tilde{F}|_{\text{ERel}_{FI}}$ on **ERel**$_I$. Since **ERel**$_I$ is a complete lattice, this composite monotone function has a greatest fixed point, which we denote by $(I, v\tilde{F}_{(I,f)})$. The relation $v\tilde{F}_{(I,f)}$ picked out in this greatest fixed point has historically turned out examples of great interest.

Perhaps foremost among these examples is the so-called canonical relation lifting, which yields bisimilarity as its greatest fixed point. We recall the description of this lifting for polynomial endofunctors.<fnref n="7" /> The *polynomial Set endofunctors* are precisely those generated by the following grammar:

$$ P ::= \text{Id} \mid C_A \mid \coprod_i P_i \mid P_1 \times P_2 $$

<footnote n="7">⁷ The canonical relation lifting can in fact be defined for all functors using image factorization in **Set**. We use the less-general inductive version as we will need it in Section 5.</footnote>
We can create an **ERel** lifting for any polynomial *P* with constructions for each of the inductive cases.

**Definition 5 (canonical relation lifting).** Let $\tilde{\sqcup}$ and $\tilde{\times}$ be the coproduct and binary product operations in **ERel**, respectively. (These exist by Theorem 1.) The canonical relation lifting of a polynomial **Set** functor *P* is:

$$
\mathrm{Rel}(P) = \left\{
\begin{array}{ll}
\mathrm{Id} = \mathrm{Id}_{\mathrm{ERel}} & \text{if } P = \mathrm{Id}_{\mathrm{Set}}, \\
\tilde{C}_A : (I, R) \mapsto (A, \Delta_A) & \text{if } P = C_A, \\
\tilde{\sqcup}_i \mathrm{Rel}(P_i) & \text{if } P = \sqcup_i P_i, \text{ and} \\
\mathrm{Rel}(P_1) \tilde{\times} \mathrm{Rel}(P_2) & \text{if } P = P_1 \times P_2.
\end{array}
\right.
$$

Given a polynomial **Set** functor *P* and a *P*-coalgebra (*I*, *f*), we can use the canonical relation lifting *Rel*(*P*) to form the function *f*\* ◦ *Rel*(*P*)|<sub>ERel<sub>I</sub></sub>. Postfixed points of this function in **ERel<sub>I</sub>** give a useful general definition of bisimulation on (*I*, *f*) [12]. The greatest postfixed point v*Rel*(*P*)<sub>(I,f)</sub> is bisimilarity on this coalgebra.

**Example 6.** As two examples of the canonical relation lifting, we present bisimulation on coalgebras of the list functor and on coalgebras of the finite powerset functor. These examples will be referenced later when we construct behavioural metrics on the same coalgebra types similarly to how we do it here.

The list functor is defined as $(-)^* = \coprod_{n \in \omega} \prod_{i \in n} \mathrm{Id}$. Following the inductive definition above, each summand in the coproduct, $\coprod_n \mathrm{Id}$, sends a relation $R$ to the $n$-fold repetition of $R$: two lists $k, \ell$ of length $n$ are related by $\mathrm{Rel}(\coprod_n \mathrm{Id})(R)$ if $k_i R \ell_i$ holds for $0 \le i < n$. The canonical relation lifting for $\coprod_{n \in \omega} \prod_n \mathrm{Id}$ then relates two lists $k, \ell$ of arbitrary length if and only if $\mathrm{len}(k) = \mathrm{len}(\ell)$ (they come from the same index in the coproduct), and $k_i R \ell_i$ holds for $0 \le i < \mathrm{len}(k)$. In other words, $(k, \ell) \in \mathrm{Rel}(\coprod_n \mathrm{Id})(R)$.

The finite powerset functor is the quotient of the list functor by the transformation
set$_I : I^* \to P_{\text{fin}}I \text{ given by } set_I : (i_1, \dots, i_n) \mapsto \{i_1, \dots, i_n\}$. The pushforward of the
lifting for the list functor along this natural transformation is the usual definition of
bisimulation for the finite powerset functor. Explicitly,

$$
\mathrm{Rel}(P_{\mathrm{fin}})(R) = \{(J, K) \in P_{\mathrm{fin}}I \times P_{\mathrm{fin}}I : \forall j \in J, \exists k \in K. jRk \land \forall k \in K, \exists j \in J. jRk\}
$$

**3.2 Generalizing Hermida-Jacobs Bisimulation**

The necessary components to define Hermida-Jacobs bisimulation conveniently can be
found in any **CLat**<sub>∧</sub>-fibration with any endolifting of any functor. Thus, we can define
the abstract counterpart of a bisimulation. This terminology is intended to echo [11].

**Definition 7.** Let $\dot{F}$ be a endolifting for $F$. An $\dot{F}$-invariant [on an $F$-coalgebra $(I, f)$] is an $\dot{F}$-coalgebra $(X, \alpha)$ [such that $\pi X = I$ and $\pi \alpha = f$].

An $\dot{F}$-invariant morphism is an $\dot{F}$-coalgebra morphism.

$\dot{F}$-invariants and $\dot{F}$-invariant morphisms together form a category, in fact exactly the category **Coalg**($\dot{F}$). $\dot{F}$-invariants also evidently sit over $F$-coalgebras according to $\pi$, so we name the functor sending **Coalg**($\dot{F}$) to **Coalg**($F$).
**Definition 8.** Given a endolifting $\dot{F}$ on a functor $F$, the underlying coalgebra functor $\mathrm{Coalg}(\pi) : \mathrm{Coalg}(\dot{F}) \to \mathrm{Coalg}(F)$ is defined as

$$ \mathrm{Coalg}(\pi)(X, \alpha) = (\pi X, \pi \alpha), \quad \mathrm{Coalg}(\pi)h = h. $$

Since $\pi$ is faithful in a $\mathrm{CLat}_\Lambda$-fibration, the coalgebra structure $\alpha$ of an $\dot{F}$-invariant $(X, \alpha)$ on $(I, f)$ is unique. Therefore, an alternative definition of an $\dot{F}$-invariant on $(I, f)$ is an object $X$ above $I$ such that there exists a (necessarily unique) morphism $\alpha : X \to \dot{F}X$ above $f$.

Yet another definition of an $\dot{F}$-invariant can be derived from the lattice structure of $\mathbb{E}_I$. For each coalgebra $(I, f)$, there is a monotone function $f^* \circ \dot{F}|_{\mathbb{E}_I} : \mathbb{E}_I \to \mathbb{E}_{FI} \to \mathbb{E}_I$ as described above. An $\dot{F}$-invariant on $(I, f)$ is then precisely a postfixed point for this function.

A useful consequence of this last characterization is the observation that since each fibre $\mathbb{E}_I$ is a complete lattice, Knaster-Tarski ensures the $\dot{F}$-invariants on $(I, f)$ form a complete sublattice. In particular

**Definition 9.** The greatest $\dot{F}$-invariant on an $F$-coalgebra $(I, f)$ always exists and is called the $\dot{F}$-coinductive invariant. We denote the $\dot{F}$-coinductive invariant on $(I, f)$ by $v\dot{F}_{(I,f)}$.

We can alternatively reach $v\dot{F}_{(I,f)}$ by the final sequence argument inside the fibre $\mathbb{E}_I$; this is the approach taken in [3]. In [11], coinductive invariants were called coinductive predicates.

$\dot{F}$-similarities give final objects within each fibre category, but there is no assurance of a final object in the total category, nor that final objects are preserved by coalgebra morphisms. The next result, which reorganizes results presented in [11, Section 4], sets out some conditions entailing these desiderata.

**Theorem 10.** Let $\dot{F}$ be a endolifting for $F$. If it preserves cartesian morphisms,

1. [11, Proposition 4.1] The underlying coalgebra functor $\mathrm{Coalg}(\pi) : \mathrm{Coalg}(\dot{F}) \to \mathrm{Coalg}(F)$ is a fibration where pullbacks are the same as in the fibration $\pi$.

2. Each pullback functor of $\mathrm{Coalg}(\pi)$ preserves final objects (hence $\mathrm{Coalg}(\dot{F})$ has fibered final objects).

3. If additionally $\mathrm{Coalg}(F)$ has a final object $vF$, then $\mathrm{Coalg}(\dot{F})$ has a final object.

For the item 2 and 3 of the above theorem, see also [11, Corollary 4.3].

This theorem is a fibred counterpart of some results in Section 6 of [3]. To see this, we instantiate Theorem 10 with the following data: the $\mathrm{CLat}_\Lambda$-fibration $\pi : \mathrm{PMet}_b \to \mathrm{Set}$ (Section 2), a functor $F : \mathrm{Set} \to \mathrm{Set}$ having a final $F$-coalgebra $vF$ and a lifting $\dot{F}$ of $F$ along $\pi$ that preserves cartesian $\mathrm{PMet}_b$ morphisms (isometries). Then

- Theorem 6.1 in [3] is equivalent to the conclusion of (this instance of) item 3 of Theorem 10.

- Let $I = (I, f)$ be an $F$-coalgebra, and $!_I : I \to vF$ be the unique $F$-coalgebra morphism. The behavioural distance of $I$ in [3] corresponds to the pullback $!_I^*(v\dot{F}_{vF})$ in our fibrational language.

- Theorem 6.2 in [3] corresponds to $vF_I = !_I^*(v\dot{F}_{vF})$, which follows from (this instance of) item 2 of Theorem 10.
# 4 Constructions of Liftings along CLat_λ-Fibrations

There are many examples of liftings of functors in well-known fibrations, such as the fibration of relations or pseudometrics. Some of these liftings even form classes which cover all functors, such as the canonical relation lifting or the generalized Kantorovich liftings of [3], which ensure every functor has a lifting in $ERel$ and $PMet_b$ respectively. In this work we are considering a variety of fibrations, so a natural concern is whether liftings of **Set** functors exist in all of these $CLat_λ$-fibrations.

In this section, we generalize a variety of constructions known in particular fibrations to arbitrary $CLat_λ$-fibrations. In Sections 4.1 and 4.2, we give two constructions, the first using enriched left Kan extensions and the second using codensity liftings. Then in Section 4.3 we mention how to use the categorical structure of the $CLat_λ$-fibration to create new liftings from old.

Hence, in this section we find ourselves with the ingredients $F$ and $\pi$:

$$ \mathbf{Set} \xrightarrow{F} \mathbf{Set} \xleftarrow{\pi} \mathbb{E} \quad \pi : \mathbf{CLat}_\lambda\text{-fibration} \quad (1) $$

and seek to create an endolifting of $F$ in a variety of ways.

## 4.1 Lifting by Enriched Left Kan Extensions

The canonical SMC structure on $\mathbb{E}$ (Section 2) allows us to discuss enriched liftings of $F$ to $\mathbb{E}^e$, the self-enriched category of $\mathbb{E}$ with its SMC structure. To discuss this, we introduce some $\mathbb{E}$-categories and $\mathbb{E}$-functors.

- By $\mathbb{E}^e$ we mean the self-enriched $\mathbb{E}$-category of $\mathbb{E}$ (that is, $\mathbb{E}^e(X, Y) = X \to Y$).

- Since the left adjoint $\Delta : \mathbf{Set} \to \mathbb{E}$ of $\pi$ (see Section 2.3) is strict monoidal, it yields the change-of-base 2-functor $\Delta_* : \mathbf{CAT} \to \mathbb{E}\text{-CAT}$. It takes a locally small category $\mathbb{C}$ and returns the $\mathbb{E}$-category $\Delta_*\mathbb{C}$ defined by $\mathbf{Obj}(\Delta_*\mathbb{C}) = \mathbf{Obj}(\mathbb{C})$ and $(\Delta_*\mathbb{C})(I, J) = \Delta(\mathbb{C}(I, J))$.

- For any functor $G : \mathbb{C} \to \mathbb{E}$, we define the $\mathbb{E}$-functor $\underline{G} : \Delta_*\mathbb{C} \to \mathbb{E}^e$ by: $\underline{GI} = GI$, and $\underline{G}_{I,J} : (\Delta_*\mathbb{C})(I, J) \to \mathbb{E}^e(GI, GJ)$ is the mate of $G_{I,J} : \mathbb{C}(I, J) \to \mathbb{E}(GI, GJ)$ with the adjunction $\Delta \dashv \pi$; recall that $\pi(\mathbb{E}^e(X, Y)) = \pi(X \to Y) = \mathbb{E}(X, Y)$ by construction.

The following is a generalisation of [2, Theorem 3.3].

**Theorem 11.** Consider the situation (1). Let $C : \mathbf{Set} \to \mathbb{E}$ be a functor such that $\pi C = F$. Then there is an enriched left Kan extension $\hat{F}$ of $C : \Delta_*\mathbf{Set} \to \mathbb{E}^e$ along $\Delta : \Delta_*\mathbf{Set} \to \mathbb{E}^e$ such that its underlying functor $\hat{F}_0 : \mathbb{E} \to \mathbb{E}$ (see [16]) is a lifting of $F$ along $\pi$.

*Proof.* Since the codomain $\mathbb{E}^e$ of $C$ has $\mathbb{E}$-tensors, the enriched left Kan extension can be computed by the enriched coed:

$$ \mathbf{Lan}_{\underline{\Delta}} \underline{\mathbf{C}} X = \int_{I \in \underline{\Delta}, \mathbf{Set}} \mathbb{E}^e(\underline{\Delta}I, X) \otimes \underline{\mathbf{C}}I; $$

see [16, (4.25)]. We define the body of this coed by $B(I, J) = \mathbb{E}^e(\underline{\Delta}I, X) \otimes \underline{\mathbf{C}}J$. It is an $\mathbb{E}$-functor of type $(\Delta_*\mathbf{Set})^{op} \otimes \Delta_*\mathbf{Set} \to \mathbb{E}^e$. Similarly, we define an ordinary functor
$\bar{B} : \mathbf{Set}^{op} \times \mathbf{Set} \to \mathbb{E}$ by $\bar{B}(I, J) = B(I, J)$ on objects and $\bar{B}(f, g) = \pi B_{(I,J),(I',J')}(f, g)$ on morphisms. A calculation shows that $\bar{B}$ is equal to the ordinary functor $\lambda(I, J)$. $(LI \to X) \otimes CJ$.

Because the codomain of $B$ is $\mathbb{E}^e$, the enriched coed can be computed as an ordinary colimit of the following large diagram in $\mathbb{E}$ [16, Section 2.1]:

<figure><img src="image_2.png" /></figure>

where $I, J$ ranges over all objects in $\mathbf{Set}$, and $l_{I,J}$ and $r_{I,J}$ are the uncurrying of $B(I, -)_{J,I}$ and $B(-, J)_{I,J}$, respectively.

In $\mathbb{E}$, $\Delta I \otimes X$ is a tensor of $X$ with $I \in \mathbf{Set}$ because

$$ \mathbb{E}(\Delta I \otimes X, Y) \approx \mathbb{E}(\Delta I, X \to Y) \approx \mathbf{Set}(I, \pi(X \to Y)) = \mathbf{Set}(I, \mathbb{E}(X, Y)). $$

We name the passage from right to left $\phi$. The bottom objects of diagram (2) are thus tensors of $B(I, J)$ with $\mathbf{Set}(J, I)$ for each $I, J \in \mathbf{Set}$, and moreover, by easy calculation, we have $l_{I,J} = \phi(\bar{B}(I, -))$ and $r_{I,J} = \phi(\bar{B}(-, J))$. Therefore a colimit of the diagram (2) can be computed as an ordinary coed of $\bar{B} : \mathbf{Set}^{op} \times \mathbf{Set} \to \mathbb{E}$.

To compute this (large) coed of $\bar{B}$, it suffices to show that the coed of $\pi \bar{B}$ exists in $\mathbf{Set}$, because $\pi$ uniquely lifts coeds. We have a natural isomorphism $\iota_{I,J} : \pi \bar{B}(I, J) \to \mathbf{Set}(I, \pi X) \times FJ$, and the right hand side has a coed $\{i_I : \mathbf{Set}(I, \pi X) \times F I \to F \pi X\}_{I \in \mathbf{Set}}$ defined by $i_I(f, x) = Ffx$. Therefore since $\pi$ uniquely lifts colimits (Section 2.3), we obtain a coed of $\bar{B}$. To summarise, the enriched left Kan extension is computed as

$$ \mathbf{Lan}_{\Delta} CX = \bigvee_{I \in \mathbf{Set}} (i_I \circ \iota_{I,I})_* ((LI \to X) \otimes CI). $$

*Example 12.* Let $\pi : \mathbf{Pre} \to \mathbf{Set}$ be the $\mathbf{CLat}_\lambda$-fibration from the category $\mathbf{Pre}$ of preorders and $F : \mathbf{Set} \to \mathbf{Set}$ be a functor. We compute the enriched left Kan extension $\mathbf{Lan}_{\Delta \mathbf{AF}}$. For $(X, \leq) \in \mathbf{Pre}$, the enriched left Kan extension $\mathbf{Lan}_{\Delta \mathbf{AF}}(X, \leq_X)$ is the pre-order on $FX$ generated from the following binary relation:

$$ \begin{aligned} & \{(Ffa, Fga) \mid I \in \mathbf{Set}, a \in FI, f, g \in \mathbf{Set}(I, X), \forall i \in I. \text{ fi} \leq_X \text{ gi}\} \\ & = \{(Fp_1a, Fp_2a) \mid a \in F(\leq_X)\} \end{aligned} $$

where $p_i : (\leq_X) \to X$ is the composite of the inclusion $(\leq_X) \hookrightarrow X \times X$ of the preorder relation and the projection function $\pi_i : X \times X \to X$.

When $F$ is the powerset functor $P$, the enriched left Kan extension $\mathbf{Lan}_{\Delta \mathbf{AP}}(X, \leq_X)$ gives the *Egli-Milner* preorder $\sqsubseteq_X$ on $PX$, as computed in [2, Example 3.8]:

$$ V \sqsubseteq_X W \iff (\forall v \in V. \exists w \in W. v \leq_X w) \wedge (\forall w \in W. \exists v \in V. v \leq_X w). $$

## 4.2 Codensity Lifting of Endofunctors

As an analog to the codensity lifting of *monads* along $\mathbf{CLat}_\lambda$-fibrations [15, Proposition 10], we give a method to lift $\mathbf{Set-endofunctors}$ along $\mathbf{CLat}_\lambda$-fibrations. We retain the
name and call it the codensity lifting (of **Set**-endofunctors). We demonstrate in Example 15 that it subsumes the Kantorovich lifting in [3].

Consider the situation (1). We take the category **Set**<sup>*F*</sup> of *F*-algebras and the associated forgetful functor **U**: **Set**<sup>*F*</sup> → **Set**. It comes with a natural transformation **α**: *FU* → **U**, whose components are defined by the *F*-algebra structure: α<sub>(A,a)</sub> = **a**: *FA* → **A**.

The codensity lifting of *F* is defined with respect to a *lifting parameter* for *F*, which is a pair (*R*, *S*) of functors from a discrete category **A** such that π*S* = *UR*:

$$
\begin{tikzcd}
  \mathbf{A} \arrow[r, "S"] \arrow[d, "R"] & \mathbf{B} \arrow[d, "\pi"] \\
  \mathbf{Set}^F \arrow[r, "U"] & \mathbf{Set}
\end{tikzcd}
\qquad
\begin{array}{l}
\mathbf{Set}^F : \text{category of } \mathbf{F}\text{-algebras} \qquad (3) \\
\mathbf{U} : \text{forgetful functor} \\
\pi S = \mathbf{UR}
\end{array}
$$

Then the codensity lifting $F^{[R,S]}$ of $F$ with respect to the above lifting parameter $(R, S)$ is defined by the following fibred meet:

$$
F^{[R,S]} X = \bigwedge_{A \in \mathcal{A}, f \in \mathcal{B}(X, SA)} (\alpha_{RA} \circ F\pi f)^*(SA).
$$

The codensity lifting can be characterised as a vertex of a pullback when the co-density monad **Ran**<sub>S</sub> *S* exists. Suppose that **Ran**<sub>S</sub> *S* exists. Since the **CLat**<sub>∧</sub>-fibration π : E → **Set** preserves all limits, π**Ran**<sub>S</sub> *S* is a right Kan extension of π*S* along *S*. We then take the mate of the natural transformation α*R* : Fπ*S* → π*S* with the right Kan extension of π*S* along *S*, and obtain α*R* : Fπ → π**Ran**<sub>S</sub> *S*.

**Theorem 13.** Suppose that $\mathbf{Ran}_S S$ exists. Then $F^{[R,S]}$ is the vertex of the following pullback in the fibration $[\mathbb{E}, p] : [\mathbb{E}, \mathbb{E}] \to [\mathbb{E}, \mathbf{Set}]$:

$$
\begin{tikzcd}
  F^{[R,S]} \arrow[r, "\mathbf{Ran}_S S"] & [\mathbb{E}, \mathbb{E}] \\
  F\pi \arrow[r, "\overline{\alpha R} \to \pi \mathbf{Ran}_S S"'] & [\mathbb{E}, \mathbf{Set}]
\end{tikzcd}
$$

The codensity lifting enjoys the following universal property. First, we introduce a partial order on the liftings of *F* by: *F̂* ≤ *F̃* if and only if *F̂*X ≤ *F̃*X holds for all *X* ∈ E. Moreover, we say that a lifting *F̂* of *F* along *π* makes *S* an algebra above *R* if, α<sub>RA</sub>: *F̂*SA → SA holds for all A ∈ A.

**Theorem 14.** Consider the situation (1) and a lifting parameter given as (3). The codensity lifting $F^{[R,S]}$ of $F$ is the largest lifting of $F$ that makes $S$ an algebra above $R$.

*Example 15.* Fix a bound *b* ∈ (0, ∞] for metrics. We show that the Kantorovich lifting in [3] is a codensity lifting along the **CLat**<sub>∧</sub>-fibration π : **PMet**<sub>*b*</sub> → **Set**. Let α : F[0, *b*) → [0, *b*) be an *F*-algebra; in [3] it is called an evaluation function. We then form the following lifting parameter: **A** = 1, *R* = ([0, *b*], α), and *S* = ([0, *b*], *d*<sub>*e*</sub>),
where $d_e$ is the standard Euclidean distance $d_e(x, y) = |x - y|$ on $[0, b]$. Then the codensity lifting with this parameter yields the following construction of pseudometric:

$$F^{[R,S]}(I, r) = (FI, r') \\ r'(x, y) = \sup \{|\alpha((F\pi f)(x)) - \alpha((F\pi f)(y))| \mid f \in \mathbf{PMet}_b((I, r), S)\}.$$

This is exactly the Kantorovich lifting in [3, Definition 3.1].

## 4.3 Combining Liftings

We have seen two methods to lift endofunctors. In this section, we discuss building new liftings from existing ones. Below we set up a suitable category in which these operations are characterised as categorical constructions.

Let $\pi : \mathbb{E} \to \mathbf{Set}$ be a CLat$_\Lambda$-fibration. Then $\pi \circ - : [\mathbb{E}, \mathbb{E}] \to [\mathbb{E}, \mathbf{Set}]$ is a partial order bifibration with fibred meets of arbitrary size. We take the following change-of-base of this fibration along $- \circ \pi$:

<figure><img src="image_3.png" /></figure>

The vertex of this change-of-base is the category $\mathbf{Lift}(\pi)$ of liftings along $\pi$. An object is a pair $(F, \dot{F})$ of an endofunctor $F : \mathbf{Set} \to \mathbf{Set}$ and its lifting $\dot{F} : \mathbb{E} \to \mathbb{E}$ along $\pi$. A morphism from $(F, \dot{F})$ to $(G, \dot{G})$ is a pair $(\alpha, \dot{\alpha})$ of natural transformations $\alpha : F \to G$ and $\dot{\alpha} : \dot{F} \to \dot{G}$ such that $\pi\dot{\alpha} = \alpha\pi$.

The derived vertical leg $q : \mathbf{Lift}(\pi) \to [\mathbf{Set}, \mathbf{Set}]$ is also a partial order bifibration with fibred meets (of arbitrary size). Since $[\mathbf{Set}, \mathbf{Set}]$ has small limits and colimits, by Theorem 1, $\mathbf{Lift}(\pi)$ has small limits and colimits, hence small products and coproducts.

The bifibredness of $q$, together with these products and coproducts give us a recipe to combine liftings.

**Identity and Constant** The lifting of $\mathrm{Id}_{\mathrm{Set}}$ is $\mathrm{Id}_{\mathbb{E}}$, while the lifting of the constant function $C_I(J) \equiv I$ is $\dot{C}_I(X) \equiv \Delta I$.

**Product and Coproduct** Let $(F_i, \dot{F}_i)$ be an $I$-indexed family of liftings along $\pi$. Then their product and coproduct are computed pointwise.

**Pullbacks and Pushforwards** For a lifting $(F, \dot{F})$ along $\pi$ and natural transformations $H \xrightarrow{\alpha} F \xrightarrow{\beta} G$, the pullback lifting $\alpha^* F$ above $H$ and pushforward lifting $\beta_* F$ above $G$ are computed pointwise in the fibration $\pi : \mathbb{E} \to \mathbf{Set}$:

$$(\alpha^* \dot{F})(X) = (\alpha_{\pi X})^* (\dot{F} X), \qquad (\beta_* \dot{F})(X) = (\beta_{\pi X})_* (\dot{F} X).$$

In particular, these constructions ensure all polynomial and finitary functors in $\mathbf{Set}$ have at least one lifting in every CLat$_\Lambda$-fibration.
## 4.4 The Hausdorff Pseudometric

As an example of how liftings can be constructed with these basic operations, we demonstrate the construction of the Hausdorff pseudometric on finite sets in a **BVal** lifting of the finite powerset functor. Our version of the Hausdorff distance will take a **BVal** object (I, d) and create a **BVal** object ($P_{\text{fin}}I$, Hd).

Recall that the finite powerset can be realized as a quotient of a polynomial functor with the following construction. First, recall the list functor: $(-)^* = \coprod_{n \in \omega} \coprod_{i \in n}$ Id. This is patently a polynomial functor. Then the finite powerset functor is the quotient of the list functor by the natural transformation $\text{set}_I : I^* \to P_{\text{fin}}I$ from Example 6.

We can build up a **BVal** lifting of the finite powerset functor in parallel with this construction. First, using the product and coproduct in **BVal** we derive a **BVal** lifting for the list functor. Given a **BVal** object (I, d) the lifted distance on lists $k, \ell \in I^*$ is:

$$d^*(k, \ell) = \begin{cases} \max_{0 \le i < \text{len}(k)} d(k_i, \ell_i) & \text{if } \text{len}(k) = \text{len}(\ell) \\ \infty & \text{if } \text{len}(k) \neq \text{len}(\ell) \end{cases}$$

Then a **BVal** lifting for the finite powerset functor arises as the pushforward of the list lifting along the transformation set. In Example 4, we found pushforward in **BVal** explicitly so, $\mathcal{H}d(J, K) = \inf_{\substack{k \in I^* : \text{set}(k)=J \\ \ell \in I^* : \text{set}(\ell)=K}} d^*(k, \ell)$. We have denoted this distance $\mathcal{H}d$ since

it turns out to be equal to the usual Hausdorff distance. However, this is not the usual formulation for the Hausdorff distance, so we briefly discuss why this is equivalent.

The usual definition of Hausdorff distance for a metric space is

$$\mathcal{H}d(J, K) = \max \left( \sup_{y \in J} \inf_{z \in K} d(y, z), \sup_{z \in K} \inf_{y \in J} d(y, z) \right)$$

where $J, K \subseteq I$. Typically the Hausdorff distance is also restricted to nonempty compact subsets of the metric space so that $\mathcal{H}d$ is truly a metric. (Otherwise $\mathcal{H}d(J, K) = 0$ does not imply $J = K$, for example.) Since we are interested in pseudometrics anyway, we do not place any such restriction on the domain of $\mathcal{H}d$.

In the finite case, the Hausdorff distance has a game theoretic interpretation as the result of a two-turn game played between a lazy walker (Gerry) and an antagonist (Tony). In the first round, Tony picks a starting point from either $J$ or $K$ for Gerry. In the second round, Gerry walks from Tony's starting point in $J$ ($K$) to any point in $K$ ($J$). The result of the game is the distance Gerry walks. Gerry's goal is to minimize this distance; Tony's goal is to maximize it.

Gerry's optimal strategy is straightforward. Given a starting point, Gerry finds the distances to the (finitely many) points in the other set and picks the least one. Since Gerry's optimal strategy is clear, Tony can make a list consisting of all the points in $J \cup K$ and the distance Gerry will have to walk if that point is used as the starting point. Then Tony's optimal strategy is to pick the starting point corresponding to the greatest distance on this list.

This analysis indicates we can interchange the order of the players and obtain a game with the same result: Gerry can first announce where he will walk given every
possible choice of starting point, then Tony picks one of the choices offered by Gerry. If Tony is given two lists $k$ and $\ell$ by Gerry, he will be to force the result of this modified game to be

$$d^*(k, \ell)$$

where $d^*$ is the list distance defined above. Gerry's best strategy is to pick $k$ and $\ell$ with the closest corresponding distances possible, making the final result of this modified game

$$\inf_{\substack{k \in I^*: \mathrm{set}(k)=J \\ \ell \in I^*: \mathrm{set}(\ell)=K}} d^*(k, \ell)$$

where the constraints $\mathrm{set}(k) = J$ and $\mathrm{set}(\ell) = K$ express the fact that Gerry must make a choice for every single starting point. Since these games have the same result, we know

$$\max \left( \sup_{y \in J} \inf_{z \in K} d(y, z), \sup_{z \in K} \inf_{y \in J} d(z, y) \right) = \inf_{\substack{k \in I^*: \mathrm{set}(k)=J \\ \ell \in I^*: \mathrm{set}(\ell)=K}} d^*(k, \ell)$$

Therefore, our formulation of the Hausdorff distance is equal to the usual formulation of the Hausdorff distance, modulo the consideration that we are satisfied with a pseudometric and so do not confine our definition to nonempty compact sets.<fnref n="8" />

# 5 The Category of Endoliftings

In Section 3, we defined endoliftings and their instantiations to $\dot{F}$-invariants on particular coalgebras. We showed that with certain constraints on the ambient categories, the $\dot{F}$-coinductive invariant exists and is preserved by coalgebra morphisms. In Section 4, we showed that endoliftings exist in many $CLat_\wedge$-fibrations, and gave several constructions and combinators for producing endoliftings in these general conditions. In this section, we observe that endoliftings can be collected into a category using the following definition.

**Definition 16.** A endolifting morphism from one endolifting ($\pi : \mathbb{E} \to Set, \dot{F}$) to another ($\rho : \mathbb{F} \to Set, \dot{F}$) is a lifting $H : \mathbb{E} \to \mathbb{F}$ of $\mathrm{Id}_{Set}$ (i.e. $\pi = \rho \circ H$) such that $H \circ \dot{F} = \dot{F} \circ H$.

Endolifting morphisms do not appear in the story of Hermida-Jacobs bisimulations or the coalgebraic predicates defined analogously, but we will observe this category is a useful abstraction for comparing coalgebraic invariants of various endoliftings.

A concrete goal in this section is to establish some general conditions under which a **BVal** coinductive invariant has an **ERel** coinductive invariant at its kernel. Results of this type are pursued, for example, in [6].

<footnote n="8">⁸ A more technical proof of the same result proceeds by first showing the Hausdorff distance on the left is a lower bound for $d^*(k, \ell)$ given the constraints on $k$ and $\ell$. The fact that $J$ and $K$ are finite is crucial so that the value of the left-hand side must be witnessed at a particular entry in one of the lists. Then it can be shown that this lower bound is sharp by a particular choice of $k$ and $\ell$ witnessing Gerry's optimal strategy, so indeed the left-hand side is the greatest lower bound for the collection of values on the right-hand side.</footnote>
## 5.1 Quantitative and Qualitative Liftings

We begin by focusing on three CLat$_{λ}$-fibrations introduced in Section 2.3, namely ERel, RRel, and BVal. These total categories consist of sets together with endorelations, real-indexed families of endorelations, and “distance” functions (which satisfy no metric axioms other than having codomain nonnegative reals), respectively.

These fibrations have many functors between them:

<figure><img src="image_4.png" /></figure>

where (the object parts of) each of these functors are given by

$$L(I, R) = (I, \lambda(x, y) . \inf\{\delta | (x, y) \in R_{\delta}\}) \quad S(I, r) = (I, \lambda\epsilon . \{(x, y) \in I | r(x, y) \le \epsilon\})$$

$$\chi_{\epsilon}(I, R) = \begin{pmatrix} I, \lambda\delta . \begin{cases} (I, \emptyset) & \text{if } \delta < \epsilon \\ (I, R) & \text{if } \delta \ge \epsilon \end{cases} \\ (I, R)\epsilon = (I, R\epsilon) \end{pmatrix}$$

Note that the two functors between ERel and RRel are actually a real-indexed family of functors, where $\epsilon \in [0, \infty)$. It may help to think of S as Stratifying a distance function into a family of relations and L as finding the Least index where the relation holds. As usual, the empty infimum in the definition of L is the maximum element, namely $\infty$.

These functors patently do not change the index set I associated with each of the objects in the total category. Each of these functors is also defined to be the identity on morphisms.<fnref n="9" /> Therefore, these are liftings of the identity on Set.

We define the composite functor $T\epsilon = (-\epsilon) \circ S$. This functor sends $(I, r) \in BVal$ to $(I, \{(x, y) | r(x, y) \le \epsilon\}) \in ERel$, truncating the distance function r at $\epsilon$. The fact that $T\epsilon$ is a right adjoint, as depicted in the diagram above, will be an important fact later on.

The functor T0 gives the kernel of a distance function, namely the relation consisting of pairs which are at distance 0. A common desideratum of pseudometric liftings or more generally BVal liftings is that the kernel of the $\hat{F}$-coinductive invariant function in BVal is bisimilarity in ERel (i.e. the Rel(F)-coinductive invariant where Rel(F) is the canonical relation lifting of F, defined in Section 3.1). We show how to establish this result for the Hausdorff metric in a highly reusable manner.

## 5.2 $T\epsilon$ is a Endolifting Morphism between Kripke Polynomial Functors

Next, we show that $T\epsilon$ is a endolifting morphism from every polynomial functor in BVal to the polynomial functor of parallel shape in ERel. This result is the backbone

<footnote n="9">⁹ Morphisms in each of these categories are Set-functions which satisfy conditions regarding the extra data in the total category. (That is, functions which preserve the source relation, shrink the source distance, etc.) It is straightforward to show $f: X \to Y$ is a morphism in A implies $f: FX \to FY$ is a morphism in B by writing down the extra conditions on f imposed by A and B where $F: A \to B$ is any of the four functors defined above.</footnote>
of our proof that $T \in \mathcal{T}$ is a endolifting morphism from the Hausdorff lifting of the finite
powerset functor to the canonical relation lifting of the finite powerset functor.

**Proposition 17.** For all $\epsilon \in [0, \infty)$, $T \in \mathcal{T}$ is a endolifting morphism:

1. from $\mathrm{Id}_{\mathbf{BVal}}$ to $\mathrm{Id}_{\mathbf{ERel}}$.

2. from $\hat{C}_A$ to $\bar{C}_A$ where $C_A$ is the constant-to-A functor, and

3. from $\hat{F}_1 \times \hat{F}_2$ to $\mathrm{Rel}(F_1) \bar{\times} \mathrm{Rel}(F_2)$, given that it is a morphism from $\hat{F}_i$ to $\mathrm{Rel}(F_i)$, and

4. from $\bigsqcup_i \hat{F}_i$ to $\bigsqcup_i \mathrm{Rel}(F_i)$, given that it is a morphism from $\hat{F}_i$ to $\mathrm{Rel}(F_i)$

Therefore, $T \in \mathcal{T}$ is a endolifting morphism from any polynomial functor in $\mathbf{ERel}$ to the polynomial functor of the same shape in $\mathbf{BVal}$.

This establishes $T \in \mathcal{T}$ as a endolifting morphism between polynomial functors, but we also want it to be a endolifting morphism from the Hausdorff lifting of $P_{\text{fin}}$ to the canonical relation lifting in $\mathbf{BVal}$. That is, we want to show $T \in \mathcal{H} \to \mathrm{Rel}(P_{\text{fin}})$ is a endolifting morphism. A reasonable strategy, given the proof we just completed, would be to hope that if $T \in \mathcal{T}$ is a endolifting morphism between two liftings of a functor, then it is a morphism between the pushforward of those functors along a natural transformation in the base category. In general this is not true, but liftings satisfying a simple side condition do have this property.

**Proposition 18.** Suppose $\tau: P \to F$ is a natural transformation in Set, $T \in \mathcal{T}: \hat{P} \to \bar{P}$ (Section 5.1) is a endolifting morphism from a BVal lift of P to an ERel lift of P, and $\hat{F}$ and $\bar{F}$ are the pushforwards of $\hat{P}$ and $\bar{P}$ along $\tau$. Further suppose for every set $I$, every $f, f' \in FI$ and $r: I \times I \to \mathbb{R}^+$, the lower bound for $\{\hat{P}r(p, p') : \tau p = f \text{ and } \tau p' = f'\}$ is achieved in this set. Then $T \in \mathcal{T}$ is a endolifting morphism from $\hat{F}$ to $\bar{F}$.

We can now apply this proposition to obtain the following corollary.

**Corollary 19.** $T \in \mathcal{T}$ is a endolifting morphism from $\mathcal{H}$ to $\mathrm{Rel}(P_{\text{fin}})$.

*Proof.* Proposition 17 shows $T \in \mathcal{T}$ is a endolifting morphism from the standard **BVal** lifting for the list functor to the standard **ERel** lifting for the list functor. We know $\mathcal{H}$ and $\mathrm{Rel}(P_{\text{fin}})$ are the pushforwards of these list functors along $\mathrm{set}_X$ in their respective total categories.<fnref n="10" /> Hence to apply Proposition 18 we only need to show for all finite sets $J, K \subseteq I$, and all distances $r: I \times I \to \mathbb{R}^+$, there exist lists $k^\dagger$ and $\ell^\dagger$ such that $\mathrm{set}(k^\dagger) = J$, $\mathrm{set}(\ell^\dagger) = K$ and $r^*(k^\dagger, \ell^\dagger) = \inf_{\substack{\mathrm{set}(k)=J \\ \mathrm{set}(\ell)=K}} r^*(k, \ell)$. We noted this in the Hausdorff distance section, where these dagger lists represent Gerry's optimal strategy.

**5.3 Approximate Bisimulations: an Example from Control Theory**

Here we present an example from a rather different context: *approximate bisimulation* by Girard and Pappas [8]. Defined as a binary relation on a metric space that is subject to the “mimicking” condition, the notion is widely used in control theory as a quantitative

<footnote n="10">¹⁰ Recall $\mathrm{set}_X$ from Example 6.</footnote>
relaxation of usual (Milner-Park) bisimulation that allows bounded errors. Its principal use is in bounding errors caused by some abstraction of dynamical systems: given the original dynamics $S$, one derives its abstraction $\mathcal{A}$; by exhibiting an $\epsilon$-approximate bisimulation between $S$ and $\mathcal{A}$, one then shows that the difference between the trajectory of $\mathcal{A}$ and that of $S$ is bounded by $\epsilon$. Such abstraction methods include: state space discretization (e.g. in [10]) and ignoring switching delays [18]. See [9] for an overview.

In the above scenario, an $\epsilon$-approximate bisimulation between $S$ and $\mathcal{A}$ is synthesized through analysis of the continuous dynamics of $S$: for example the incremental stability of $S$ yields an approximate bisimulation via its Lyapunov-type witness. Another common strategy for finding an approximate bisimulation is via a bisimulation function. Our goal here is to describe the latter strategy in the current coalgebraic and fibrational framework.

We fix the set $O$ of output values together with a distance function $d: O \times O \to \mathbb{R}^+$, and a $U$-labelled finitely branching LTS $(Q, \delta: Q \to U \hat{\cap} P_{fin}Q)$ with an output function $o: Q \to O$, where $\hat{\cap}$ denotes the power operation [19, p. 70]. An $\epsilon$-approximate bisimulation relation is a binary relation $R \subseteq Q \times Q$ such that

$$ \begin{array}{l} \forall (q, q') \in R . d(o(q), o(q')) \le \epsilon \land \forall l \in U . \\ \quad (\forall r \in Q . r \in \delta(l, q) \implies \exists r' \in Q . r' \in \delta(l, q') \land (r, r') \in R) \land \\ \quad (\forall r' \in Q . r' \in \delta(l, q') \implies \exists r \in Q . r \in \delta(l, q) \land (r, r') \in R). \end{array} \quad (4) $$

The difference from the usual Milner-Park bisimulation is that $R$ is additionally required to witness the $\epsilon$-proximity of outputs of related states $q$ and $q'$.

A bisimulation function is a quantitative (real-valued) witness for an approximate bisimulation. In many settings in control theory where dynamics are smooth and described by ordinary differential equations, such real-valued functions are easier to come up with than an approximate bisimulation itself. For the above LTS, a function $v: Q \times Q \to \mathbb{R}^+$ is a bisimulation function if it satisfies, for each $q, q' \in Q$,

$$ \max(d(o(q), o(q')), \sup_{l \in U} \mathcal{H}v(\delta(l, q), \delta(l, q'))) \le v(q, q') \quad (5) $$

A crucial fact is that a bisimulation function $v$ gives rise to an $\epsilon$-approximate bisimulation $\{(q, q') | v(q, q') \le \epsilon\}$. See e.g. [9].

We move on to give a categorical account of this construction. We use the following functor as a coalgebra signature:

$$ F: \mathbf{Set} \to \mathbf{Set}, \quad FX = O \times (U \hat{\cap} P_{fin}X), $$

We can then package a $U$-labelled finitely branching LTS and an output function into a single $F$-coalgebra $Q = (Q, \langle o, \delta \rangle: Q \to FQ)$.

Firstly, the endolifting that captures $\epsilon$-approximate bisimulations consists of

$$ r: \mathbf{ERel} \to \mathbf{Set}, \quad \tilde{F}_{\epsilon}X = T\epsilon(O, d) \times (U \hat{\cap} \mathrm{Rel}(P_{fin})(X)). $$

Secondly, the endolifting that captures bisimulation functions consists of

$$ p: \mathbf{BVal} \to \mathbf{Set}, \quad \hat{F}X = (O, d) \times (U \hat{\cap} \mathcal{HX}). $$
Indeed, by unfolding the definitions the following can be observed: $\tilde{F}_{\epsilon}$-invariants on $Q$ are nothing but $\epsilon$-approximate bisimulations; and $\hat{F}$-invariants on $Q$ are bisimulation functions. Thanks to Proposition 17 and Corollary 19, the functor $T\epsilon$—that sends a function $v : Q \times Q \to \mathbb{R}^+$ to the relation $\{(q, q') | v(q, q') \le \epsilon\}$—is a endolifting morphism from $\hat{F}$ to $\tilde{F}$. Therefore $T\epsilon$ transfers a $\hat{F}$-invariant $v$ on $Q$ to a $\tilde{F}_{\epsilon}$-invariant $T\epsilon v$ on $Q$, that is, a bisimulation function to an $\epsilon$-approximate bisimulation.

## 5.4 Endolifting Morphisms Preserve Final Coalgebras

We next state a result which we can use to ensure that the coinductive invariant in the source of an endolifting morphism is sent to the coinductive invariant in the target of that morphism.

**Lemma 20.** Suppose $H$ is a endolifting morphism from $(\pi : \mathbb{E} \to \mathbf{Set}, \hat{F})$ to $(\rho : \mathbb{F} \to \mathbf{Set}, \ddot{F})$ which is also a fibration map. Suppose additionally that $H$ preserves fibred meets. Then $H(I, v\hat{F}_{(I,f)}) = (I, v\ddot{F}_{(I,f)})$.

*Proof.* Preservation of top elements ensures $H \upharpoonright_{\mathbb{E}_I} = \upharpoonright_{\mathbb{F}_I}$. Since $H$ is a fibration map and a endolifting morphism, we get $H(f^*\hat{F}(A_I)) = f^*\ddot{F}(H(A_I))$ for all $A_I \in \mathbb{E}_I$. Combining this with the above observation ensures $H$ sends the final sequence in the fiber $\mathbb{E}_I$ to the final sequence in the fiber $\mathbb{F}_I$. Finally, $H$ preserving meets ensures $H$ will send the $\hat{F}$-coinductive invariant for $(I, f)$ to the $\ddot{F}$-coinductive invariant for $(I, f)$.

Note $T\epsilon$ satisfies most of the conditions in this lemma. Since we are interested in concluding something about the kernel of a behavioural metric, we specialize to the case where $\epsilon = 0$ where these conditions are all satisfied.

**Corollary 21.** If $T0$ is a endolifting morphism from $(\hat{F}, \mathbf{BVal})$ to $(\ddot{F}, \mathbf{ERel})$, then the behavioural metric induced by $\hat{F}$ has the coalgebraic predicate induced by $\ddot{F}$ at its kernel.

*Proof.* $T\epsilon$ is a fibration map and a right adjoint, and thus preserves all fibred meets.

All our work from the previous section establishing that $T\epsilon$ is a endolifting morphism from $\mathcal{H}$ to $\mathrm{Rel}(P_{\mathrm{fin}})$ now pays off.

**Corollary 22.** The Hausdorff behavioural metric on $P_{\mathrm{fin}}\mathcal{X}$ has $P_{\mathrm{fin}}$-bisimilarity at its kernel.

Above, we also showed $T0$ is a endolifting morphism between many other **BVal** and **ERel** liftings (Proposition 17). Therefore, we could also derive an analog of Corollary 21 for these pairs and conclude behavioural metrics of the **BVal** lift have bisimilarity (the coalgebraic relation of the corresponding **ERel** lift) at their kernels.
# 6 Conclusions and Future Work

We presented a fibrational framework for various extensions of (bi)simulation notions. On the categorical side our focus has been on structural aspects of fibrations such as fibration morphisms and lifting by Kan extensions; on the application side we took examples from quantitative reasoning about systems. This has allowed us to capture known constructions in more abstract and general terms, such as the Hausdorff pseudo-metric and approximate bisimulation in control theory.

As future work, we shall investigate conditions under which the two liftings in Section 4—one by left Kan extension and the other involving right Kan extension—coincide. We would then compare this coincidence and the Kantorovich-Wasserstein duality, which is the coincidence of the metric on probability distributions computed by sup and inf. We mentioned that **Top** and **Meas** are examples of $CLat_\lambda$-fibrations; their use in reasoning about systems will also be explored.

# Acknowledgement

This research was supported by ERATO HASUO Metamathematics for Systems Design Project (No. JPMJER1603), JST. The authors are grateful to anonymous reviewers, whose constructive comments helped to improve the paper.

# References

1. Azevedo de Amorim, A., Gaboardi, M., Hsu, J., Katsumata, S.y., Cherigui, I.: A semantic account of metric preservation. In: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2017). pp. 545–556 (2017). https://doi.org/10.1145/3009837.3009890, http://doi.acm.org/10.1145/3009837.3009890

2. Balan, A., Kurz, A., Velebil, J.: Extensions of Functors From Set to V-cat. In: Proceedings of the 6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015). pp. 17–34 (2015). https://doi.org/10.4230/LIPIcs.CALCO.2015.17, https://doi.org/10.4230/LIPIcs.CALCO.2015.17

3. Baldan, P., Bonchi, F., Kerstan, H., König, B.: Behavioral Metrics via Function Lifting. In: Proceedings of the 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014). pp. 403–415 (2014). https://doi.org/10.4230/LIPIcs.FSTTCS.2014.403, https://doi.org/10.4230/LIPIcs.FSTTCS.2014.403

4. Borceux, F.: Handbook of Categorical Algebra 2, Encyclopedia of Mathematics and Its Applications, vol. 51. Cambridge University Press (1994)

5. van Breugel, F., Worrell, J.: A behavioural pseudometric for probabilistic transition systems. Theoretical Computer Science 331(1), 115–142 (2005)

6. Chatzikokolakis, K., Gebler, D., Palamidessi, C., Xu, L.: Generalized Bisimulation Metrics. In: Proceedings of the 25th International Conference on Concurrency Theory (CONCUR 2014). pp. 32–46 (2014)

7. Desharnais, J., Jagadeesan, R., Gupta, V., Panangaden, P.: The Metric Analogue of Weak Bisimulation for Probabilistic Processes. In: Proceedings of the 17th IEEE Symposium on Logic in Computer Science (LICS 2002). pp. 413–422 (2002)
8. Girard, A., Pappas, G.J.: Approximation Metrics for Discrete and Continuous Systems. IEEE Transactions on Automatic Control **52**(5), 782–798 (2007). https://doi.org/10.1109/TAC.2007.895849

9. Girard, A., Pappas, G.J.: Approximate Bisimulation: A Bridge Between Computer Science and Control Theory. European Journal of Control **17**(5-6), 568–578 (2011). https://doi.org/10.3166/ejcc.17.568-578

10. Girard, A., Pola, G., Tabuada, P.: Approximately Bisimilar Symbolic Models for Incrementally Stable Switched Systems. IEEE Transactions on Automatic Control **55**(1), 116–126 (2010)

11. Hasuo, I., Cho, K., Kataoka, T., Jacobs, B.: Coinductive Predicates and Final Sequences in a Fibration. Electronic Notes in Theoretical Computer Science **298**, 197–214 (2013). https://doi.org/10.1016/j.entcs.2013.09.014, https://doi.org/10.1016/j.entcs.2013.09.014

12. Hermida, C., Jacobs, B.: Structural Induction and Coinduction in a Fi-
brational Setting. Information and Computation **145**(2), 107–152 (1998).
https://doi.org/https://doi.org/10.1006/inco.1998.2725

13. Herrlich, H.: Topological functors. General Topology and its Applications **4**(2), 125–142 (1974). https://doi.org/https://doi.org/10.1016/0016-660X(74)90016-6, http://www.sciencedirect.com/science/article/pii/0016660X74900166

14. Jacobs, B.: Categorical Logic and Type Theory, Studies in Logic and the Foundations of Mathematics, vol. 141. Elsevier Science (1999)

15. Katsumata, S., Sato, T.: Codensity Liftings of Monads. In: Proceedings of the 6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015). pp. 156–170 (2015). https://doi.org/10.4230/LIPIcs.CALCO.2015.156, https://doi.org/10.4230/LIPIcs.CALCO.2015.156

16. Kelly, G.M.: Basic Concepts of Enriched Category Theory, Lecture Notes in Mathematics, vol. 64. Cambridge University Press (1982)

17. Kelly, G.M., Rossi, F.: Topological categories with many symmetric monoidal closed structures. Bulletin of the Australian Mathematical Society **31**(1), 41–59 (1985). https://doi.org/10.1017/S0004972700002264

18. Kido, K., Sedwards, S., Hasuo, I.: Bounding Errors Due to Switching Delays in Incrementally Stable Switched Systems (Extended Version). arXiv:1712.06311 (2017), http://arxiv.org/abs/1712.06311

19. Lane, S.M.: Categories for the Working Mathematician, Graduate Texts in Mathematics, vol. 5. Springer (1998)

20. Rutten, J.: Universal coalgebra: a theory of systems. Theoretical Computer Science **249**(1), 3–80 (2000). https://doi.org/10.1016/S0304-3975(00)00056-6

21. Činčura, J.: Tensor products in the category of topological spaces. Commentationes Mathematicae Universitatis Carolinae **20**(3), 431–446 (1979)