The relational quotient completion

In this paper, we show how, by combining Lawvere's doctrines and the calculus of relations, one can unify many different mathematical contexts under the common property of having quotients for appropriate equivalence relations. We introduce relational doctrines as a functorial description of (the essential core of) the calculus of relations. We provide a universal construction to add quotients to a relational doctrine. This deals with an intensional notion of quotient, disrupting the extensional equality of morphisms. So we introduce another construction to force extensionality, which we show it abstracts several notions of separation in metric and topological structures. Composing these two constructions yields the extensional quotient completion. This extends two completions known in the literature, namely the elementary quotient completion of an existential elementary doctrine and the exact completion of a category with weak finite limits. Additionally, it recovers many quantitative examples, such as metric spaces and normed vector spaces. Finally, we compare relational doctrines to other categorical structures where one can model the calculus of relations.