Extending set functors to generalised metric spaces

For a commutative quantale $\mathcal{V}$, the category $\mathcal{V}-cat$ canbe 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 theextension in concrete examples, which cover well-known notions such as thePompeiu-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 westudy how their solutions (that is, the final coalgebras) are related viachange of base. Mathematically, the heart of the matter is to show that, for any commutativequantale $\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 tocompute 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 adde