Lawvere's generalised the notion of complete metric space to the field of enriched categories: an enriched category is said to be Cauchy-complete if every left adjoint bimodule into it is represented by an enriched functor. Looking at this definition from a logical standpoint, regarding bimodules as an abstraction of relations and functors as an abstraction of functions, Cauchy-completeness resembles a formulation of the rule of unique choice. In this paper, we make this analogy precise, using the language of relational doctrines, a categorical tool that provides a functorial description of the calculus of relations, in the same way Lawvere's hyperdoctrines give a functorial description of predicate logic. Given a relational doctrine, we define Cauchy-complete objects as those objects of the domain category satisfying the rule of unique choice. Then, we present a universal construction that completes a relational doctrine with the rule of unique choice, that is, producing a new relational doctrine where all objects are Cauchy-complete. We also introduce relational doctrines with singleton objects and show that these have the minimal structure needed to build the reflector of the full subcategory of its domain on Cauchy-complete objects. The main result is that this reflector exists if and only if the relational doctrine has singleton objects and this happens if and only if its restriction to Cauchy-complete objects is equivalent to its completion with the rule of unique choice. We support our results with many examples, also falling outside the scope of standard doctrines, such as complete metric spaces, Banach spaces and compact Hausdorff spaces in the general context of monoidal topology, which are all shown to be Cauchy-complete objects for appropriate relational doctrines.

翻译：Lawvere将完备度量空间的概念推广至丰富范畴领域：若一个丰富范畴的每个左伴随双模均由某个丰富函子所表示，则称该范畴是柯西完备的。从逻辑视角审视这一定义，将双模视为关系的抽象化、函子视为函数的抽象化时，柯西完备性恰似唯一选择原则的一种表述。本文借助关系论这一范畴论工具精确阐释这种类比——正如Lawvere的超 doctrines为谓词逻辑提供函子化描述，关系论为关系演算提供函子化框架。给定关系论，我们将满足唯一选择原则的域范畴对象定义为柯西完备对象。随后，我们提出一种普遍构造，通过引入唯一选择原则来完成关系论，即生成所有对象均为柯西完备的新关系论。我们还引入具有单子对象的关系论，并证明这些结构构成构造其域范畴中柯西完备对象全子范畴反射子的最小必要条件。主要结论是：该反射子存在当且仅当关系论具有单子对象，且此条件等价于其在柯西完备对象上的限制与其且伴随唯一选择原则的完备化范畴等价。我们通过丰富实例支撑结论，涵盖标准论域之外的若干情形，包括幺半拓扑一般框架中的完备度量空间、巴拿赫空间与紧豪斯多夫空间——它们均被证明为对应关系论中的柯西完备对象。