# Injective Objects and Fibered Codensity Liftings

Yuichi Komorida

► To cite this version:

Yuichi Komorida. Injective Objects and Fibered Codensity Liftings. 15th International Workshop on Coalgebraic Methods in Computer Science (CMCS), Apr 2020, Dublin, Ireland. pp.112-132, 10.1007/978-3-030-57201-3_7. hal-03232347

HAL Id: hal-03232347

https://inria.hal.science/hal-03232347

Submitted on 21 May 2021

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
# Injective Objects and Fibered Codensity Liftings*

Yuichi Komorida¹,²

¹ The Graduate University for Advanced Studies, SOKENDAI, Tokyo, Japan

² National Institute of Informatics, Tokyo, Japan, komorin@nii.ac.jp

**Abstract.** Functor lifting along a fibration is used for several different purposes in computer science. In the theory of coalgebras, it is used to define coinductive predicates, such as simulation preorder and bisimilarity. Codensity lifting is a scheme to obtain a functor lifting along a fibration. It generalizes a few previous lifting schemes including the Kantorovich lifting. In this paper, we seek a property of functor lifting called fiberedness. Hinted by a known result for Kantorovich lifting, we identify a sufficient condition for a codensity lifting to be fibered. We see that this condition applies to many examples that have been studied. As an application, we derive some results on bisimilarity-like notions.

# 1 Introduction

In this paper, we focus on a category-theoretical gadget, called *functor lifting*, and seek a property thereof, called *fiberedness*. As is often the case with such mathematical topics, functor lifting comes up in several different places in computer science under various disguises (as mentioned in Section 1.6). Here we see one of such places, *bisimilarity and its generalizations on coalgebras*, before we formally introduce functor lifting.

## 1.1 Coalgebras and Bisimilarity

Computer programs work as we write them, not necessarily as we expect. One approach to overcome this gap is to *verify* the systems so that we can make sure that they meet our requirements. Abstract mathematical methods are often useful for the purpose, but before that, we have to *model* the target system by some mathematical structure.

*Coalgebra* [27] is one of such mathematical structure with a broad scope of application. It is defined in terms of the theory of *categories and functors*. Given a category $C$ and an endofunctor $F: C \to C$, an $F$-coalgebra is defined as an arrow $c: X \to FX$. This simple definition includes many kinds of state-transition systems as special cases, e.g., Kripke frame (and model), Markov chain (and process), and (deterministic and non-deterministic) automata.

<footnote>* The author was supported by ERATO HASUO Metamathematics for Systems Design Project (No. JPMJER1603), JST.</footnote>
Having modeled a system as a coalgebra, we can ask a fundamental question: which states behave the same? Bisimilarity [25,26] is one of the notions to define such equivalence. (For an introduction, see, e.g., [28].) We sketch the idea in the case where $C = \mathbf{Set}$ and $F = \Sigma \times (-)$. In this case, $F$-coalgebras are deterministic LTSs. Consider a coalgebra $c: X \to \Sigma \times X$ and define $l: X \to \Sigma$ and $n: X \to X$ by $(l(x), n(x)) = c(x)$. The point here is the following observation: if $x, y \in X$ behave the same, then $l(x) = l(y)$ must hold, and $n(x)$ and $n(y)$ must behave the same. This is almost the definition of bisimilarity: the bisimilarity relation is the greatest binary relation $\sim \subseteq X \times X$ that satisfies

$$x \sim y \implies l(x) = l(y) \land n(x) \sim n(y).$$

For other functors $F$, the idea is roughly the same: in a coalgebra $c: X \to FX$, for $x, y \in X$ to behave the same, $c(x)$ and $c(y)$ must behave the same. To define bisimilarity precisely, however, we have to turn a relation $R \subseteq X \times X$ into $R' \subseteq FX \times FX$.

## 1.2 Qualitative and Quantitative Bisimilarity from Functor Lifting

An elegant way to formulate this is the following: bundle binary relations on all sets into one *fibration* and use *functor lifting* as in [11]. We give ideas on them here. The precise definitions are in Section 2.

First, we gather all pairs $(X, R)$ of a set $X$ and a binary relation $R \subseteq X \times X$ into one category $\mathbf{ERel}$ (Example 8). It comes with a forgetful functor $U: \mathbf{ERel} \to \mathbf{Set}$. (This is a *fibration*.) Any binary relation $R$ on $X$ is sent to $X$ by $U$; placing the things vertically, $R$ is “above” $X$. Now let us assume that there exists a functor $\dot{F}: \mathbf{ERel} \to \mathbf{ERel}$ satisfying $U \circ \dot{F} = F \circ U$. This means that any binary relation $R$ on $X$ is sent to one on $FX$:

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

(This means that the functor $\dot{F}$ is a *lifting* of $F$ along $U$.) The functor $U: \mathbf{ERel} \to \mathbf{Set}$ has an important structure: for any $f: Y \to X$ and a relation $R$ on $X$, we can obtain a relation $f^*R$ on $Y$ in a canonical way:

$$f^*R = \{(y, y') \in Y \times Y | (f(y), f(y')) \in R\}.$$

(This is called *reindexing* or *pullback*.) By using these, we can define the bisim- ulation relation on $c: X \to FX$ as the greatest fixed point of $f^* \circ \dot{F}$.

An advantage of this approach is that we can readily generalize this to other “bisimilarity-like” notions. For example, by changing the fibration to $\mathbf{PMet}_\top \to \mathbf{Set}$ (Example 7), one can define a *behavioral (pseudo)metric* [2].
## 1.3 Codensity Lifting of Endofunctors

Now we know that a functor lifting induces a bisimilarity-like notion. Then, how can we obtain a functor lifting? *Codensity Lifting* is a scheme to obtain such liftings. It is first introduced by Katsumata and Sato [16] for monads using *codensity monad* construction [22]. It is later extended to general endofunctors by Sprunger et al. [31]. It is parametrized in a set of data called a *lifting parameter*. By changing lifting parameters, a broad class of functor liftings can be represented as codensity liftings, as is shown, e.g., in Komorida et al. [18].

As mentioned in the last section, we can define a bisimilarity-like notion using codensity lifting. It is called *codensity bisimilarity* in [18, Sections III and VI].

## 1.4 Fiberedness of Lifting

In some situations, we have to assume that $\dot{F}: \mathbb{E} \to \mathbb{E}$ interacts well with the pullback operation between the fibers. In such a situation, $\dot{F}$ is required to be *fibered* (Definition 11). It means that pullbacks and $\dot{F}$ are “commutative,” in the sense that they satisfy $\dot{F}(f^*P) = (Ff)^*(\dot{F}P)$.

Some of the existing works indeed require fiberedness. For example, Hasuo et al. [9, Definition 2.2] include fiberedness in their definition of predicate lifting. Fiberedness also plays a notable role in [3], where it is rephrased to isometry-preservation. However, there has been no systematic result on fiberedness of codensity lifting.

## 1.5 Contributions

In the current paper, hinted by a result of Baldan et al. [3], we show a sufficient condition on the lifting parameter guaranteeing the resulting functor to be fibered (Theorem 20). The scope of our fiberedness result is so broad that it covers, e.g., most of the examples presented in [18] (Section 5).

The condition involves a variation of the notion of injective object, which we call *c-injective object* (Definition 15). To our knowledge, such a notion connecting injective objects and fibrations is new. We study some basic properties of them.

Using the fiberedness result, we show a property of codensity bisimilarity which we call *stability under coalgebra morphisms* (Proposition 49). As a corollary, we see that, when there is a final coalgebra, the codensity bisimilarity on any coalgebra is determined by that on the final coalgebra. Note that this kind of property is well-known for a conventional bisimilarity relation (Corollary 50).

To summarize, our technical contributions are as follows:

- We define *c-injective objects* for fibrations (Definition 15) and show some properties of them.

- We show a sufficient condition on the lifting parameter to guarantee fiberedness of codensity lifting (Theorem 20 and Corollary 24).

- We show a number of examples (Section 5) to which the condition above is applicable.
- As an application, we show that codensity bisimilarity is stable under coalgebra morphisms (Proposition 49) in many cases, including a new one (Example 51).

## 1.6 Related Work

Even though we focused on bisimilarity and coalgebra above, functor lifting comes up in computer science here and there. To name a few, it has applications in logical predicates [11,15], quantitative bisimulation [3], and differential privacy [29].

As mentioned above, there have been many methods to obtain liftings of functors. *Kantorovich lifting* [2,19] and *generalized Kantorovich metric* [5] are both special cases of the version of codensity lifting considered here. *Categorical ⊤⊤-lifting* [15] is the precursor of the original version of codensity lifting, but it is not a special case of codensity lifting. For categorical ⊤⊤-lifting, one uses internal Hom-objects rather than Hom-sets like codensity lifting. Obtaining a sufficient condition for fiberedness of categorical ⊤⊤-lifting is future work. *Wasserstein lifting* [2] is another method that is somehow dual to Kantorovich lifting. They have shown that any lifting obtained by this scheme is fibered. Klin [17] goes a different way: rather than showing fiberedness, they incorporate fiberedness in the definition. They study *the least fibered lifting* along **EqRel** → **Set** and show that, in good situations, it coincides with the *canonical relation lifting*.

The notion of *injective object* is first introduced in homological algebra as *injective modules* [1]. There are also some works about injective objects outside homological algebra: Scott [30] and Banaschewski and Bruns [4] have identified the injective objects in **Top**₀ and **Pos**, respectively. We use their results in Section 4 (where the categories mentioned are defined). Injective objects w.r.t. isometric embeddings in the category of metric spaces are also well-studied and called *hyperconvex spaces* [7]. Finding a precise connection between them and c-injective objects in **PMet**⊤ → **Set** (Example 7) is future work. Recently, in his preprint [8], Fujii has extended the above result in **Pos** and characterized injective objects in the category of *Q*-categories with respect to the class of fully faithful *Q*-functors, for any quantale *Q*.

## 1.7 Organization

In Section 2, we review **CLat**ₜ-fibrations and functor liftings. In Section 3, we review the definition of codensity lifting and introduce the notion of *c-injective objects*. We show a sufficient condition for a codensity lifting to be fibered. In Section 4, we show some general results on c-injective objects. In Section 5, we list several examples of fibered codensity liftings using the results in Section 4. In Section 6, we apply the fiberedness result to codensity bisimilarity. In Section 7, we conclude with some remarks and future work.
## 2 Preliminaries

We assume some knowledge of category theory, but the full content of the standard reference [24] is not needed. The basic definitions and theorems, e.g., those in Leinster [23], is enough. Even though we have explained our motivation through coalgebra, no knowledge of coalgebra is needed for the main result in Section 3.

In the following, **Set** means the category of sets and (set-theoretic) functions.

### 2.1 CLat$_{⊓}$-Fibrations

Here we introduce CLat$_{⊓}$-fibrations, as defined in [18]. We use them to model various “notions of indistinguishability” like preorder, equivalence relation, and pseudometric. Assuming full knowledge of the theory of fibrations, we could define them as poset fibrations with fibered small meets. Instead, we give an explicit definition below. This is mainly because we need the notion of *Cartesian arrow*. For a comprehensive account of the theory of fibrations, the reader can consult, e.g., a book by Jacobs [13] or Hermida’s thesis [10], but in the following, we do not assume any knowledge of fibrations.

We first define a fiber of a functor over an object. Basically, this is only considered in the case where the functor is a fibration.

**Definition 1 (fiber).** Let $p: \mathbb{E} \to \mathbb{C}$ be a functor and $X \in \mathbb{C}$ be an object. The fiber over $X$ is the subcategory of $\mathbb{E}$

- whose objects are $P \in \mathbb{E}$ such that $pP = X$ and

- whose arrows are $f: P \to Q$ such that $pf = \text{id}_X$.

We denote it by $\mathbb{E}_X$.

Note that, if $p$ is faithful, then each fiber is a thin category, i.e., a preorder. The following definition of poset fibration is a special case of that in [13].

**Definition 2 (cartesian arrow and poset fibration).** Let $p: \mathbb{E} \to \mathbb{C}$ be a faithful functor.

An arrow $f: P \to Q$ in $\mathbb{E}$ is *Cartesian* if the following condition is satisfied:

- For each $R \in \mathbb{E}$ and $g: R \to Q$, there exists $h: R \to P$ such that $g = f \circ h$ if and only if there exists $h': pR \to pP$ such that $pg = pf \circ h'$.

The functor $p$ is called a *poset fibration* if the following are satisfied:

- For each $X \in \mathbb{C}$, the fiber $\mathbb{E}_X$ is a poset. The order is denoted by $\sqsubseteq$. We define the direction so that $P \sqsubseteq Q$ holds if and only if there is an arrow $P \to Q$ in $\mathbb{E}_X$.

- For each $Q \in \mathbb{E}$ and $f: X \to pQ$, there exists an object $f^*Q \in \mathbb{E}_X$ and a Cartesian arrow $\dot{f}: f^*Q \to Q$ such that $p\dot{f} = f$. (Such $f^*Q$ and $\dot{f}$ are necessarily unique.)
The map $Q \mapsto f^*Q$ turns out to be a monotone map from $\mathbb{E}_Y$ to $\mathbb{E}_X$. We call it the pullback functor and denote it by $f^*: \mathbb{E}_Y \to \mathbb{E}_X$.

Intuitively, pullback functors model substitutions. Indeed, in many examples, they are just “assigning $f(x)$ to $y$”, as can be seen below.

**Example 3 (pseudometric).** Let $\top$ be a positive real number or $+\infty$. Define a category $\mathbf{PMet}_\top$ as follows:

- Each object is a pair $(X, d)$ of a set $X$ and a $[0, \top]$-valued pseudometric $d: X \times X \to [0, \top]$. (A pseudometric is a metric without the condition $d(x, y) = 0 \implies x = y$.)

- Each arrow from $(X, d_X)$ to $(Y, d_Y)$ is a nonexpansive map $f: X \to Y$. ($f$ is nonexpansive if, for all $x$ and $x' \in X$, $d_X(x, x') \ge d_Y(f(x), f(x'))$.)

The obvious forgetful functor $\mathbf{PMet}_\top \to \mathbf{Set}$ is a poset fibration. For each $X \in \mathbf{Set}$, the objects of the fiber $(\mathbf{PMet}_\top)_X$ are the pseudometrics on $X$. However, the order is reversed: in our notation, the order is defined by

$$ (X, d_1) \sqsubseteq (X, d_2) \Leftrightarrow \forall x, x' \in X, d_1(x, x') \ge d_2(x, x'). $$

An arrow $f: (X, d_X) \to (Y, d_Y)$ is Cartesian if and only if it is an isometry, i.e., $d_X(x, x') = d_Y(f(x), f(x'))$ holds for all $x, x'$. For $(Y, d_Y) \in \mathbf{PMet}_\top$ and $f: X \to Y$, the pullback $f^*(Y, d_Y)$ is the set $X$ with the pseudometric $(x, x') \mapsto d_Y(f(x), f(x'))$.

We list a few properties of pullback functors that we use:

**Proposition 4.** Let $p: \mathbb{E} \to \mathbb{C}$ be a poset fibration, $f: X \to Y$ be an arrow in $\mathbb{C}$ and $P \in \mathbb{E}_X$ and $Q \in \mathbb{E}_Y$ be objects in $\mathbb{E}$. There exists an arrow $g: P \to Q$ such that $pg = f$ if and only if $P \sqsubseteq f^*Q$. Moreover, such $g$ is Cartesian if and only if $P = f^*Q$. $\square$

**Proposition 5.** Let $p: \mathbb{E} \to \mathbb{C}$ be a poset fibration.

- For each $X \in \mathbb{C}$, $(\mathrm{id}_X)^*: \mathbb{E}_X \to \mathbb{E}_X$ is the identity functor.

- For each composable pair of arrows $X \xrightarrow{f} Y \xrightarrow{g} Z$ in $\mathbb{C}$, $(g \circ f)^* = f^* \circ g^*$ holds. $\square$

Now we define the class that we are concerned about, $\mathbf{CLat}_\sqcap$-fibrations.

**Definition 6 (CLat_\sqcap-fibration).** A poset fibration $p: \mathbb{E} \to \mathbb{C}$ is a $\mathbf{CLat}_\sqcap$-fibration if the following conditions are satisfied:

- Each fiber $\mathbb{E}_X$ is small and has small meets, which we denote by $\sqcap$.

- Each pullback functor $f^*$ preserves small meets.

Note that, in the situation above, each fiber $\mathbb{E}_X$ is a complete lattice: the small joins can be constructed using small meets.
*Example 7 (pseudometric).* The poset fibration $\mathbf{PMet}_\top \to \mathbf{Set}$ in *Example 3* is a $\mathbf{CLat}_\sqcap$-fibration. Indeed, meets can be defined by sups of pseudometrics: if we let $(X, d) = \bigsqcup_{a \in A}(X, d_a)$, then

$$d(x, x') = \sup_{a \in A} d_a(x, x')$$

holds.

*Example 8 (binary relations).* Define a category $\mathbf{ERel}$ of sets with an endorelation as follows:

- Each object is a pair $(X, R)$ of a set $X$ and a binary relation $R \subseteq X \times X$.

- Each arrow from $(X, R_X)$ to $(Y, R_Y)$ is a map $f: X \to Y$ preserving the relations; that is, we require $f$ to satisfy $(x, x') \in R_X \implies (f(x), f(x')) \in R_Y$.

The obvious forgetful functor $\mathbf{ERel} \to \mathbf{Set}$ is a $\mathbf{CLat}_\sqcap$-fibration. For each $X \in \mathbf{Set}$, the fiber $\mathbf{ERel}_X$ is the complete lattice of subsets of $X \times X$.

An arrow $f: (X, R_X) \to (Y, R_Y)$ is Cartesian if and only if it reflects the relations, i.e., $(x, x') \in R_X \Leftrightarrow (f(x), f(x')) \in R_Y$ holds for all $x, x'$. For $(Y, R_Y) \in \mathbf{ERel}$ and $f: X \to Y$, the pullback $f^*(Y, R_Y)$ is the set $X$ with the relation $\{(x, x') \in X \times X | (f(x), f(x')) \in R_Y\}$.

Define the following full subcategories of $\mathbf{ERel}$:

- The category $\mathbf{Pre}$ of preordered sets and monotone maps.

- The category $\mathbf{EqRel}$ of sets with an equivalence relation and maps preserving them.

The forgetful functors $\mathbf{Pre} \to \mathbf{Set}$ and $\mathbf{EqRel} \to \mathbf{Set}$ are also $\mathbf{CLat}_\sqcap$-fibrations.

$\mathbf{CLat}_\sqcap$-fibrations are not necessarily “relation-like”. There also is an example with a much more “space-like” flavor.

*Example 9.* The forgetful functor $\mathbf{Top} \to \mathbf{Set}$ from the category $\mathbf{Top}$ of topological spaces and continuous maps is a $\mathbf{CLat}_\sqcap$-fibration.

## 2.2 Lifting and Fiberedness

Another pivotal notion in the current paper is *functor lifting*. In Section 1.2 we have seen that it is used to define bisimilarity, or more generally bisimilarity-like notions, as a way to turn a relation (or pseudometric, etc.) on $X$ into one on $FX$. Here we review the formal definition in a restricted form that only considers $\mathbf{CLat}_\sqcap$-fibration. (Note that, usually it is defined more generally, and there are indeed applications of such general definition.)

**Definition 10 (lifting of endofunctor).** Let $p: \mathbb{E} \to \mathbb{C}$ be a $\mathbf{CLat}_\sqcap$-fibration and $F: \mathbb{C} \to \mathbb{C}$ be a functor. A *lifting* of $F$ along $p$ is a functor $\tilde{F}: \mathbb{E} \to \mathbb{E}$ such that $p \circ \tilde{F} = F \circ p$ holds:

<figure><img src="image_3.png" /></figure>
We then define *fiberedness* of a lifting. This means that the lifting interacts well with the pullback structure of the fibration, but we first give a definition focusing on Cartesian arrows. Here we define it in a slightly more general way so that we can use them later (Section 4).

**Definition 11 (fibered functor [13, Definition 1.7.1]).** Let $p: \mathbb{E} \to \mathbb{C}$ and $q: \mathbb{F} \to \mathbb{D}$ be $\mathbf{CLat}_{\sqcap}$-fibrations. A *fibered functor* from $p$ to $q$ is a functor $\dot{F}: \mathbb{E} \to \mathbb{F}$ such that there is another functor $F: \mathbb{C} \to \mathbb{D}$ satisfying $q \circ \dot{F} = F \circ p$ and $\dot{F}$ sends each Cartesian arrow to a Cartesian arrow.

Note that, in the situation above, such $F$ is uniquely determined by $p$, $q$, and $\dot{F}$.

Now we see a characterization of fiberedness by means of pullback.

**Proposition 12.** Let $p: \mathbb{E} \to \mathbb{C}$ and $q: \mathbb{F} \to \mathbb{D}$ be $\mathbf{CLat}_{\sqcap}$-fibrations and $\dot{F}: \mathbb{E} \to \mathbb{F}$ and $F: \mathbb{C} \to \mathbb{D}$ be functors satisfying $q \circ \dot{F} = F \circ p$. $\dot{F}$ is a fibered functor if and only if, for any $f: X \to Y$ in $\mathbb{C}$ and $P \in \mathbb{E}_Y$, $\dot{F}(f^*P) = (Ff)^*(\dot{F}P)$ holds. $\square$

We use this in the proof of the main result.

# 3 C-injective Objects and Codensity Lifting

## 3.1 Codensity Lifting

Before we formulate our main result, we introduce *codensity lifting* of endofunctors [16,31]. Here we use an explicit definition for a narrower situation than the original one.

**Definition 13 (codensity lifting (as in [18]))**. Let

- $p: \mathbb{E} \to \mathbb{C}$ be a $\mathbf{CLat}_{\sqcap}$-fibration,

- $F: \mathbb{C} \to \mathbb{C}$ be a functor,

- $\Omega \in \mathbb{E}$ be an object above $\Omega \in \mathbb{C}$, and

- $\tau: F\Omega \to \Omega$ be an $F$-algebra.

Define a functor $F^{\Omega, \tau}: \mathbb{E} \to \mathbb{E}$, which is a lifting of $F$ along $p$, by

$$F^{\Omega, \tau} P = \bigcap_{f \in \mathbb{E}(P, \Omega)} (F(pf))^{\tau^* \Omega}$$

for each $P \in \mathbb{E}$. The functor $F^{\Omega, \tau}$ is called a *codensity lifting* of $F$. Note that, for each $P \in \mathbb{E}$ and $f: P \to \Omega$, the situation is as follows:

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

and we can indeed obtain the pullback $(F(pf))^{\tau^* \Omega}$.
We have given only the object part of $F^{\Omega, \tau}$ above, but the arrow part, if it is well-defined, should be determined uniquely since $p$ is faithful. We give a proof that it is indeed well-defined. For each $f: P \to Q$, we need another arrow $g: F^{\Omega, \tau}P \to F^{\Omega, \tau}Q$ such that $pg = F(pg)$. By Proposition 4, it suffices to show the following proposition:

**Proposition 14.** For any $f: P \to Q$, $F^{\Omega, \tau}P \subseteq (F(pg))^*(F^{\Omega, \tau}Q)$ holds.

*Proof.* By definition, the l.h.s. satisfies

$$F^{\Omega, \tau}P = \bigcap_{g \in \mathbb{E}(P, \Omega)} (F(pg))^* \tau^* \Omega.$$

On the other hand, the r.h.s. satisfies

$$ \begin{align*} (F(pg))^*(F^{\Omega, \tau}Q) &= (F(pg))^* \left( \bigcap_{h \in \mathbb{E}(Q, \Omega)} (F(ph))^* \tau^* \Omega \right) \\ &= \bigcap_{h \in \mathbb{E}(Q, \Omega)} (F(pg))^*(F(ph))^* \tau^* \Omega \\ &= \bigcap_{h \in \mathbb{E}(Q, \Omega)} (F(p(h \circ f)))^* \tau^* \Omega. \end{align*} $$

Here, since $\{g \in \mathbb{E}(P, \Omega)\} \supseteq \{h \circ f \mid h \in \mathbb{E}(Q, \Omega)\}$ holds, we have

$$\bigcap_{g \in \mathbb{E}(P, \Omega)} (F(pg))^* \tau^* \Omega \subseteq \bigcap_{h \in \mathbb{E}(Q, \Omega)} (F(p(h \circ f)))^* \tau^* \Omega.$$

This means $F^{\Omega, \tau}P \subseteq (F(pg))^*(F^{\Omega, \tau}Q)$. $\square$

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

## 3.2 C-injective Object

In the proof of the functoriality of $F^{\Omega, \tau}$, ultimately we use the fact that, for any $f: P \to Q$, any “test” $k: Q \to \Omega$ can be turned into another “test” $k \circ f: P \to \Omega$. On the other hand, when we try to prove fiberedness of $F^{\Omega, \tau}$, we have to somehow lift a “test” $g: P \to \Omega$ along a Cartesian arrow $f: P \to Q$ and obtain another “test” $h: Q \to \Omega$. This observation leads us to the following definition of c-injective object. (The letter c here comes from Cartesian.)

**Definition 15 (c-injective object).** Let $p: \mathbb{E} \to \mathbb{C}$ be a fibration. An object $\Omega \in \mathbb{E}$ is a c-injective object if the functor $\mathbb{E}(-, \Omega): \mathbb{E}^{\text{op}} \to \text{Set}$ sends every Cartesian arrow to a surjective map.

Equivalently, $\Omega \in \mathbb{E}$ is a c-injective object if, for any Cartesian arrow $f: P \to Q$ in $\mathbb{E}$ and any (not necessarily Cartesian) arrow $g: P \to \Omega$, there is a (not necessarily Cartesian) arrow $h: Q \to \Omega$ satisfying $g = h \circ f$.

Some basic objects can be shown to be c-injective objects.
Example 16 (the two-point set) . In the fibration EqRel → Set , (2 , =) is a c- injective object. Here, 2 = { ⊥ , ⊤ } is the two-point set and = means the equality relation. Indeed, for any Cartesian f : ( X, R$_{X}$ ) → ( Y, R$_{Y}$ ) and any g : ( X, R$_{X}$ ) → (2 , =), if we define h : ( Y, R$_{Y}$ ) → (2 , =) by

$$
h(y) = \begin{cases}
g(x) & \text{if } (y, f(x)) \in R_Y \\
\top & \text{otherwise,}
\end{cases}
$$

then this turns out to be well-defined and satisfies h ◦ f = g .

Example 17 (the two-point poset of truth values) . In the fibration Pre → Set , (2 , ≤ ) is a c-injective object. Here, ≤ is the unique partial order satisfying ⊥ ≤ ⊤ and ⊤ ≲ ⊥ . Indeed, for any Cartesian arrow f : ( X, R$_{X}$ ) → ( Y, R$_{Y}$ ) and any g : ( X, R$_{X}$ ) → (2 , ≤ ), if we define h : : ( Y, R$_{Y}$ ) → (2 , ≤ ) by

$$
h(y) = \begin{cases} \bot & \text{if } (y, f(x)) \in R_Y \text{ for some } x \text{ such that } g(x) = \bot \\ \top & \text{otherwise,} \end{cases}
$$

then this turns out to be well-defined and satisfies h ◦ f = g .

Example 18 (the unit interval as a pseudometric space [3, Theorem 5.8]) . In the fibration PMet$_{⊤}$ → Set , [0 , ⊤] is a c-injective object. Indeed, for any arrow g : ( X, d$_{X}$ ) → ([0 , ⊤] , d$_{e}$ ) and any Cartesian arrow f : ( X, d$_{X}$ ) → ( Y, d$_{Y}$ ), we can show that the map h : Y → [0 , ⊤] defined by h ( y ) = inf$_{x}$$_{∈}$$_{X}$ ( g ( x ) + d$_{Y}$ ( f ( x ) , y )) is nonexpansive from ( Y, d$_{Y}$ ) to ([0 , ⊤] , d$_{e}$ ).

The following non-example shows that c-injectivity crucially depends on the fibration we consider.

Example 19 (non-example) . In contrast to Example 17, in the fibration ERel → Set , (2 , ≤ ) is not c-injective, where 2 = { ⊥ , ⊤ } is the two-point set and ≤ is the unique partial order satisfying ⊥ ≤ ⊤ and ⊤ ≲ ⊥ .

This can be seen as follows. Let X = { a, b } , Y = { x, y, z } , R$_{X}$ =  , and R$_{Y}$ = { ( x, z ) , ( z, y ) } . Then ( X, R$_{X}$ ) and ( Y, R$_{Y}$ ) are objects of ERel . Consider the maps f : ( X, R$_{X}$ ) → ( Y, R$_{Y}$ ) and g : ( X, R$_{X}$ ) → (2 , ≤ ) defined by f ( a ) = x , f ( b ) = y , g ( a ) = ⊤ , and g ( b ) = ⊥ . Note that f is Cartesian. However, there is no h : ( Y, R$_{Y}$ ) → (2 , ≤ ) such that h ◦ f = g : such h would satisfy ⊤ = h ( f ( a )) = h ( x ) ≤ h ( z ) ≤ h ( y ) = h ( f ( b )) = ⊥ , which contradict ⊤ ≲ ⊥ .

The same example can also be used to show that, in contrast to Example 16, (2 , =) is not c-injective, where = means the equality relation.

3.3 Sufficient Condition for Fibered Codensity Lifting

Now we are prepared to state the following main theorem of the current paper. The strategy of the proof is roughly as mentioned earlier.

Theorem 20 (fiberedness from injective object) . In the setting of Defini- tion 13, if Ω is a c-injective object, then F $^{Ω}$,τ is fibered.
**Proof.** Let $f: P \to Q$ be any Cartesian arrow. By Proposition 12, it suffices to show $F^{\Omega, \tau}P = (F(pf))^* (F^{\Omega, \tau}Q)$. Here, $F^{\Omega, \tau}P \sqsubseteq (F(pf))^* (F^{\Omega, \tau}Q)$ has already been proven. Thus, our goal is the inequality $F^{\Omega, \tau}P \supseteq (F(pf))^* (F^{\Omega, \tau}Q)$. Here, since $\Omega$ is c-injective and $f$ is Cartesian, the following inclusion holds:

$$ \{g \in \mathbb{E}(P, \Omega)\} \subseteq \{h \circ f \mid h \in \mathbb{E}(Q, \Omega)\}. $$

By the definition of the meet, we have

$$ \bigcap_{g \in \mathbb{E}(P, \Omega)} (F(pg))^* \tau^* \Omega \supseteq \bigcap_{h \in \mathbb{E}(Q, \Omega)} (F(p(h \circ f)))^* \tau^* \Omega. $$

By the calculation in the proof of Proposition 14, this implies

$$ F^{\Omega, \tau} P \supseteq (F(pf))^* (F^{\Omega, \tau} Q). \quad \square $$

**Remark 21.** A refinement of Theorem 20 to an if-and-only-if result seems hard. At least there is a simple counterexample to the most naive version of it: Consider a $CLat_\sqcap$-fibration Id: $C \to C$, an endofunctor Id: $C \to C$, an object $C \in C$, and an arrow $\tau: C \to C$. The codensity lifting $Id^{C, \tau}$ is always equal to Id, which is fibered. However, since any arrow in $C$ is a Cartesian arrow w.r.t. Id, it is not hard to find an example of $C$ and $C$ such that $C$ is not c-injective w.r.t. Id.

**Example 22 (Kantorovich lifting).** Baldan et al. [3, Theorem 5.8] have shown that any Kantorovich lifting preserves isometries. In terms of fibrations, this means that such functor is a fibered endofunctor on the fibration $PMet_\top \to Set$.

Since Kantorovich lifting is a special case of codensity lifting where $\Omega = ([0, \top], d_\mathbb{R})$, Theorem 20 and Example 18 recover the same result. Actually, this has inspired Theorem 20 as a prototype.

The argument above also applies to situations with multiple parameters.

**Definition 23 (codensity lifting with multiple parameters (as in [18]))**. Let $\mathbb{E}, \mathbb{C}, p$, and $F$ be as in Definition 13. Let $A$ be a set. Assume that, for each $a \in A$, we are given $\Omega_a \in \mathbb{E}$ above $\Omega_a \in \mathbb{C}$ and $\tau_a: F\Omega_a \to \Omega_a$. Define a functor $F^{\Omega, \tau}: \mathbb{E} \to \mathbb{E}$ by

$$ F^{\Omega, \tau} P = \bigcap_{a \in A} F^{\Omega_a, \tau_a} P $$

for each $P \in \mathbb{E}$.

**Corollary 24.** In the setting of Definition 23, if, for each $a \in A$, $\Omega_a$ is a c-injective object, then $F^{\Omega, \tau}$ is fibered.

**Proof.** For any $P \in \mathbb{E}$ above $X \in \mathbb{C}$ and $f: Y \to X$ in $\mathbb{C}$, using Theorem 20, we can see

$$ \begin{align*} (Ff)^* F^{\Omega, \tau} P &= (Ff)^* \bigcap_{a \in A} F^{\Omega_a, \tau_a} P \\ &= \bigcap_{a \in A} (Ff)^* F^{\Omega_a, \tau_a} P \\ &= \bigcap_{a \in A} F^{\Omega_a, \tau_a} f^* P \\ &= F^{\Omega, \tau} f^* P. \quad \square \end{align*} $$
*Example 25 (Kantorovich lifting with multiple parameters).* In [19], König and Mika-Michalski introduced a generalized version of Kantorovich lifting.

Since it is a special case of Definition 23 where $p$ is the fibration $\mathbf{PMet}_{\top} \to \mathbf{Set}$ and $\Omega = ([0, \top], d_{\mathbb{R}})$, Corollary 24 and Example 18 imply that such lifting always preserves isometries.

# 4 Results on C-injective Objects

Here we seek properties of c-injective objects, mainly to obtain more examples of them. We also see that, in a few fibrations, c-injective objects have been essentially identified by previous works.

## 4.1 $\mathcal{M}$-injective Objects

To connect c-injectivity with existing works, we consider a more general notion of $\mathcal{M}$-injective object. The following definition is found e.g. in [14, Section 9.5].

**Definition 26.** Let $\mathbb{C}$ be a category and $\mathcal{M}$ be a class of arrows in $\mathbb{C}$. An object $X \in \mathbb{C}$ is an $\mathcal{M}$-injective object if the functor $\mathbb{C}(-, X): \mathbb{C}^{\text{op}} \to \mathbf{Set}$ sends every arrow in $\mathcal{M}$ to a surjective map.

The definition of c-injective objects is a special case of the definition above where $\mathcal{M}$ is the class of all Cartesian arrows.

The following is a folklore result. The dual is found e.g. in [12, Proposition 10.2].

**Proposition 27.** Let $\mathbb{C}, \mathbb{D}$ be categories, $\mathcal{M}_{\mathbb{C}}, \mathcal{M}_{\mathbb{D}}$ be classes of arrows, and $L \dashv R: \mathbb{C} \to \mathbb{D}$ be a pair of adjoint functors. Assume that $L$ sends any arrow in $\mathcal{M}_{\mathbb{D}}$ to one in $\mathcal{M}_{\mathbb{C}}$. For any $\mathcal{M}_{\mathbb{C}}$-injective $C \in \mathbb{C}$, $RC \in \mathbb{D}$ is $\mathcal{M}_{\mathbb{D}}$-injective.

*Proof.* It suffices to show that $\mathbb{D}(-, RC): \mathbb{D}^{\text{op}} \to \mathbf{Set}$ sends each arrow in $\mathcal{M}_{\mathbb{D}}$ to a surjective map. By the assumption, the functor above factorizes to $L: \mathbb{D} \to \mathbb{C}$ and $\mathbb{C}(-, C): \mathbb{D}^{\text{op}} \to \mathbf{Set}$. The former sends each arrow in $\mathcal{M}_{\mathbb{D}}$ to one in $\mathcal{M}_{\mathbb{C}}$ and the latter sends one in $\mathcal{M}_{\mathbb{C}}$ to a surjective map. Thus, the composition of these sends each arrow in $\mathcal{M}_{\mathbb{D}}$ to a surjective map. $\square$

For epireflective subcategories, we have a sharper result:

**Proposition 28.** In the setting of Proposition 27, assume, in addition,

- $R$ is fully faithful,

- $R$ sends each arrow in $\mathcal{M}_{\mathbb{C}}$ to one in $\mathcal{M}_{\mathbb{D}}$, and

- each component of the unit $\eta: \text{Id} \to RL$ is an epimorphism in $\mathcal{M}_{\mathbb{D}}$.

Then, $D \in \mathbb{D}$ is $\mathcal{M}_{\mathbb{D}}$-injective if and only if it is isomorphic to $RC$ for some $\mathcal{M}_{\mathbb{C}}$-injective $C \in \mathbb{C}$.
*Proof.* The “if” part is Proposition 27. We show the “only if” part.

Let $D \in \mathbb{D}$ be any $\mathcal{M}_{\mathbb{D}}$-injective object. Since $\eta_D: D \to \mathrm{RLD}$ is in $\mathcal{M}_{\mathbb{D}}$, we can use the $\mathcal{M}_{\mathbb{D}}$-injectiveness of $D$ to obtain $f: \mathrm{RLD} \to D$ such that $f \circ \eta_D = \mathrm{id}_D$. Here, $\eta_D \circ f \circ \eta_D = \eta_D$ and, by epi-ness of $\eta_D$, $\eta_D \circ f = \mathrm{id}_{\mathrm{RLD}}$. Thus, $\eta_D$ is an isomorphism.

Now we show that $\mathrm{LD}$ is $\mathcal{M}_{\mathbb{C}}$-injective. Let $f: C \to \mathrm{LD}$ and $g: C \to C'$ be any arrow in $\mathbb{C}$ and assume that $g$ is in $\mathcal{M}_{\mathbb{C}}$. Send these by $R$ to $\mathbb{D}$ and consider $Rf$ and $Rg$. By the assumption, $Rg$ is in $\mathcal{M}_{\mathbb{D}}$. Since $\mathrm{RLD}$ is isomorphic to $D$, it is also $\mathcal{M}_{\mathbb{D}}$-injective. Using these, we can obtain $h': RC' \to \mathrm{RLD}$ such that $h' \circ Rg = Rf$. Since $R$ is full, there is $h: C' \to \mathrm{LD}$ such that $Rh = h'$. The faithfulness of $R$ implies $h \circ g = f$. Thus $\mathrm{LD}$ is $\mathcal{M}_{\mathbb{C}}$-injective. $\square$

Using this result, we can identify c-injective objects in a few situations.

*Example 29 (continuous lattices in Top $\to$ Set [30]).* In the setting of Proposition 28, consider the case where $\mathbb{D} = \mathrm{Top}$, $\mathbb{C} = \mathrm{Top}_0$. Here $\mathrm{Top}_0$ is the full subcategory of **Top** of $T_0$ spaces. Let $R$ be the inclusion. It has a left adjoint $L$, taking each space to its Kolmogorov quotient. Let $\mathcal{M}_{\mathbb{C}}$ be the class of topological embeddings (i.e. homeomorphisms to their images) and $\mathcal{M}_{\mathbb{D}}$ be the class of Cartesian arrows (w.r.t. the fibration **Top** $\to$ **Set**). Then the assumptions in Proposition 28 are satisfied and we can conclude that c-injective objects in **Top** are precisely injective objects in $\mathrm{Top}_0$ w.r.t. embeddings.

The latter has been identified by Scott [30]. According to his result, such objects are precisely *continuous lattices* with the Scott topology. Thus, we can see that c-injective objects in **Top** are precisely such spaces.

*Example 30 (complete lattices in Pre $\to$ Set [4]).* In the setting of Proposition 28, consider the case where $\mathbb{D} = \mathrm{Pre}$, $\mathbb{C} = \mathrm{Pos}$. Here **Pos** is the full subcategory of **Pre** of posets. Let $R$ be the inclusion. It has a left adjoint $L$, taking each preordered set to its poset reflection. Let $\mathcal{M}_{\mathbb{C}}$ be the class of embeddings and $\mathcal{M}_{\mathbb{D}}$ be the class of Cartesian arrows (w.r.t. the fibration **Pre** $\to$ **Set**). Then the assumptions in Proposition 28 are satisfied and we can conclude that c-injective objects in **Pre** are precisely injective objects in **Pos** w.r.t. embeddings.

The latter has been identified by Banaschewski and Bruns [4]. According to their result, such objects are precisely complete lattices. Thus, we can see that c-injective objects in **Pre** are precisely complete lattices.

## 4.2 Results Specific to C-injective Objects

To develop the theory of c-injective objects further, we establish some preservation results for c-injectivity. Based on the two propositions of the last section, we show two propositions specific to fibrations and c-injective objects.

From Proposition 27, we can derive the following:

**Proposition 31.** Let $p: \mathbb{E} \to \mathbb{C}$, $q: \mathbb{F} \to \mathbb{D}$ be $\mathrm{CLat}_{\mathbb{N}}$-fibrations and $L \dashv R: \mathbb{E} \to \mathbb{F}$ be a pair of adjoint functors. If $L$ is fibered (from $q$ to $p$), then $RE \in \mathbb{F}$ is c-injective (in $q$) for each c-injective $E \in \mathbb{E}$.
Proof. Let $\mathcal{M}_E$ be the class of all arrows Cartesian w.r.t. $p$ and $\mathcal{M}_F$ be the class of all arrows Cartesian w.r.t. $q$. Then, use Proposition 27 to the pair $L \dashv R$ of adjoint functors. $\square$

From Proposition 28, we can derive the following:

**Proposition 32.** In the setting of Proposition 31, assume in addition that both $L$ and $R$ are fibered and that $\eta: \mathrm{Id} \to RL$ is componentwise epi. Then, $F \in \mathcal{F}$ is c-injective if and only if it is isomorphic to $RE$ for some c-injective $E \in \mathcal{E}$.

Proof. Use Proposition 28 in the same setting as the proof of Proposition 31. $\square$

# 5 Examples

We list several examples of Theorem 20. Indeed, most of the examples listed in [18, Table VI] turn out to be fibered by Theorem 20. Since the conditions in Theorem 20 only refer to $p: \mathcal{E} \to \mathbb{C}$ and $\Omega$, we sort the examples by these data.

We here recall some basic functors considered:

**Definition 33.** Let $\mathcal{P}: \mathrm{Set} \to \mathrm{Set}$ be the covariant powerset functor and $\mathcal{D}_{\le 1}: \mathrm{Set} \to \mathrm{Set}$ be the subdistribution functor. Here, a subdistribution $p \in \mathcal{D}_{\le 1}X$ is a measure on the $\sigma$-algebra of all subsets of $X$ with total mass $\le 1$. We abbreviate $p(\{x\})$ to $p(x)$.

## 5.1 Kantorovich Lifting

In Example 18 we have seen that, in the fibration $\mathrm{PMet}_{\top} \to \mathrm{Set}$, the object $([0, \top], d_{\mathbb{R}})$ is c-injective. We gather examples of this case here. As mentioned in Example 22 and Example 25, this class of examples has been already studied and shown to be fibered in [3,19].

**Example 34 (Hausdorff pseudometric).** Let $\inf: \mathcal{P}[0, \top] \to [0, \top]$ be the map taking any set to its infimum. Then, the codensity lifting $\mathcal{P}([0, \top], d_{\mathbb{R}})_{\inf}: \mathrm{PMet}_{\top} \to \mathrm{PMet}_{\top}$ turns out to induce the Hausdorff distance: for any $(X, d_X) \in \mathrm{PMet}_{\top}$, if we let $(\mathcal{P}X, d_{\mathcal{P}X}) = \mathcal{P}([0, \top], d_{\mathbb{R}})_{\inf}(X, d_X)$, then

$$d_{\mathcal{P}X}(S, T) = \max \left( \sup_{x \in S} \inf_{y \in T} d_X(x, y), \sup_{y \in T} \inf_{x \in S} d_X(x, y) \right)$$

holds for any $S, T \in \mathcal{P}X$. By Theorem 20, this functor is fibered.

**Example 35 (Kantorovich pseudometric).** Let $e: \mathcal{D}_{\le 1}[0, \top] \to [0, \top]$ be the map taking any distribution to its expected value. Then, the codensity lifting

$$\mathcal{D}_{\le 1}([0, \top], d_{\mathbb{R}})^e: \mathrm{PMet}_{\top} \to \mathrm{PMet}_{\top}$$

turns out to induce the Kantorovich distance: for any $(X, d_X) \in \mathrm{PMet}_{\top}$, if we let $(\mathcal{D}_{\le 1}X, d_{\mathcal{D}_{\le 1}X}) = \mathcal{D}_{\le 1}([0, \top], d_{\mathbb{R}})^e(X, d_X)$, then

$$d_{\mathcal{D}_{\le 1}X}(p, q) = \sup_{f: (X, d_X) \to ([0, \top], d_{\mathbb{R}}) \text{ nonexpansive}} \left| \sum_{x \in X} f(x)p(x) - \sum_{x \in X} f(x)q(x) \right|$$

holds for any $p, q \in \mathcal{D}_{\le 1}X$. By Theorem 20, this functor is fibered.
## 5.2 Lower, Upper, and Convex Preorders

In Example 30, we have identified complete lattices as c-injective objects in the fibration Pre → Set. In particular, the two-point set $(2, \leq)$ is a c-injective object (Example 17).

Katsumata and Sato [16, Section 3.1] used codensity lifting to recover the lower, upper, and convex preorders on powersets. Here we see that our result applies to them: all of the following liftings are fibered.

**Example 36 (lower preorder).** Define $\diamond: \mathcal{P}2 \to 2$ so that $\diamond S = \top$ if and only if $\top \in S$. Then, the codensity lifting $\mathcal{P}^{(2, \leq), \diamond}: \text{Pre} \to \text{Pre}$ turns out to induce the lower preorder: if we let $(\mathcal{P}X, \leq_{\mathcal{P}X}) = \mathcal{P}^{(2, \leq), \diamond}(X, \leq_X)$, then, for any $S, T \in \mathcal{P}X$,

$$S \leq_{\mathcal{P}X} T \Leftrightarrow \forall x \in S, \exists y \in T, x \leq_X y.$$

**Example 37 (upper preorder).** Define $\Box: \mathcal{P}2 \to 2$ so that $\Box S = \top$ if and only if $\bot \notin S$. Then, the codensity lifting $\mathcal{P}^{(2, \leq), \Box}: \text{Pre} \to \text{Pre}$ turns out to induce the upper preorder: if we let $(\mathcal{P}X, \leq_{\mathcal{P}X}) = \mathcal{P}^{(2, \leq), \Box}(X, \leq_X)$, then, for any $S, T \in \mathcal{P}X$,

$$S \leq_{\mathcal{P}X} T \Leftrightarrow \forall y \in T, \exists x \in S, x \leq_X y.$$

**Example 38 (convex preorder).** Denote the family of the two lifting parameters above by $((2, \leq), \{\diamond, \Box\})$. Then, the codensity lifting (with multiple parameters, Definition 23) $\mathcal{P}^{(2, \leq), \{\diamond, \Box\}}: \text{Pre} \to \text{Pre}$ is simply the meet of $\mathcal{P}^{(2, \leq), \diamond}$ and $\mathcal{P}^{(2, \leq), \Box}$. This is what is called the convex preorder.

**Remark 39.** The original formulation [16, Section 3.1] is based on codensity lifting of monads, so apparently different to ours. In our terms, they used the multiplication $\mu_1: \mathcal{P}\mathcal{P}1 \to \mathcal{P}1$ and two different preorders on $\mathcal{P}1$. Using two different bijections between $\mathcal{P}1$ and $2$, it can be shown that their formulation is actually equivalent to ours.

## 5.3 Equivalence relations

In Example 16 we have seen that, in the fibration EqRel → Set, the object $(2, =)$ is c-injective. We gather examples of this case here. All of the following liftings are fibered. Details on the following examples can be found in [18].

**Example 40 (lifting for bisimilarity on Kripke frames).** Consider the codensity lifting $\mathcal{P}^{(2, =), \diamond}: \text{EqRel} \to \text{EqRel}$, where $\diamond$ is as defined in Example 36. This turns out to satisfy the following: if we let $(\mathcal{P}X, \sim_{\mathcal{P}X}) = \mathcal{P}^{(2, =), \diamond}(X, \sim_X)$, then

$$S \sim_{\mathcal{P}X} T \Leftrightarrow (\forall x \in S, \exists y \in T, x \sim_X y) \wedge (\forall y \in T, \exists x \in S, x \sim_X y)$$

holds for any $S, T \in \mathcal{P}X$. This can be used to define (the conventional notion of) bisimilarity on Kripke frames ($\mathcal{P}$-coalgebras).

**Example 41 (lifting for bisimilarity on Markov chains).** For each $r \in [0, 1]$, define a map $\text{thr}_r: \mathcal{D}_{\leq 1} 2 \to 2$ so that $\text{thr}_r(p) = \top$ if and only if $p(\top) \geq r$. These define a $[0, 1]$-indexed family of lifting parameters $((2, =), \text{thr}_r)_{r \in [0, 1]}$. The codensity lifting $\mathcal{D}_{\leq 1}^{(2, =), \text{thr}}$ defined by this family can be used to define probabilistic bisimilarity on Markov chains ($\mathcal{D}_{\leq 1}$-coalgebras).
## 5.4 Topologies

In Example 29, we have identified c-injective objects in the fibration **Top** → **Set**.
In particular, the *Sierpinski space*, defined as follows, is a c-injective object:

**Definition 42 (Sierpinski space).** The *Sierpinski space* is a topological space (2, O_0) where 2 = {⊥, ⊤} and the family O_0 of open sets is {0, {⊤}, 2}. We denote this space by O.

The following liftings of $\mathcal{P}$ have appeared in [16, Section 3.2]. All of them are
fibered: in other words, they send embeddings to embeddings.

*Example 43 (lower Vietoris lifting).* Consider the codensity lifting $\mathcal{P}^{\diamond, \diamond}: \mathbf{Top} \to \mathbf{Top}$, where $\diamond$ is as defined in Example 36. For each $(X, \mathcal{O}_X) \in \mathbf{Top}$, if we let $(\mathcal{P}X, \mathcal{O}_{\mathcal{P}X}^{\diamond}) = \mathcal{P}^{\diamond, \diamond}(X, \mathcal{O}_X)$, then the topology $\mathcal{O}_{\mathcal{P}X}^{\diamond}$ is the coarsest one such that, for each $U \in \mathcal{O}_X$, the set $\{V \subseteq X \mid V \cap U \neq \emptyset\}$ is open. This is called lower Vietoris lifting in [16].

*Example 44 (upper Vietoris lifting).* Consider the codensity lifting $\mathcal{P}^{\square, \square}: \mathbf{Top} \to \mathbf{Top}$, where $\square$ is as defined in Example 37. For each $(X, \mathcal{O}_X) \in \mathbf{Top}$, if we let $(\mathcal{P}X, \mathcal{O}_{\mathcal{P}X}^{\square}) = \mathcal{P}^{\square, \square}(X, \mathcal{O}_X)$, then the topology $\mathcal{O}_{\mathcal{P}X}^{\square}$ is the coarsest one such that, for each $U \in \mathcal{O}_X$, the set $\{V \subseteq X \mid V \subseteq U\}$ is open. This is called upper Vietoris lifting in [16].

*Example 45 (Vietoris lifting).* Define the codensity lifting $\mathcal{P}^{\square, \{\diamond, \square\}}: \mathbf{Top} \to \mathbf{Top}$ like one in Example 38. We call this *Vietoris lifting*.

This turns out to be connected to *Vietoris topology* [20] as follows. For each $(X, \mathcal{O}_X) \in \mathbf{Top}$, let $(\mathcal{P}X, \mathcal{O}_{\mathcal{P}X}^{\diamond, \square}) = \mathcal{P}^{\square, \{\diamond, \square\}}(X, \mathcal{O}_X)$. The set $K(X, \mathcal{O}_X)$ of closed subsets of $(X, \mathcal{O}_X)$ is a subset of $\mathcal{P}X$. Here, the topology on $K(X, \mathcal{O}_X)$ induced from $\mathcal{O}_{\mathcal{P}X}^{\diamond, \square}$ is the same as the Vietoris topology.

This coincidence and the fiberedness of $\mathcal{P}^{\square, \{\diamond, \square\}}$ implies that the *Vietoris functor* $\mathbf{V}: \mathbf{Stone} \to \mathbf{Stone}$, defined in [20], sends embeddings to embeddings.

In [18], we considered another lifting:

*Example 46 (lifting for bisimulation topology).* Fix any set $\Sigma$. Let $A_\Sigma$: **Set** → **Set** be the functor defined by $A_\Sigma X = 2 \times X^\Sigma$. Define acc: $A_\Sigma 2 \to 2$ by $\text{acc}(t, \rho) = t$. For each $a \in \Sigma$, define $\langle a \rangle$: $A_\Sigma 2 \to 2$ by $\langle a \rangle (t, \rho) = \rho(a)$. Here, $(\emptyset, \text{acc})$ and $(\emptyset, \langle a \rangle)$ for each $a \in \Sigma$ consist of a family of lifting parameters. The codensity lifting (with multiple parameters, Definition 23) $A_\Sigma^{\emptyset, \{\text{acc}\} \cup \{\langle a \rangle | a \in \Sigma\}}$: **Top** → **Top** was used to define *bisimulation topology* for deterministic automata ($A_\Sigma$-coalgebras). This is fibered. This fact is used in Example 51, where we will look at bisimulation topology again.

# 6 Application to Codensity Bisimilarity

Now we present an application of our main result. Based on codensity lifting,
we defined codensity bisimilarity in [18]. It subsumes bisimilarity, simulation
preorder, and behavioral metric as special cases. Here we see that, in the cases to which our fiberedness result applies, codensity bisimilarity interacts well with coalgebra morphisms. In particular, the codensity bisimilarity on any coalgebra is determined by that on the final coalgebra, if it exists.

Recall the definition of coalgebra:

**Definition 47 (coalgebra of an endofunctor).** Let $F: \mathbb{C} \to \mathbb{C}$ be an endofunctor on a category $\mathbb{C}$. An $F$-coalgebra is a pair of an object $X \in \mathbb{C}$ and an arrow $c: X \to FX$.

Let $c: X \to FX$ and $d: Y \to FY$ be $F$-coalgebras. A morphism of coalgebras from $(X, c)$ to $(Y, d)$ is an arrow $f: X \to Y$ in $\mathbb{C}$ such that $d \circ f = Ff \circ c$ holds.

As sketched in Section 1, functor lifting can be used to define a “bisimilarity-like notion”. If we use codensity lifting in this construction, we obtain the following definition:

**Definition 48 (codensity bisimilarity [18, Definitions III.6 and III.8]).** Assume the setting of Definition 23. Let $c: X \to FX$ be any $F$-coalgebra. Define $\Phi_c^{\Omega, \tau}: \mathbb{E}_X \to \mathbb{E}_X$ by $\Phi_c^{\Omega, \tau} P = c^* (F^{\Omega, \tau} P)$.

The $((\Omega, \tau)-)codensity$ bisimilarity is the greatest fixed point (w.r.t. $\sqsubseteq$) of $\Phi_c^{\Omega, \tau}$. We denote this by $\nu\Phi_c^{\Omega, \tau}$.

Note that the greatest fixed point of $\Phi_c^{\Omega, \tau}$ always exists. This can be seen, for example, by the Tarski fixed point theorem. Another option is to use the constructive fixed point theorem by Cousot and Cousot [6]. We use their characterization of the greatest fixed point to prove the following proposition:

**Proposition 49 (stability of codensity bisimilarity).** Assume the setting of Definition 23 (codensity lifting with multiple parameters). Assume also that each $\Omega_a$ is a c-injective object. Then, codensity bisimilarity is stable under coalgebra morphisms: for any morphism of coalgebras $f$ from $(X, c)$ to $(Y, d)$, we have $\nu\Phi_c^{\Omega, \tau} = f^* (\nu\Phi_d^{\Omega, \tau})$.

*Proof.* Define a transfinite sequence $(\nu_\alpha \Phi_c^{\Omega, \tau})_{\alpha \text{ is an ordinal}}$ of elements of $\mathbb{E}_X$ by the following:

$$ \nu_\alpha \Phi_c^{\Omega, \tau} = \bigcap_{\beta < \alpha} \Phi_c^{\Omega, \tau} (\nu_\beta \Phi_c^{\Omega, \tau}). $$

Define another transfinite sequence $(\nu_\alpha \Phi_d^{\Omega, \tau})_{\alpha \text{ is an ordinal}}$ by a similar manner. By the result in [6], there is an ordinal $\gamma$ such that $\nu_\gamma \Phi_c^{\Omega, \tau} = \nu_\gamma \Phi_c^{\Omega, \tau}$ and $\nu_\gamma \Phi_d^{\Omega, \tau} = \nu_\gamma \Phi_d^{\Omega, \tau}$. 3 Thus, it suffices to show the following claim:

**Claim.** For any ordinal $\alpha$, we have $\nu_\alpha \Phi_c^{\Omega, \tau} = f^* (\nu_\alpha \Phi_d^{\Omega, \tau})$.

<footnote n="3">3 This formulation differs slightly from the conventional one where successor and limit ordinals are distinguished, but the result also holds under this definition.</footnote>
We show this by transfinite induction on $\alpha$. Assume the claim holds for all $\beta < \alpha$.

Using the assumption that $f$ is a morphism of coalgebras, the fiberedness of $F^{\Omega, \tau}$ (Corollary 24), and the functoriality of pullback (Proposition 5), we have $f^* \circ \Phi_d^{\Omega, \tau} = \Phi_c^{\Omega, \tau} \circ f^*$. It implies the claim for $\alpha$

$$ \begin{align*} f^*(\nu_\alpha \Phi_d^{\Omega, \tau}) &= f^* \left( \bigcap_{\beta < \alpha} \Phi_d^{\Omega, \tau} (\nu_\beta \Phi_d^{\Omega, \tau}) \right) = \bigcap_{\beta < \alpha} f^* (\Phi_d^{\Omega, \tau} (\nu_\beta \Phi_d^{\Omega, \tau})) \\ &= \bigcap_{\beta < \alpha} \Phi_c^{\Omega, \tau} (f^* \nu_\beta \Phi_d^{\Omega, \tau}) = \bigcap_{\beta < \alpha} \Phi_c^{\Omega, \tau} (\nu_\beta \Phi_c^{\Omega, \tau}) \\ &= \nu_\alpha \Phi_c^{\Omega, \tau}. \end{align*} \quad \square $$

In particular, the codensity bisimilarity is determined by that on the final coalgebra:

**Corollary 50.** Assume the setting of Proposition 49. Assume also that there exists a final $F$-coalgebra $z: Z \to FZ$. Then, for any $F$-coalgebra $c: X \to FX$, the unique coalgebra morphism $!_X: X \to Z$ satisfies $\nu \Phi_c^{\Omega, \tau} = (!_X)^* (\nu \Phi_z^{\Omega, \tau})$.

*Example 51 (bisimulation topology for deterministic automata).* Recall Example 46. For any $A_\Sigma$-coalgebra $c: X \to A_\Sigma X$, we defined the codensity bisimilarity on $X$ by $\nu \Phi_c^{\Omega, \{acc\} \cup \{\langle a \rangle | a \in \Sigma\}} \in \mathbf{Top}_X$ [18].

The functor $A_\Sigma$ has a final coalgebra: the set $2^{\Sigma^*}$ of all languages on the alphabet $\Sigma$ can be given an $A_\Sigma$-coalgebra structure and it is final. For an $A_\Sigma$-coalgebra $c: X \to A_\Sigma X$, the unique coalgebra morphism $l: X \to 2^{\Sigma^*}$ assigns to each state the recognized language when started from it.

Corollary 50 implies that this map $l$ determines the bisimulation topology on $X$. We believe that this fact is new, and it supports our use of the term language topology in [18, §VIII-C].

# 7 Conclusions

Inspired by the proof of fiberedness of Kantorovich lifting [3], we showed a sufficient condition for codensity lifting to be fibered. We listed a number of examples that satisfy the sufficient condition. In addition, we apply the fiberedness to show a result on codensity bisimilarity.

One possible direction of research is to investigate the notion of c-injectiveness in more depth. The existing work on injective objects in homological algebra and topos theory can be a clue for that. In particular, we have not studied which category has enough c-injectives. This may be connected with some deep fibrational property.

Another possible direction is to generalize the main result. In [16], codensity lifting of a monad was introduced for a general fibration in terms of right Kan
extension. This definition can readily be adapted to endofunctors, but in the
current paper, we considered only CLat_n-fibrations. Extending the main result
to this general situation, in particular, to non-poset fibrations, may broaden the
scope of application. It can also be fruitful to extend the definition of codensity
lifting itself: for example, in Definition 13, we could substitute τ*Ω with other
objects above FΩ.<fnref n="4" /> Seeking consequences and examples of this version of the
definition is future work. Another related research direction is to obtain a similar
sufficient condition for fiberedness of categorical ⊤⊤-lifting [15].

Last but not least, we have to seek other applications. As mentioned in Sec-
tion 1, functor lifting is used in many situations. Using codensity lifting there
and seeing what can be implied by the current result seems to be a promising
research direction. In particular, codensity lifting seems to be intimately con-
nected to coalgebraic modal logic, where τ : FΩ → Ω is regarded as a modality.
Recently, Kupke and Rot [21] have identified a sufficient condition for a logic
to expressive w.r.t. a coinductive predicate (like bisimilarity, behavioral metric
etc.). They used fiberedness of lifting in a crucial way (they use the term fi-
bration map), which suggests that the current work can play a pivotal role in
investigating modal logics.

**Acknowledgments** The author is grateful to Ichiro Hasuo and Shin-ya Kat-
sumata for fruitful discussions on technical and structural points. The author is
also indebted to anonymous reviewers for clarifying things and pointing out pos-
sible future directions, including a topos-theoretic viewpoint and an alternative
definition of codensity lifting.

References

1. Baer, R.: Abelian groups that are direct summands of every containing abelian group. Bull. Amer. Math. Soc. **46**(10), 800–806 (10 1940), https://projecteuclid.org:443/euclid.bams/1183503234

2. Baldan, P., Bonchi, F., Kerstan, H., König, B.: Behavioral Metrics via Func-tor Lifting. In: Raman, V., Suresh, S.P. (eds.) 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014). Leibniz International Proceedings in Informatics (LIPIcs), vol. 29, pp. 403–415. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany (2014). https://doi.org/10.4230/LIPIcs.FSTTCS.2014.403, http://drops.dagstuhl.de/opus/volltexte/2014/4859

3. Baldan, P., Bonchi, F., Kerstan, H., König, B.: Coalgebraic behav-
ioral metrics. Logical Methods in Computer Science 14(3) (2018).
https://doi.org/10.23638/LMCS-14(3:20)2018, https://doi.org/10.23638/LMCS-14(3:20)2018

4. Banaschewski, B., Bruns, G.: Categorical characterization of the mac-
neille completion. Archiv der Mathematik 18(4), 369–377 (Sep 1967).
https://doi.org/10.1007/BF01898828, https://doi.org/10.1007/BF01898828

<footnote n="4">⁴ This has been pointed out by an anonymous reviewer.</footnote>
5. Chatzikokolakis, K., Gebler, D., Palamidessi, C., Xu, L.: Generalized bisimula-
tion metrics. In: Baldan, P., Gorla, D. (eds.) CONCUR 2014 - Concurrency The-
ory - 25th International Conference, CONCUR 2014, Rome, Italy, September 2-
5, 2014. Proceedings. Lecture Notes in Computer Science, vol. 8704, pp. 32–46.
Springer (2014). https://doi.org/10.1007/978-3-662-44584-6_4, https://doi.org/10.
1007/978-3-662-44584-6_4

6. Cousot, P., Cousot, R.: Constructive versions of tarski's fixed point theorems. Pacific J. Math. **82**(1), 43–57 (1979), https://projecteuclid.org:443/euclid.pjm/1102785059

7. Espínola, R., Khamsi, M.A.: Introduction to Hyperconvex Spaces, pp. 391–435. Springer Netherlands, Dordrecht (2001). https://doi.org/10.1007/978-94-017-1748-9_13, https://doi.org/10.1007/978-94-017-1748-9_13

8. Fujii, S.: Enriched categories and tropical mathematics (2019)

9. Hasuo, I., Cho, K., Kataoka, T., Jacobs, B.: Coinductive predicates and final sequences in a fibration. Electron. Notes Theor. Comput. Sci. **298**, 197–214 (Nov 2013). https://doi.org/10.1016/j.entcs.2013.09.014, http://dx.doi.org/10.1016/j.entcs.2013.09.014

10. Hermida, C.: Fibrations, logical predicates and indeterminates. Ph.D. thesis, Uni-
versity of Edinburgh, UK (1993)

11. 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, http:
//www.sciencedirect.com/science/article/pii/S0890540198927250

12. Hilton, P.J., Stammbach, U.: A Course in Homological Algebra, Graduate Texts in Mathematics, vol. 4. Springer-Verlag New York (1997)

13. Jacobs, B.: Categorical Logic and Type Theory. No. 141 in Studies in Logic and the Foundations of Mathematics, North Holland, Amsterdam (1999)

14. Kashiwara, M., Schapira, P.: Categories and Sheaves, Grundlehren der mathema-
tischen Wissenschaften, vol. 332. Springer-Verlag Berlin Heidelberg (2006)

15. Katsumata, S.: A semantic formulation of tt-lifting and logical predicates for com-
putational metalanguage. In: Ong, C.L. (ed.) Computer Science Logic, 19th In-
ternational Workshop, CSL 2005, 14th Annual Conference of the EACSL, Ox-
ford, UK, August 22-25, 2005, Proceedings. Lecture Notes in Computer Sci-
ence, vol. 3634, pp. 87–102. Springer (2005). https://doi.org/10.1007/11538363.8,
https://doi.org/10.1007/11538363.8

16. Katsumata, S., Sato, T.: Codensity Liftings of Monads. In: Moss, L.S., Sobocinski, P. (eds.) 6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015). Leibniz International Proceedings in Informatics (LIPIcs), vol. 35, pp. 156–170. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany (2015). https://doi.org/10.4230/LIPIcs.CALCO.2015.156, http://drops.dagstuhl.de/opus/volltexte/2015/5532

17. Klin, B.: The least fibred lifting and the expressivity of coalgebraic modal logic. In: Fiadeiro, J.L., Harman, N., Roggenbach, M., Rutten, J.J.M.M. (eds.) Algebra and Coalgebra in Computer Science: First International Conference, CALCO 2005, Swansea, UK, September 3-6, 2005, Proceedings. Lecture Notes in Computer Science, vol. 3629, pp. 247–262. Springer (2005). https://doi.org/10.1007/11548133-16, https://doi.org/10.1007/11548133-16

18. Komorida, Y., Katsumata, S., Hu, N., Klin, B., Hasuo, I.: Codensity games for bisimilarity. In: 2019 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) (June 2019). https://doi.org/10.1109/LICS.2019.8785691
19. König, B., Mika-Michalski, C.: (Metric) Bisimulation Games and Real-Valued Modal Logics for Coalgebras. In: Schewe, S., Zhang, L. (eds.) 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), vol. 118, pp. 37:1–37:17. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany (2018). https://doi.org/10.4230/LIPIcs.CONCUR.2018.37, http://drops.dagstuhl.de/opus/volltexte/2018/9575

20. Kupke, C., Kurz, A., Venema, Y.: Stone coalgebras. Electr. Notes Theor. Comput. Sci. 82(1), 170–190 (2003). https://doi.org/10.1016/S1571-0661(04)80638-8, https://doi.org/10.1016/S1571-0661(04)80638-8

21. Kupke, C., Rot, J.: Expressive logics for coinductive predicates (2020), to appear in Proc. CSL2020

22. Leinster, T.: Codensity and the ultrafilter monad. TAC (2013)

23. Leinster, T.: Basic Category Theory. Cambridge Studies in Advanced Mathematics, Cambridge University Press (2014). https://doi.org/10.1017/CBO9781107360068

24. Mac Lane, S.: Categories for the Working Mathematician. Springer, New York, NY (1978)

25. Milner, R.: Communication and Concurrency. Prentice-Hall (1989)

26. Park, D.: Concurrency and automata on infinite sequences. In: Proceedings of the 5th GI-Conference on Theoretical Computer Science. pp. 167–183. Springer-Verlag, London, UK, UK (1981), http://dl.acm.org/citation.cfm?id=647210.720030

27. Rutten, J.J.M.M.: Universal coalgebra: a theory of systems. Theor. Comput. Sci. 249(1), 3–80 (2000). https://doi.org/10.1016/S0304-3975(00)00056-6, https://doi.org/10.1016/S0304-3975(00)00056-6

28. Sangiorgi, D.: Introduction to Bisimulation and Coinduction. Cambridge University Press (2011). https://doi.org/10.1017/CBO9780511777110

29. Sato, T., Barthe, G., Gaboardi, M., Hsu, J., Katsumata, S.: Approximate span liftings: Compositional semantics for relaxations of differential privacy. In: 34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2019, Vancouver, BC, Canada, June 24-27, 2019. pp. 1–14. IEEE (2019). https://doi.org/10.1109/LICS.2019.8785668, https://doi.org/10.1109/LICS.2019.8785668

30. Scott, D.: Continuous lattices. In: Lawvere, F.W. (ed.) Toposes, Algebraic Geometry and Logic. pp. 97–136. Springer Berlin Heidelberg, Berlin, Heidelberg (1972)

31. Sprunger, D., Katsumata, S., Dubut, J., Hasuo, I.: Fibrational bisimulations and quantitative reasoning. In: Cirstea, C. (ed.) Coalgebraic Methods in Computer Science. pp. 190–213. Springer International Publishing, Cham (2018)