# WR: Internal Metric Spaces

We recently reviewed the notion of [internal order](https://hackmd.io/@alexhkurz/H1mRJ1Mxw).

In this note we propose to generalise to internal enriched categories using the notion of relation presheaves.

## Questions

Any suggestions for interesting examples of internal metric spaces?

Is there a nice string diagrammatic calculus in terms of cartesian bicategories, with relations labelled by "epsilons"?

Could there be a use for relational presheaves taking values in monotone relations instead of in ordinary relations?

## Notation and Preliminaries

Relational presheaves are from Rosenthal "The theory of quantaloids" (1996) but I use our own summary in [Extending set functors to generalised metric spaces](https://lmcs.episciences.org/5132/pdf) to recall this notion below.

## Relational Presheaves

Let $\Omega$ be a unital quantale in general or the [Lawvere real numbers](https://raw.githubusercontent.com/mattearnshaw/lawvere/master/pdfs/1973-metric-spaces-generalized-logic-closed-categories.pdf) in particular.

Consider $\Omega$ as a one-object order-enriched category. A **relational presheaf** is a functor
$$X:\Omega^{coop}\to Rel(Set)$$

satisfying

\begin{gather}
Id \subseteq X_e \\
X_r\cdot X_s \subseteq X_{r\otimes s}\\
X_{\bigvee r_i} = \bigcap X_{r_i}
\end{gather}

**Example:** If we take for $\Omega$ the Lawvere real numbers $[0,\infty]$ then a relational presheaf describes a Lawvere metric space where $X_r$ is the set of points at most $r$ apart.

**Theorem:** The category of relational presheaves is equivalent to the category of $\Omega$-categories.

*Proof:* (Sketch). Given an $\Omega$-category $X$, one defines $X_r=\{(x,x') \mid X(x,x')\ge r\}$. Conversely, the functor $X$ selects a set, also denoted by $X$, as the image of the one object and the hom-objects are defined as $X(x,x')= \bigvee\{r \mid (x,x')\in X_r\}$.

**Remark:** In the interpretation of $\Omega$-categories as metric spaces the order is reversed so that $X_r=\{(x,x') \mid X(x,x')\ge r\}$ is the set of all points at distance $\le r$.

## Internal $\Omega$-categories

What happens if we replace in
$$X:\Omega^{coop}\to Rel(Set)$$

the category Set by other regular categories?

**Definition:** Let $\mathcal E$ be a regular category such that $|\Omega|$-sized intersections of subobjects exist. Consider $\Omega$ as a one-object order-enriched category. An internal $\Omega$-category is a locally monotone functor

$$X:\Omega^{coop}\to Rel(\mathcal E)$$

satisfying

\begin{gather}
Id \le X_e \\
X_r\cdot X_s \le X_{r\otimes s}\\
X_{\bigvee r_i} = \bigwedge X_{r_i}
\end{gather}

**Example:** Let $\Omega=2=\{\bot < \top\}$. We get two relations, but $X_\bot=X\times X$ is redundant. $X_\top$ makes the object $X$ into an internal order of $\mathcal E$. This shows that [internal orders](https://hackmd.io/@alexhkurz/H1mRJ1Mxw) are instances of this definition.

In the example above, we know that the category of internal orders with monotone maps is order-enriched. The same is also true for the category of internal orders with monotone relations.

Do analogous properties hold of internal metric spaces?

Is the category of internal $\Omega$-categories ($\Omega$-cat)-enriched?

Given $X,Y:\Omega^{coop}\to Rel(\mathcal E)$, we need to equip $Hom(X,Y)$ with the structure of an $\Omega$-category. Let $f,g:X\to Y$. We define $f(Y_r)g$ in the same way as we define $f\le g$ in the example above. Now we put

$$ Hom(X,Y)(f,g) = \bigwedge \{ r \mid f(Y_r)g\} $$

**Theorem:** The category of internal $\Omega$-categories is ($\Omega$-cat)-enriched.

*Proof:* To be checked.

Similarly, we should get:

The category of internal $\Omega$-categories and monotone relations is ($\Omega$-cat)-enriched.

## Literature to look at

Mike Shulman: [Framed bicategories and monoidal fibrations](https://arxiv.org/pdf/0706.1286.pdf), Thm 11.5, Thm 14.4, Exle 15.4.

Simon Cho on [Categorical semantics of metric spaces and continuous logic](https://arxiv.org/pdf/1901.09077.pdf)

Reichman: [Semicontinuous Real Numbers in a Topos](https://core.ac.uk/reader/82582022)

...