Adriana Balan ; Alexander Kurz ; Jiří Velebil - Extending set functors to generalised metric spaces

lmcs:4959 - Logical Methods in Computer Science, January 29, 2019, Volume 15, Issue 1 - https://doi.org/10.23638/LMCS-15(1:5)2019
Extending set functors to generalised metric spacesArticle

Authors: Adriana Balan ; Alexander Kurz ; Jiří Velebil

For a commutative quantale $\mathcal{V}$, the category $\mathcal{V}-cat$ can be perceived as a category of generalised metric spaces and non-expanding maps.
We show that any type constructor $T$ (formalised as an endofunctor on sets) can be extended in a canonical way to a type constructor $T_{\mathcal{V}}$ on $\mathcal{V}-cat$. The proof yields methods of explicitly calculating the extension in concrete examples, which cover well-known notions such as the Pompeiu-Hausdorff metric as well as new ones.
Conceptually, this allows us to to solve the same recursive domain equation $X\cong TX$ in different categories (such as sets and metric spaces) and we study how their solutions (that is, the final coalgebras) are related via change of base.
Mathematically, the heart of the matter is to show that, for any commutative quantale $\mathcal{V}$, the `discrete' functor $D:\mathsf{Set}\to \mathcal{V}-cat$ from sets to categories enriched over $\mathcal{V}$ is $\mathcal{V}-cat$-dense and has a density presentation that allows us to compute left-Kan extensions along $D$.

Comment: 57 pages; extended version of the paper presented at CALCO 2015;
accepted for publication in LMCS; Sections 2.4 and 3.3 were added


Volume: Volume 15, Issue 1
Secondary volumes: Selected Papers of the 6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015)
Published on: January 29, 2019
Accepted on: November 19, 2018
Submitted on: November 7, 2018
Keywords: Mathematics - Category Theory, Computer Science - Logic in Computer Science, 18B35, 18D20

1 Document citing this article

Consultation statistics

This page has been seen 3540 times.
This article's PDF has been downloaded 1644 times.