# On the Logic of Generalised Metric Spaces

Octavian Babus, Alexander Kurz

► To cite this version:

Octavian Babus, Alexander Kurz. On the Logic of Generalised Metric Spaces. 13th International Workshop on Coalgebraic Methods in Computer Science (CMCS), Apr 2016, Eindhoven, Netherlands. pp.136-155, 10.1007/978-3-319-40370-0_9. hal-01446037

HAL Id: hal-01446037

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

Submitted on 25 Jan 2017

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
# On the logic of generalised metric spaces

Octavian Babus¹ and Alexander Kurz²

¹ University of Leicester, UK
octavianbabus@yahoo.com

² University of Leicester, UK
ak155@le.ac.uk

**Abstract.** The aim of the paper is to work towards a generalisation of coalgebraic logic enriched over a commutative quantale. Previous work has shown how to dualise the coalgebra type functor $T : \Omega\text{-Cat} \to \Omega\text{-Cat}$ in order to obtain the modal operators and axioms describing transitions of type $T$. Here we give a logical description of the dual of $\Omega\text{-Cat}$.

## 1 Introduction

Recently, following on work of Rutten [18] and Worrell [24], the interest in coalgebras enriched over posets or, more generally, enriched over a commutative quantale has attracted some attention. In particular, the question of a coalgebraic logic in this setting has been asked [2].

In the non-enriched situation we start with a functor $T : \mathbf{Set} \to \mathbf{Set}$ and ask for a logic that allows us to completely describe $T$-coalgebras up to bisimilarity. More specifically, we would like to ensure *strong expressivity* in the sense that for any property $p \subseteq X$ of any $T$-coalgebra $(X, \xi)$ there is a formula $\phi$ such that $p$ coincides with the semantics $\llbracket \phi \rrbracket_{(X,\xi)}$ of $\phi$ on $(X, \xi)$. Moreover, we would like to have *completeness* in the sense that if $\llbracket \phi \rrbracket_{(X,\xi)} \subseteq \llbracket \phi \rrbracket_{(X,\xi)}$ then $\phi \le \psi$ in the initial algebra of formulas.

To achieve the above, the **first step** is to let $LA = [T([A, 2]), 2]$ in

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

and to declare the initial $L$-algebra, if it exists, as the “Lindenbaum-algebra” of $T$. This terminology is justified insofar as the adjoint transpose

$$ \delta : L([-, 2]) \to [T-, 2] $$
of the iso $L \to [T([-, 2]), 2]$ allows us to define the semantics $\mathbb{I}_{(X, \xi)}$ wrt a coalgebra $(X, \xi)$ as the unique arrow from the initial $L$-algebra $\iota : LI \to I$ as in

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

But the reason why, at this stage, we cannot truly speak of $\iota : LI \to I$ as a Lindenbaum algebra is that it lives in $\mathbf{Set}^{\mathrm{op}}$ and is not (yet) an algebra over $\mathbf{Set}$ with elements and operations in the usual sense.

The **second step**, then, consists in using the well-known fact that $[-, 2] : \mathbf{Set}^{\mathrm{op}} \to \mathbf{Set}$ is monadic and, therefore, $\mathbf{Set}^{\mathrm{op}}$ is equivalent to a category of algebras defined by operations and equations. In particular, we know that $\mathbf{Set}^{\mathrm{op}}$ is equivalent to the category of complete atomic Boolean algebras, which now allows us to consider $(L, \iota)$ as the Lindenbaum algebra of infinitary $T$-logic.

The aim of the paper is to carry out these steps in the case where we replace $\mathbf{Set}$ by the category $\Omega$-Cat of categories enriched over $\Omega$ for a commutative quantale $\Omega$. It is based on the $\Omega$-generalisations of the downset monad $\mathcal{D}$ and the upset monad $\mathcal{U}$. We will define algebras for operations $\Sigma_{\mathcal{D}\mathcal{U}}$ and equations $E_{\mathcal{D}\mathcal{U}}$ and will argue via (3), Theorem 16, Theorem 22, and Theorem 49 that $\langle \Sigma_{\mathcal{D}\mathcal{U}}, E_{\mathcal{D}\mathcal{U}} \rangle$-algebras complete the table

<table><tr><td>$\mathbf{Set}^{\mathrm{op}}$</td><td>complete atomic Boolean algebras</td></tr><tr><td>$\Omega$-Cat$^{\mathrm{op}}$</td><td>$\langle \Sigma_{\mathcal{D}\mathcal{U}}, E_{\mathcal{D}\mathcal{U}} \rangle$-algebras</td></tr></table>

Importantly, this includes an equation for generalised distributivity, Axiom (13), and will allow us to derive a logic for $\Omega$-Cat very much in the same way as we can say that Boolean logic is the logic of $\mathbf{Set}$.

**Related work.** The results in Section 3 generalize the results in [13] by Mar-molejo, Rosebrugh, and Wood to arbitrary commutative quantales $\Omega$ but the proofs remain the same as they work in any 3-category where 3-cells form a poset. Theorem 16 is also a special case of a theorem of Stubbe [19].

Section 4 generalises the well-known dual adjunction

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

between preorders and completely distributive lattices to categories enriched over a commutative quantale. This is similar in spirit to the work in Hofmann [5], where a generalisation from preorders to topological spaces and to approach spaces can be found.

The category of distributive complete $\Omega$-lattices of Lai and Zhang [9] coincides with what we denote CCD in Definition 18. Compared to their work, we add the
argument of how to obtain CCD from the monad [[-, Ω], Ω] and we show that the CCD is isomorphic to the category of (ordinary, set-based) ⟨Σ<sub>DU</sub>, E<sub>DU</sub>⟩-algebras.

In Pu and Zhang [14] it is shown, amongst other things, that the category of anti-symmetric CCD's is monadic over Set, but the proof proceeds by Beck's monadicity theorem whereas we give the operations and equations ⟨Σ<sub>DU</sub>, E<sub>DU</sub>⟩ explicitly.

The double powerset monad *DU* is investigated in detail, in the case Ω = 2, by Vickers in [23,20,21,22].

**Acknowledgement.** The second author acknowledges the influence of J. Velebil through a long-standing collaboration on enriched coalgebraic logic and his deep insights into the subject. In particular, our description of Ω-Cat<sup>OP</sup> by operations and equations confirms his suggestion that the propositional logic of Ω-Cat should have operations corresponding to the categorical (co)limits of tensor and cotensor.

## 2 Preliminaries and related work

We are interested in categories enriched over commutative quantales [15].

**Definition 1.** By a quantale Ω = ((Ω, ≤), e, ⊗) we understand a complete lattice with a binary operation ⊗ : Ω × Ω —→ Ω with unit e, such that ⊗ preserves colimits in both arguments. We call a quantale commutative if the operation ⊗ is commutative.

Since ⊗ preserves joins, a commutative quantale Ω can be considered as a symmetric monoidal closed category and one can enrich over Ω, see [7]. A category enriched over Ω is also called a Ω-category and the 2-category of Ω-categories, Ω-functors and Ω-natural transformations is denoted by Ω-Cat. The interpretation of such enriched categories as metric spaces is due to [10] and recalled in the following examples:

*Example 2.*

1. Ω = 2 = ((2, ≤), 1, ∧). Categories enriched over 2 are preorders and the corresponding functors are monotone maps. The closed structure is implication.

2. Ω = (([0, ∞], ≥<sub>ℝ</sub>), 0, +), the non-negative reals with infinity and the opposite of the natural order. That the top element is 0 formalises the idea that the elements of Ω measure distance from 'truth'. A Ω-category is called a *generalised metric space*. The corresponding functors are non-expansive maps. The closed structure is given by

$$[0, \infty](r, s) = s \div r = \text{if } s \leq_{ℝ} r \text{ then } 0 \text{ else } s - r$$

Examples include:

(a) [0, ∞] itself.
(b) The real numbers $(R, \leq_R)$ with the metric given by $R(a, b) = \begin{cases} a & \text{if } a \leq_R b \\ b & \text{else} \end{cases}$

(c) Any metric space.

3. $\Omega = (([0, 1], \leq_R), 1, \cdot)$ where $x \cdot y$ is the usual multiplication. Then

$$x \Rightarrow y = \begin{cases} y \\ \text{if } x \leq y \text{ then } 1 \text{ else } x \end{cases}$$

The exponential map $x \mapsto \exp(-x)$ induces an isomorphism from the $\Omega$ of the previous item, so that we can think of both representing two views of the same mathematics, one in terms of distances and the other in terms of truth-values.

4. $\Omega = (([0, 1], \geq_R), 0, \max)$. This is example is in the same spirit as above, but this time $\Omega$-categories are *generalised ultrametric spaces* [17]. The closed structure is given by

$$[0, 1](x, y) = \begin{cases} y & \text{if } x \geq_R y \\ 0 & \text{else} \end{cases}$$

Examples include:

(a) $[0, 1]$ itself, as well as $[0, 1]^{\text{op}}$ with 1 and min.

(b) Let $A^\infty$ be the finite and infinite words over $A$. Define $A^\infty(v, w) = 0$ if $v$ is a prefix of $w$ and $A^\infty(v, w) = 2^{-n}$ otherwise where $n \in \mathbb{N}$ is the largest number such that $v_n = w_n$ (where $v_n$ is the prefix of $v$ consisting of $n$ letters from $A$).

Whenever we talk about limits or colimits in a $\Omega$-category we understand a weighted limit or weighted colimit and we will use the same notations as in [7, Chapter 3].

Note that every $\Omega$-category $X$ is equipped with a preorder $x \leq y \Leftrightarrow X(x, y) \geq e$. We call a $\Omega$-category $X$ *anti-symmetric* if $x \leq y$ and $y \leq x$ implies $x = y$. In the examples above, this order coincides with the expected one. For example, in Example 2b the induced order on $R$ is the natural one and in Example 3b it is the prefix order.

**Proposition 3.** 1. The order $x \leq y \Leftrightarrow \Omega(x, y) \geq e$ is the order of $\Omega$.

2. $[X, \Omega]$ is anti-symmetric for any $\Omega$-category $X$.

3. $[X, Y]$ is anti-symmetric iff $Y$ is anti-symmetric.

We already said that $\Omega$-categories form a category $\Omega$-Cat of small $\Omega$-categories. $\Omega$-Cat is $\Omega$-Cat enriched, with the distance between two $\Omega$-functors $f, g : A \to B$ given by $\Omega$-Cat$(A, B)(f, g) = [A, B](f, g) = \bigwedge_{a \in A} B(fa, ga)$. Hence $\Omega$-Cat is an object of $(\Omega$-Cat)-Cat. The category $(\Omega$-Cat)-Cat of $\Omega$-Cat-categories, $\Omega$-Cat-functors, and $\Omega$-Cat-natural transformations is a 3-category in which natural transformations $\alpha, \beta : F \to G : A \to B$ are pre-ordered since $(\Omega$-Cat)-Cat$(A, B)(F, G)$ is a $\Omega$-category.

The reason to insist on pre-ordered natural transformations is that we can make use of the following notion due to [8] and reformulated by [12].
Writing down the formula for left and right Kan extensions, see [7, Chapter 4.2],
we obtain for $\varphi : X^{\text{op}} \to V$ and $\psi : X \to \Omega$

$$
\begin{align*}
\mathcal{D}f(\varphi) &= \mathrm{Lan}_{dX}(dY \circ f)(\varphi) = \int^{x \in X} [X^{\text{op}}, \Omega](X(-, x), \varphi) \otimes Y(-, f(x)) \\
&= \int^{x \in X} \varphi(x) \otimes Y(-, f(x)) = \varphi * (dY \circ f),
\end{align*}
$$

and

$$
\begin{align*}
\mathcal{U}f(\psi) &= \int_{x \in X} \mathcal{U}X(\psi, X(x, -)) \hat{\cap} Y(f(x), -) \\
&= \int_{x \in X} \psi(x) \hat{\cap} Y(f(x), -).
\end{align*}
$$

But considering that we calculate this end in $[Y, \Omega]^{\text{op}}$, in $[Y, \Omega]$ it becomes

$$
U f(\psi) = \int_{x \in X} \psi(x) \otimes Y(f(x), -) = \psi * (uY \circ f)
$$

Because $Dd$ and $uU$ are, respectively, left and right Kan extensions, their universal
properties yield

**Proposition 12.** *There exist natural transformations $\lambda : Dd \to dD$ and $\delta : uU \to Uu$.*

We want $\mathcal{D}$ to be a KZ-doctrine, so the multiplication $\mu : \mathcal{D}\mathcal{D} \to \mathcal{D}$ has to be a
left adjoint of $d\mathcal{D}$. As $d\mathcal{D}$ preserves all limits and the right Kan extension of $\mathrm{id}_\mathcal{D}$
along $d\mathcal{D}$ exists, using [7, Theorem 4.81], we know that the left adjoint of $d\mathcal{D}$
exists and is expressed by $\mathrm{Ran}_{d\mathcal{D}} \mathrm{id}_\mathcal{D}$. Dually, the right adjoint of $uU$ exists and
is expressed by $\mathrm{Lan}_{uU} \mathrm{id}_U$.

$$
\begin{tikzcd}[column sep=2.8em, row sep=2.8em]
    \mathcal{D}\mathcal{D} \arrow[r, "\mu"] \arrow[d, "\mathrm{Ran}_{d\mathcal{D}} \mathrm{id}_\mathcal{D}"'] & \mathcal{D} \\
    d\mathcal{D} \arrow[d, "\mathrm{id}_\mathcal{D}"'] & \mathcal{D}
\end{tikzcd}
\qquad
\begin{tikzcd}[column sep=2.8em, row sep=2.8em]
    \mathcal{U}\mathcal{U} \arrow[r, "\nu"] \arrow[d, "\mathrm{Lan}_{uU} \mathrm{id}_U"'] & \mathcal{U} \\
    u\mathcal{U} \arrow[d, "\mathrm{id}_U"'] & \mathcal{U}
\end{tikzcd}
\qquad (5)
$$

$$
\mu G = \int_{\varphi \in \mathcal{D}X} \mathcal{D}\mathcal{D}X(G, \mathcal{D}X(-, \varphi)) \hat{\cap} \varphi \qquad \nu F = \int_{\psi \in \mathcal{U}X} [\mathcal{U}X, \Omega](G, \mathcal{U}\mathcal{U}(\psi)) \hat{\cap} \psi \tag{6}
$$

Furthermore as $d\mathcal{D}$ and $uU$ are fully faithful, one has $\mu \circ d\mathcal{D} = \mathrm{id}_\mathcal{D}$ and $\nu \circ uU = \mathrm{id}_U$. Following Proposition 5 to show that $\mathcal{D}$ is a KZ-doctrine we just have to prove that $\mu \circ Dd = \mathrm{id}$ as well. For that we know that $\mu$ is a left adjoint so it preserves left Kan extensions, so $\mu X \circ DdX = \mu X \circ \mathrm{Lan}_{dX}(d\mathcal{D}X \circ dX) = \mathrm{Lan}_{dX}(\mu X \circ DdX \circ dX) = \mathrm{Lan}_{dX}(\mathrm{id}_{\mathcal{D}X} \circ d) = \mathrm{Lan}_{dX}dX = \mathrm{id}_{\mathcal{D}X}$

$$
\begin{tikzcd}[column sep=2.8em, row sep=2.8em]
    \mathcal{D}X \arrow[r, "\mathcal{D}dX"] \arrow[d, "dX"'] & \mathcal{D}\mathcal{D}X \arrow[r, "\mu"] \arrow[d, "d_{\mathcal{D}X}"'] & \mathcal{D}X \arrow[d, "\mathrm{id}_{\mathcal{D}X}"'] \\
    X \arrow[r, "dX"'] & \mathcal{D}X \arrow[u, "\mathrm{id}_{\mathcal{D}X}"]
\end{tikzcd}
\qquad (7)
$$
Similarly, $\nu \circ \mathcal{U}u = \mathrm{id}_{\mathcal{U}}$, so $\mathcal{U}$ is a co-KZ-doctrine. Thus we have proved

**Proposition 13.** ($\mathcal{D}$, $d$, $\mu$) is a KZ-doctrine and ($\mathcal{U}$, $u$, $\nu$) is a co-KZ doctrine.

## 3.2 Distributive laws and equivalence of $\mathcal{D}\mathcal{U}$ with $[-, \Omega]$, $\Omega$

In the previous section we constructed two monads, but in order for their
composite to be a monad, one needs a distributive law between them.

Verifying that a natural transformation is indeed a distributive law may not be
easy, but, thanks to [13], for KZ-doctrines, we just have to check the conditions
of Proposition 10. To construct $\mathcal{D}$ and $\mathcal{U}$, we have used Kan extensions, thus
it make sense that a distributive law between them is a Kan extension as well.
Looking at the diamond above and as both $u\mathcal{D}$ and $\mathcal{U}d$ are fully faithful, a Kan
extension along any of them would make that triangle commute, so intuitively, it
should make no difference from which triangle one starts. So if one calculates all
four Kan extensions one obtains

1. $r_{\mathcal{D}}^r = \mathrm{Ran}_{u\mathcal{D}} \mathcal{D}u = \mathcal{U}\mathcal{D}(\mathcal{D}u, -)$

2. $r_{\mathcal{U}}^l = \mathrm{Lan}_{\mathcal{U}d} d\mathcal{U} = \mathcal{U}\mathcal{D}(\mathcal{U}d, -)$

3. $r_{\mathcal{D}}^l = \mathrm{Lan}_{u\mathcal{D}} \mathcal{D}u = \mathcal{U}\mathcal{D}(d\mathcal{D} \circ d, -) * d\mathcal{U} \circ u$

4. $r_{\mathcal{U}}^r = \mathrm{Ran}_{\mathcal{U}d} d\mathcal{U} = \{\mathcal{U}\mathcal{D}(-, \mathcal{U}d), d\mathcal{U}\}$

Now as for any $X$ and any $\varphi \in \mathcal{D}X$ and any $\psi \in \mathcal{U}X$ one has $\mathcal{D}uX(\varphi)(\psi) = \mathcal{U}dX(\varphi)(\psi)$ it follows $\mathrm{Ran}_{u\mathcal{D}} \mathcal{D}u = \mathrm{Lan}_{\mathcal{U}d} d\mathcal{U}$.

**Proposition 14.** *The natural transformation $r = \mathrm{Ran}_{u\mathcal{D}} \mathcal{D}u = \mathrm{Lan}_{\mathcal{U}d} d\mathcal{U} : \mathcal{U}\mathcal{D} \to \mathcal{D}\mathcal{U}$ is a distributive law between $\mathcal{D}$ and $\mathcal{U}$.*

In a similar way one has a distributive law $l = \mathrm{Ran}_{\mathcal{D}u} u\mathcal{D} = \mathrm{Lan}_{d\mathcal{U}} \mathcal{U}d : \mathcal{D}\mathcal{U} \to \mathcal{U}\mathcal{D}$, given by $l = \mathcal{D}\mathcal{U}(-, \mathcal{D}u)$.

**Proposition 15.** *With the notations from above we have $l \vdash r$.*

Next, we state that the monad $\mathcal{D}\mathcal{U}$ is equivalent to the double dualisation monad $\mathcal{D}U$, a result due to [13] and generalised in [19].

**Theorem 16.** For a commutative quantale $\Omega$, the composite monad $\mathcal{D}\mathcal{U}$ is equivalent to the monad generated by the adjunction $[-, \Omega] \dashv [-, \Omega] : \Omega$-Cat$^{\mathrm{op}}$.

## 3.3 CCD: complete and completely distributive algebras

In this section we discuss the algebras of the two monads defined above. As $\mathcal{D}$ is a KZ-doctrine, following [8], a $\mathcal{D}$-algebra $A$ is a tuple $A = (A, \alpha)$ such that $\alpha : \mathcal{D}A \to A$ is a left adjoint to $d_A$, and since $\mathcal{U}$ is a co-KZ-doctrine a $\mathcal{U}$-algebra $B$ is a tuple $B = (B, \beta)$ such that $\beta : \mathcal{U}B \to B$ is a right adjoint to $u_B$.

**Proposition 17.** The carrier $A$ of a $\mathcal{D}$-algebra $A = (A, \alpha_A)$ is co-complete, and the carrier $C$ of an $\mathcal{U}$-algebra $C = (C, \beta_C)$ is complete. Moreover, $f : (A, \alpha_A) \to (B, \alpha_B)$ is $\mathcal{D}$-morphism if and only if $f$ preserves all weighted colimits, and it is a $\mathcal{U}$-morphism if and only if it preserves all weighted limits.
## 4.1 The left adjoint of the comparison functor

**Definition 24.** An atom in a category $\mathcal{C}$ is an object $\mathcal{C}$ such that $\mathcal{C}(\mathcal{C}, -)$ preserves all colimits. $\mathrm{At}(\mathcal{C})$ is the full subcategory of $\mathcal{C}$ whose objects are atoms.

Before we continue let us give some example of atoms.

*Example 25.*

1. In posets atoms are known as completely prime elements. In a completely distributive lattice being an atom is equivalent to being completely join irreducible.

2. The category $[0, \infty]$ seen as a generalized metric space has only one atom 0.

3. Let $[X^{\mathrm{op}}, \Omega]$ be a functor category, then using Yoneda and the definition of a colimit in a functor category, see [7, Chapter 3.3], one has that any representable is an atom. Moreover, see [7, Chapter 5.5], one has that $[X^{\mathrm{op}}, \Omega] \cong [\mathrm{At}(X)^{\mathrm{op}}, \Omega]$. In general one has $X \subseteq \mathrm{At}([X^{\mathrm{op}}, \Omega])$.

We define a functor $\mathrm{AT}: \mathcal{D}\mathcal{U}\text{-alg} \to \Omega\text{-Cat}^{\mathrm{op}}$ on objects by $\mathrm{AT}(A, \alpha) = (\mathrm{At}(A))^{\mathrm{op}}$. In order to define $\mathrm{AT}$ on maps we need some additional lemmas.

First note that for any $H: A \to B$ in $\mathcal{D}\mathcal{U}\text{-alg}$, since $A$ is complete and $H$ preserves all limits, there exists a left adjoint $L: B \to A$ in $\Omega\text{-Cat}$.

**Lemma 26.** For all $A, B \in \mathcal{A}$ and $H: A \to B$ with left adjoint $L$, there exists $f: \mathrm{At}(B) \to \mathrm{At}(A)$ such that $L \circ i_B = i_A \circ f$, where $i_A: \mathrm{At}(A) \to A$ and $i_B: \mathrm{At}(B) \to B$ are the atom-inclusion maps.

We can now define $\mathrm{AT}(H) = f^{\mathrm{op}}$ with $f$ as in the lemma. This defines a functor because composition of adjoints is again an adjoint. We are ready to prove

**Theorem 27.** For any $X \in \Omega\text{-Cat}$ and $A \in \mathcal{D}\mathcal{U}\text{-alg}$, we have a natural isomorphism of categories $\Omega\text{-Cat}(X^{\mathrm{op}}, \mathrm{At}(A))^{\mathrm{op}} \cong \mathcal{D}\mathcal{U}\text{-alg}(A, [X, \Omega])$. Moreover this is isomorphism also an isomorphism of $\Omega$-categories.

*Proof.* We sketch the construction of the isomorphism. We have to define the functors

$$ \phi_{XA}: \Omega\text{-Cat}(X^{\mathrm{op}}, \mathrm{At}(A))^{\mathrm{op}} \to \mathcal{D}\mathcal{U}\text{-alg}(A, [X, \Omega]), $$

$$ \psi_{XA}: \mathcal{D}\mathcal{U}\text{-alg}(A, [X, \Omega]) \to \Omega\text{-Cat}(X^{\mathrm{op}}, \mathrm{At}(A))^{\mathrm{op}} $$

and show that they are inverse to each other. First define $\phi_{XA}$ on objects. For all $h: X^{\mathrm{op}} \to \mathrm{At}(A)$ let

$$ \phi_{XA}(h) = A(h-, -): A \to [X, \Omega]. $$

Now define $\psi_{XA}$ on objects. Let $H: A \to [X, \Omega]$ and let $L: [X, \Omega] \to A$ be its left adjoint, and also let $uX: X^{\mathrm{op}} \to [X, \Omega]$, $x \mapsto X(x, -)$ the Yoneda embedding.
<figure><img src="image_5.png" /></figure>

Since $L \circ uX(x)$ is an atom for all $x$ in $X$, we let $\psi_{XA}(H) = L \circ uX$. In order to define $\phi_{XA}$ and $\psi_{XA}$ on arrows, one uses the concept of conjugate natural transformation [11, Chapter 4.7].

**Theorem 28.** The functor $\mathbf{AT}: \mathcal{D}\mathcal{U}\text{-alg} \to \Omega\text{-Cat}^{\text{op}}$ is a left adjoint to the functor $K: \Omega\text{-Cat}^{\text{op}} \to \mathcal{D}\mathcal{U}\text{-alg}$.

*Proof.* Let $X \in \Omega\text{-Cat}$ and $A \in \mathcal{D}\mathcal{U}\text{-alg}$. We have to show that $\Omega\text{-Cat}^{\text{op}}(\mathbf{AT}(A), X) \cong \mathcal{D}\mathcal{U}\text{-alg}(A, KX)$ which is equivalent to $\Omega\text{-Cat}(X, \text{At}(A)^{\text{op}}) \cong \mathcal{D}\mathcal{U}\text{-alg}(A, [X, \Omega])$, and as $\Omega\text{-Cat}(X, \text{At}(A)^{\text{op}}) \cong \Omega\text{-Cat}(X^{\text{op}}, \text{At}(A))^{\text{op}}$, see [7, 2.28], we have to prove that there is a natural isomorphism between

$$ \Omega\text{-Cat}(X^{\text{op}}, \text{At}(A))^{\text{op}} \cong \mathcal{D}\mathcal{U}\text{-alg}(A, [X, \Omega]), $$

which is Theorem 27.

After having constructed a left adjoint $\mathbf{AT}$ of $K$, we next ask when $\Omega\text{-Cat}^{\text{op}}$ is a full reflective subcategory of $\mathcal{D}\mathcal{U}\text{-alg}$, that is, we ask when $K$ is fully faithful. We also want to characterise the image of $K$ and describe the subcategories of $\Omega\text{-Cat}^{\text{op}}$ and $\mathcal{D}\mathcal{U}\text{-alg}$ on which the adjunction restricts to an equivalence.

## 4.2 A fully faithfulness of the comparison and its image

In the case of $\Omega = 2$ the comparison $K$ is fully faithful, but this is not true for all commutative quantales $\Omega$. In this subsection, we give necessary and sufficient conditions for $K$ to be fully faithful and describe its image.

Using Proposition 3 we notice that $K$ is faithful on $\Omega\text{-Cat}^{\text{op}}(X, Y)$ if and only if $X$ is anti-symmetric. Indeed, if $X$ is not anti-symmetric let $g_1, g_2: Y \to X$ be two distinct equivalent maps. Then as $\Omega$ is we have that $Kg_1 = Kg_2$.

For $K$ to be full we need that for any two categories $X, Y \in \Omega\text{-Cat}$ and every map $H: KX \to KY$ there exists a map $h: Y \to X$ such that $Kh = H$. Using the adjunction, we have $K \circ \mathbf{AT}(H) = H$ so if one can make sure that $\text{At}(KX) \cong X$ and $\text{At}(KY) \cong Y$ then the functor $K$ will be full. For that we need the following definition [10,6].

**Definition 29.** We say that $X \in \Omega\text{-Cat}$ is Cauchy complete if $X \simeq \text{At}([X, \Omega])^{\text{op}}$. We denote by $\Omega\text{-Cat}_{cc}$ the full subcategory of $\Omega\text{-Cat}$ spanned by the antisymmetric Cauchy complete categories.
**Remark 30.** 1. Let $\Omega = [0, \infty]$ and let $Q$ and $R$ be the rational and real numbers, respectively, with the usual Euclidean metric. Then the map in $H: [Q, \Omega] \to [R, \Omega]$ given by $H(f)(r) = \lim_n f(q_n)$ where $(q_n)$ is a Cauchy sequence with limit $r$, is in $\mathcal{D}U$-alg and cannot be restricted to a map $\text{At}(H) : R \to Q$. So $K$ is not full in general.

2. Any poset is Cauchy complete, see [16].

3. As shown in [10], a generalised metric space $X$ is isomorphic to $\text{At}([X^{\text{op}}, \Omega])$ if it is Cauchy complete in the usual sense of metric spaces.

**Theorem 31.** *The comparison functor for the adjunction $[-, \Omega] \dashv [-, \Omega] : \Omega\text{-Cat} \to \Omega\text{-Cat}_{cc}^{\text{op}}$ is full and faithful.*

This result is conceptually important to us. When we started out from the basic picture (3), we were guided by the example $\Omega = 2$, in which $\Omega$-Cat$_{cc} = \Omega$-Cat. Therefore we could as well have chosen $\Omega$-Cat$_{cc}^{\text{op}}$ instead of $\Omega$-Cat$^{\text{op}}$ in (3). From this point of view, the theorem confirms that we are free to consider $K$ in (3) to be fully faithful.

To characterise the image of $K$, we use the description of full reflective subcategories by orthogonality, see [3, Chapter 5.4]. First we need again some definitions.

**Definition 32.** A functor $F : A \to C$ is called dense if $c = C(F-, c) * F$ for all $c \in C$.

For more equivalent descriptions of dense functors see [7, Chapter 5].

**Definition 33.** A category $A$ is called atomic if the atom-inclusion functor $i_A : \text{At}(A) \to A$ is dense.

Let us give some example of atomic categories.

*Example 34.* 1. Any finite distributive lattice is atomic.

2. Any presheaf category is atomic as every functor is a colimit of representables

3. The category $[0, \infty]$ is atomic if seen as a generalised metric space but not if seen as a poset.

We will need the following property of dense functors.

**Lemma 35.** If $A$ is cocomplete and the atom-inclusion functor $i_A : \text{At}(A) \to A$ is dense then $A \cong [\text{At}(A)^{\text{op}}, \Omega]$.

*Proof.* Let $A \in \mathcal{A}$ such that $i : \text{At}(A) \to A$ is dense. According to [7, Theorem 5.1] if $i$ is dense then $\tilde{i} : A \to [\text{At}(A)^{\text{op}}, \Omega]$, defined by $\tilde{ia} = A(i-, a)$, is fully faithful. So we just have to show that it is essentially surjective. Let $H : \text{At}(A)^{\text{op}} \to \Omega$, as $A$ is cocomplete $H * i$ exists, then $\tilde{i}(H * i) \cong H * \tilde{ii} \cong H * d\text{At}(A) \cong H$ thus $\tilde{i}$ is essentially surjective and so $A \cong [\text{At}(A)^{\text{op}}, \Omega]$.

**Theorem 36.** An algebra $A$ in $\mathcal{D}U$-alg is isomorphic to an algebra in the image of $K$ if and only if it is atomic.
*Proof.* We shall use orthogonality [3, Chapter 5.4]. First let us take $X$ in $\Omega$-Cat$^{\text{op}}$ and show that it is atomic. Let us denote by $\theta: \mathrm{id} \to K\mathrm{A}\mathrm{T}$ the unit of the adjunction $\mathrm{A}\mathrm{T} \to K$. From orthogonality we obtain that for every $B \in \mathcal{D}\mathrm{U}\text{-alg}$ and any $f: B \to X$ we have a unique factorisation through $\theta_B$, so let us take $B = X$ and $f = \mathrm{id}_X$. There exists $g: [\mathrm{At}^{\text{op}}(X), \Omega] \to X$ such that $g$ preserves limits and colimits and such that $g \circ \theta_X = \mathrm{id}_X$. Thus, for every $x \in X$ one has

$$g(\theta_X(x)) = x.$$

Now $\theta_X(x) = X(-, x) : \mathrm{At}^{\text{op}}(X) \to \Omega$ and as every presheaf is a colimit of representables one has

$$X(-, x) = X(-, x) * d_{\mathrm{At}(X)}.$$

Thus one also has

$$
\begin{align*}
x &= g(X(-, x)) = g(X(-, x) * d_{\mathrm{At}(X)}) \\
&= g\left(\int_{x' \in \mathrm{At}(X)} X(x', x) \otimes \mathrm{At}(X)(-, x')\right) = \int_{x' \in \mathrm{At}(X)} X(x', x) \otimes g(\mathrm{At}(X)(-, x')) \\
&= \int_{x' \in \mathrm{At}(X)} X(x', x) \otimes g(X(-, x')) = \int_{x' \in \mathrm{At}(X)} X(x', x) \otimes x') \\
&= X(i_X -, x) * i_X
\end{align*}
$$

So, in conclusion, $X$ is atomic as $i_X : \mathrm{At}(X) \to X$ is dense. The converse follows from Lemma 35 because $X \cong [\mathrm{At}^{\text{op}}(X), \Omega] = \mathcal{D}(\mathrm{At}(X))$ which is ccd.

*Remark 37.* In the case $\Omega = \mathbb{2}$, we have $^{\text{op}}\mathrm{CCD} = \mathrm{CCD}$ (since the dual of a completely distributive lattice is a completely distributive lattice). But this is not true for general $\Omega$. Using results from [4] and reproving them for the enriched case we can show that the categories of $\mathcal{D}\mathrm{U}$-algebras and $\mathcal{U}\mathcal{D}$-algebras are isomorphic if $\Omega \cong \Omega^{\text{op}}$ in $\Omega$-Cat.

# 5 Algebras for operations and equations

We will show that the categories of algebras for the monads $\mathcal{D}$, $\mathcal{U}$, and $\mathcal{D}\mathrm{U}$ are isomorphic to categories of algebras given by operations and equations over Set.

## 5.1 Syntactic $\mathcal{D}$-algebras and $\mathcal{U}$-algebras

**Definition 38.** By a $(\Sigma_D, E_D)$-algebra we understand a set $A$ together with a family of unary operations $(v \star -)_{v \in \Omega}: A \to A$ indexed by $\Omega$, and a family of operations $\sqcup_K: A^K \to A$, where $K$ ranges over all sets, satisfying the following $\mathfrak{7}$ axioms. Dually the notions of a $(\Sigma_U, E_U)$-algebra is given by a set $B$ together with a family of unary operations $(v \triangleright -)_{v \in \Omega}: B \to B$ and for each set $K$ an operation $\sqcap_K: B^K \to B$ satisfying the following $\mathfrak{7}$ axioms.
1. $e \star - = \mathrm{id}_A$

$e \triangleright - = \mathrm{id}_A$

2. For all $a \in A$, $b \in B$ and $v, w \in \Omega$

$$v \star (w \star a) = (v \otimes w) \star a$$

$$v \triangleright (w \triangleright b) = (v \otimes w) \triangleright b$$

3. For all $v \in \Omega$ and $a_k \in [K, A]$, $b_k \in [K, B]$

$$v \star \bigsqcup_K a_k = \bigsqcup_K (v \star a_k)$$

$$v \triangleright \bigsqcup_K b_k = \bigsqcup_K (v \triangleright b_k)$$

4. For all $a \in A$, $b \in B$ and $v_k \in [K, \Omega]$

$$(\int^K v_k) \star a = \bigsqcup_K (v_K \star a)$$

$$(\int^K v_k) \triangleright b = \bigsqcup_K (v_K \triangleright b)$$

5. For a set $K$ and function $J: K \to \text{Set}$ let us denote with $\bar{J} = \bigsqcup_{k \in K} J_k$. For each $k \in K$ let $a_k: J(k) \to A$ and let $a: \bar{J} \to A$ be the map induced by the coproduct. For each $k \in K$ let $b_k: J(k) \to B$ and let $b: \bar{J} \to B$ be the map induced by the coproduct.

$$\bigsqcup_K (\bigsqcup_{J_k} a_k) = \bigsqcup_{\bar{J}} a$$

$$\bigsqcup_K (\bigsqcup_{J_k} b_k) = \bigsqcup_{\bar{J}} b$$

6. Let $\Delta$ be the diagonal functor then for any set $K$ and for all $a \in A$ and $b \in B$ we have

$$\bigsqcup_K \Delta a = a$$

$$\bigsqcup_K \Delta b = b$$

7. For any two sets $J, K$ and any bijective function $f: J \to K$ one has

$$\bigsqcup_J \circ A^f = \bigsqcup_K$$

$$\bigsqcup_J \circ A^f = \bigsqcup_K$$

Before we continue let us fix some notations and give some examples. If the set $K$ is 2 then we put $\bigsqcup_K = \sqcup$ and $\bigsqcup_K = \sqcap$ and use infix notation. For any set $K$ by an element $a_K$ of $A^K$ we understand any function $a_K: K \to A$. If $K$ is finite $a_K$ can be represented as a tuple $a_K = (a_1, a_2, ..., a_k)$ where $k = |K|$.

**Example 39.** 1. For any quantale $\Omega$, the $\Omega$-category $\Omega$ is a $\langle \Sigma_D, E_D \rangle$-algebra, with $\sqcup$ given by $\vee$ and $v \star -$ given by $v \otimes -$. The fact that this satisfies all the axioms is trivial. In a similar way $\Omega$ is also a $\langle \Sigma_U, E_U \rangle$-algebra with $\sqcap$ given by $\wedge$ and $v \triangleright -$ given by $\Omega(v, -)$.

2. Any cocomplete $\Omega$-category $A$ is a $\langle \Sigma_D, E_D \rangle$-algebra. For any $v \in \Omega$ and $a \in A$ we define $v \star a$ as the colimit of $a$ weighted by $v$. And for every set $K$ and any $a_K \in A^K$ we define $\bigsqcup_K a_K$ as the colimit of $a_K$ weighted by constant $\Omega$-functor $e_K: K \to \Omega$ given by $e_K(k) = e$ for all $k \in K$. That is equivalent to saying that $\bigsqcup_K$ is a coend.

3. Any complete $\Omega$-category $A$ is a $\langle \Sigma_U, E_U \rangle$-algebra

4. For any quantale $\Omega$ and any $\Omega$-category $X$ the functor category $[X, \Omega]$ is a $\langle \Sigma_D, E_D \rangle$-algebra and the functor category $[X, \Omega]^{\mathrm{op}}$ is a $\langle \Sigma_U, E_U \rangle$-algebra. If $\Omega \cong \Omega^{\mathrm{op}}$ then any functor category is both a $\langle \Sigma_D, E_D \rangle$ and a $\langle \Sigma_U, E_U \rangle$-algebra.
As any $\langle \Sigma_D, E_D \rangle$-algebra $A$ has a preorder structure on it, given by $a \le b \Leftrightarrow a \sqcup b = b$. We now show that $A$ also carries a $\Omega$-category structure.

**Proposition 40.** Any $\langle \Sigma_D, E_D \rangle$-algebra $A$ has a $\Omega$-category structure given by

$$A(a, b) = \bigvee \{v \in \Omega \mid (v \star a) \leq b\}, \qquad (10)$$

for all $a, b \in A$. Also any $\langle \Sigma_U, E_U \rangle$-algebra $B$ has a $\Omega$-category structure given by

$$B(b, b') = \bigvee \{v \in \Omega \mid b \le (v \triangleright b')\}, \qquad (11)$$

for all $b, b' \in B$.

One could ask why we do not define $A(a, b)$ as that $v \in \Omega$ such that $v \star a = b$, and the answer is because $\star$ is not injective in general. For example, take $\Omega = [0, \infty]$ and note that $w \star \infty = \infty$ for all $w \in \Omega$, thus there is no unique $w \in \Omega$ to define $[0, \infty)(\infty, \infty)$.

**Example 41.** Let us look at $\Omega = ([0, \infty] \ge), 0, +)$. Define $v \star a = v + a$ and $\sqcup_K(v_1, \dots, v_k) = \inf_R(v_1, \dots, v_k)$, thus $\Omega$ is a $\langle \Sigma_D, E_D \rangle$-algebra. Let us check that the $\Omega$-category structure given by Proposition 40 is the usual one. Let $a, b \in [0, \infty]$, then one has

$$\{v \in \Omega \mid v + a \ge b\} = \{v \in \Omega \mid v \ge b - a\}$$

Now obviously $[0, \infty](a, b) = b - a = \inf\{v \in \Omega \mid v \ge b - a\} = \bigvee\{v \in \Omega \mid v \ge b - a\}$. Also let us note that $\bigwedge\{v \in \Omega \mid v \ge b - a\} = \infty$.

One has two equivalent definitions of a semi-lattice, one using operations and equations, and one saying that a semi-lattice is a complete/cocomplete poset. The $\Omega$-Cat analogue is as follows.

**Theorem 42.** Let $A$ be a $\langle \Sigma_D, E_D \rangle$-algebra and $B$ a $\langle \Sigma_U, E_U \rangle$-algebra.

1. For any $v \in \Omega$ and $a, b \in A$ we have $A(v \star a, b) = \Omega(v, A(a, b))$. Thus $v \star a$ is the colimit of a weighted by $v$.

2. The operation $\sqcup_K$ is a coend, in the sense that for any set $K$ one has $A(\sqcup_K a_k, b) = \int_{k \in K} A(a_k, b)$.

3. For any $v \in \Omega$ and $a, b \in B$ we have $B(a, v \triangleright b) = \Omega(v, A(a, b))$. Thus $v \triangleright b$ is the limit of $b$ weighted by $v$.

4. The operation $\sqcap_K$ is an end, in the sense that for any set $K$ one has $B(a, \sqcap_K b_k) = \int_{k \in K} B(a, b_k)$.

Thus any $\langle \Sigma_D, E_D \rangle$-algebra is co-complete as a $\Omega$-category, and any $\langle \Sigma_U, E_U \rangle$-algebra is complete as a $\Omega$-category.
4. for any set $K$ and any functions $\varphi: K \to \Omega$ and $G: K \times A \to \Omega$

$$ \bigcap_K \varphi(k) \triangleright \left( \bigcup_A G(k)(a) \star a \right) = \bigcup_A \{ \varphi, \downarrow G(-, a) \} \star a, \quad (13) $$

where $\{\varphi, \downarrow G(-, a)\}$ is a limit computed in $\Omega$ with $\downarrow G(k) : A^{\text{op}} \to \Omega$ given by $\downarrow G(k) = \text{Lan}_i G = \int^{b \in A} A(-, i(b)) \otimes G(k)(b)$ for $i : |A| \to A^{\text{op}}$ the object inclusion functor.

**Remark 48.** 1. As we will see below a $\langle \Sigma_{\mathcal{D}U}, E_{\mathcal{D}U} \rangle$-algebra $A$ can be translated into a $\mathcal{D}U$-algebras $(A, \alpha, \beta)$. Under this translation, Axiom (13) becomes

$$ \{\varphi, \alpha \circ \downarrow G\} = \alpha(\{\varphi, \downarrow G\}) $$

stating that $\alpha$ preserves limits.

2. In the case that $\varphi$ and $G$ are crisp, that is, they take values in $\{\perp, e\} \subseteq \Omega$, we can identify $K$ with the extension of $\varphi$ and $G(k)$ with subsets of $A$ so that Axiom (13) becomes

$$ \bigcap \{ \bigcup G(k) \mid k \in K \} = \bigcup \bigcap \{ \downarrow G(k) \mid k \in K \} $$

Note that this coincides with the specialisation of Axiom (13) to the case $\Omega = 2$. It expresses that joins perserve meets. As observed in [4] this is equivalent (under the axiom of choice) to the usual distributive law using choice functions. Choice functions allow us to replace the intersection $\bigcap \{\downarrow G(k) \mid k \in K\}$, which is a meet in $\mathcal{D}A$, by a collection of meets in $A$. Moreover, in case that $K$ and the $G(k)$ are finite, the join $\bigcup \bigcap \{\downarrow G(k) \mid k \in K\}$ can be replaced by a join indexed over *finitely* many choice functions, even if $A$ is infinite. Under what circumstances the distributive law (13) can be restricted to a finite one is a question we do not pursue in this paper.

Now let us show that $\langle \Sigma_{\mathcal{D}U}, E_{\mathcal{D}U} \rangle$ algebras are indeed $\mathcal{D}U$-algebras.

**Theorem 49.** *The category of $\langle \Sigma_{\mathcal{D}U}, E_{\mathcal{D}U} \rangle$-algebras is isomorphic to the category of $\mathcal{D}U$-algebras.*

*Proof.* Let $(A, v\star-, \sqcup_K, v\triangleright-, \sqcap_K)$ be a $\langle \Sigma_{\mathcal{D}U}, E_{\mathcal{D}U} \rangle$ algebra. By Propositions 40 and 46, $A$ has a $\Omega$-category structure. Define $\alpha : \mathcal{D}A \to A$ and $\beta : \mathcal{U}A \to A$, by $\alpha(\varphi) = \sqcup_{|A|} \varphi(a) \star a$ and $\beta(\psi) = \sqcap_{|A|} \psi(a) \triangleright a$. Using all axioms of Definition 38 and Theorem 42 one shows that $\alpha$ is a $\mathcal{D}$-algebra and $\beta$ is a $\mathcal{U}$-algebra. Moreover, $A$ is complete and cocomplete. Axiom (13) implies that $\alpha$ preserves all limits, hence has a left adjoint and thus is *ccd*. By Theorem 22, $(A, \alpha, \beta)$ is a $\mathcal{D}U$-algebra.

For the converse, define $\star, \triangleright, \sqcup$, and $\sqcap$ as the respective (co)limits and show that *ccd* implies Axiom (13).
## 5.3 Ω-Cat-logic

For any (commutative) quantale $\Omega$, we have a propositional $\Omega$-logic given by $\langle\Sigma_{\mathcal{D}U}, E_{\mathcal{D}U}\rangle$. The language is given by

$$ \mathcal{L} : p \mid v \star - \mid v \triangleright - \mid \Box \mid \Box , $$

where $p$ are atomic propositions; $v \star -$ and $v \triangleright -$ are unary operations; $\Box$ and $\Box$ are K-ary operations for each set $K$. These operations satisfy the equations listed in Definitions 38 and 47.

The semantics of these operations wrt a $\Omega$-category $X$ is as follows. If $F_P$ is the free algebra$^3$ over atomic propositions $p \in P$, then any interpretation of the atomic propositions as many-valued upsets $X \to \Omega$ induces a morphism $\llbracket - \rrbracket : F_P \to [X, \Omega]$, which is nothing but a many-valued relation (bimodule)

$$ \Vdash : X \otimes F_P \to \Omega. $$

The values of $\Omega$ measure how well a state $x \in X$ satisfies a specification $\phi \in F_P$. We say “$x$ satisfies $\phi$ up to $r$” if $(x \Vdash \phi) = r$ and “$x$ satisfies $\phi$” if $r$ is top. The operations $\Box$ and $\Box$ are join and meet and we have

$$ \llbracket v \star \phi \rrbracket = (x \mapsto v \otimes \llbracket \phi \rrbracket(x)) \qquad \llbracket v \triangleright \phi \rrbracket = (x \mapsto [v, \llbracket \phi \rrbracket(x)]). $$

Reasoning in the $\Omega$-valued setting, we are interested in judgements

$$ \phi \vdash_r \psi $$

which are interpreted as $F_P(\phi, \psi) \geq r$, the latter being equivalent to

$$ [x \Vdash \phi, x \Vdash \psi] \geq r $$

for all $\Omega$-categories $X$ and all $x \in X$.

*Example 50.* 1. In the case of $\Omega = \mathbb{2}$ the operations $\star$ and $\triangleright$ are redundant and we obtain the equational theory of complete and completely distributive lattices. $\vdash_0$ is redundant and $\phi \vdash_1 \psi$ means $(x \Vdash \phi) \Rightarrow (x \Vdash \psi)$ for all $X$ and $x \in X$.

2. In the case of $\Omega = [0, \infty]$, we write inf for $\Box$ and sup for $\Box$ (note the reversal of the order to reflect that distance 0 is top and $\infty$ is bottom). If $x$ satisfies $\phi$, then $x$ satisfies $v \star \phi$ up to $v$. If $x$ satisfies $\phi$ up to $v$, then $x$ satisfies $v \triangleright \phi$. That $[X, \Omega]$ is atomic means that arbitrary predicates can be built from “singleton”, $v \star -$ and $\Box$. A judgement $\phi \vdash_r \psi$ means $(x \Vdash \psi) - (x \Vdash \phi) \leq_R r$ for all $X$ and $x \in X$.

<footnote>$^3$ Here we make use of the fact that due to complete distributivity free algebras exist, even though the signature has operations of unbounded arity.</footnote>
# 6 Conclusions

We have shown in Theorem 49 that for any commutative quantale $\Omega$ the category $\Omega$-Cat of $\Omega$-categories, or, in other words, the category of $\Omega$-valued generalised metric spaces, is isomorphic to a category of algebras for operations and equation in the usual sense, if we admit operations of infinite unbounded arity.

Moreover, due to the duality underlying our approach, these operations have a logical interpretation and the equations can be seen as logical axioms.

The value of Theorem 49 resides not only in its statement but even more so in how we proved it: We didn't guess $\langle \Sigma_{\mathcal{D}U}, E_{\mathcal{D}U} \rangle$ and then proved the theorem, but we derived $\langle \Sigma_{\mathcal{D}U}, E_{\mathcal{D}U} \rangle$ in a systematic fashion from the functor $[-, \Omega]$. We started from the aim to derive the logic of $\Omega$-valued predicates, that is, the logic given implicitly by the structure of the categories $[X, \Omega]$. To extract this logical structure, we considered $[X, \Omega]$ as algebras for the monad induced by $[-, \Omega]$. We then employed a result linking that monad to the 'semi-lattice' monads $\mathcal{D}$ and $\mathcal{U}$. The algebraic structure of these monads computes limits and colimits and an equational description of these was given as $\langle \Sigma_{\mathcal{D}U}, E_{\mathcal{D}U} \rangle$.

It lies in the nature of this method that the logic $\langle \Sigma_{\mathcal{D}U}, E_{\mathcal{D}U} \rangle$ we derived from $\Omega$ is not purely syntactic but still depends on $\Omega$. The operations are infinitary and the laws contain side conditions depending on $\Omega$. We can think of $\Omega$ as an oracle that we need to consult in our reasoning. Restricting to particular, syntactically given $\Omega$ and then describing $\langle \Sigma_{\mathcal{D}U}, E_{\mathcal{D}U} \rangle$ fully syntactically, so that consulting the oracle can be replaced by asking an automated theorem prover, is a task of future research.

In future work, finitary versions of the $\langle \Sigma_{\mathcal{D}U}, E_{\mathcal{D}U} \rangle$ will be investigated. Extension with tensor and implication will also be of interest. These should be linked with the theory of MV-algebras. Properties of $\langle \Sigma_{\mathcal{D}U}, E_{\mathcal{D}U} \rangle$ and their finitary versions should be linked with properties of $\Omega$. Moerover, it needs to be investigated how to integrate the propositional $\Omega$-logics with the modalities arising from coalgebraic type functors.

# References

1. J. Beck. Distributive laws. In B. Eckmann, editor, *Seminar on Triples and Categorical Homology Theory*, volume 80 of *Lecture Notes in Mathematics*, pages 119–140. Springer Berlin Heidelberg, 1969.

2. M. Bílková, A. Kurz, D. Petrisan, and J. Velebil. Relation lifting, with an application to the many-valued cover modality. *Logical Methods in Computer Science*, 9(4), 2013.

3. F. Borceaux. *Handbook of Categorical Algebra 1*, volume 1. Cambridge University Press, 1994.

4. B. W. Fawcett and R. J. Wood. Constructive complete distributivity i. *Mathematical Proceedings of the Cambridge Philosophical Society*, 1990.

5. D. Hofmann. Duality for distributive space, 2010. arXiv:1009.3892v1.
6. G. M. Kelly and V. Schmitt. Notes on enriched categories with colimits of some class. *Theory Appl. Categ.*

7. M. Kelly. *Basic Concepts of Enriched Category Theory*.

8. A. Kock. Monads for which structures are adjoint to units. *Journal of Pure and Applied Algebra*, 104(1):41–59, 1995.

9. H. Lai and D. Zhang. Many-Valued Complete Distributivity. 2006.

10. F. Lawvere. Metric spaces, generalized logic and closed categories. *Rendiconti del Seminario Matematico e Fisico di Milano*, XLIII, 1973. Republished in *Reprints in Theory Appl. Categ.*

11. S. Mac Lane. *Categories for the Working Mathematician*. Springer, 1971.

12. F. Marmolejo. Doctrines whose structure forms a fully faithful adjoint string. *Theory Appl. Categ*, 3:24–44, 1997.

13. F. Marmolejo, R. Rosebrugh, and R. J. Wood. A basic distributive law. *Journal of Pure and Applied Algebra*, 168(2):209–226, 2002.

14. Q. Pu and D. Zhang. Categories Enriched Over a Quantaloid: Algebras. *Theory and Applications of Categories*, 2015.

15. K. I. Rosenthal. *Quantales and their applications*, volume 234 of *Pitman Research Notes in Mathematics Series*. Longman Scientific & Technical, Harlow, 1990.

16. G. Rosolini. A note on cauchy completeness for preorders.

17. J. J. M. M. Rutten. Elements of generalized ultrametric domain theory. *Theor. Comput. Sci.*, 170(1-2):349–381, 1996.

18. J. J. M. M. Rutten. Relators and metric bisimulations (extended abstract). In *CMCS'98*, volume 11, 1998.

19. I. Stubbe. The double power monad is the composite power monad. Technical report, LMPA, Université du Littoral-Côte d'Opale, Sept. 2013.

20. S. Vickers. The double powerlocale and exponentiation: A case study in geometric reasoning. *Theory and Applications of Categories*, 12:372–422, 2004.

21. S. Vickers. Localic completion of generalized metric spaces I. *Theory and Applications of Categories*, 14:328–356, 2005.

22. S. Vickers. Localic completion of generalized metric spaces II: Powerlocales. *Journal of Logic and Analysis*, 1(11):1–48, 2009.

23. S. Vickers and C. Townsend. A universal characterization of the double powerlocale. *Theoretical Computer Science*, 316:297–321, 2004.

24. J. Worrell. Coinduction for recursive data types: partial order, metric spaces and Omega-categories. In *CMCS'00*, volume 33 of *ENTCS*, 2000.