Quotients and Extensionality in Relational Doctrines

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. Quotients are crucial in many constructions both in mathematics and computer science and have been widely studied using categorical tools. Among them, Lawvere’s doctrines stand out, providing a fairly simple functorial framework capable to unify many notions of quotient and related constructions. However, abstracting usual predicate logics, they cannot easily deal with quantitative settings. In this paper, we show how, combining 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.