Taking a quotient roughly means changing the notion of equality on a given object, set or type. In a quantitative setting, equality naturally generalises to a distance, measuring how much elements are similar instead of just stating their equivalence. Hence, quotients can be understood quantitatively as a change of distance. In this paper, we show how, combining Lawvere's doctrines and the calculus of relations, one can unify quantitative and usual quotients in a common picture. More in detail, we introduce relational doctrines as a functorial description of (the core of) the calculus of relations. Then, we define quotients and a universal construction adding them to any relational doctrine, generalising the quotient completion of existential elementary doctrine and also recovering many quantitative examples. This construction deals with an intensional notion of quotient and breaks extensional equality of morphisms. Then, we describe another construction forcing extensionality, showing how it abstracts several notions of separation in metric and topological structures. Combining these two constructions, we get the extensional quotient completion, whose essential image is characterized through the notion of projective cover. As an application, we show that, under suitable conditions, relational doctrines of algebras arise as the extensional quotient completion of free algebras. Finally, we compare relational doctrines to other categorical structures where one can model the calculus of relations.

翻译：取商大致意味着改变给定对象、集合或类型上的相等性概念。在定量设定中，相等性自然地推广为距离，用于度量元素之间的相似程度，而不仅仅是陈述它们的等价性。因此，商可以定量地理解为距离的改变。在本文中，我们展示了如何结合Lawvere学说和关系演算，将定量商与通常的商统一在一个共同的框架中。更详细地说，我们引入关系学说作为关系演算（的核心）的函子性描述。然后，我们定义了商以及一个将商添加到任何关系学说的通用构造，推广了存在性基本学说的商完备化，并同时涵盖了许多定量实例。该构造处理的是商的强内涵概念，并打破了态射的外延相等性。接着，我们描述了另一个强制外延性的构造，展示了它如何抽象度量结构和拓扑结构中的多种分离概念。结合这两个构造，我们得到了外延商完备化，其本质像通过投射覆盖的概念来刻画。作为一个应用，我们证明了在适当条件下，代数的关系学说可以作为自由代数的外延商完备化而出现。最后，我们将关系学说与其他可以建模关系演算的范畴结构进行了比较。