The Relational Quotient Completion
Francesco Dagnino, Fabio Pasquali
TL;DR
The paper develops a unifying, categorical account of quotients that encompasses both classical and quantitative notions by using relational doctrines as a variable-free version of the calculus of relations. It introduces the intensional quotient completion to freely add quotients to any relational doctrine and an extensionality construction to enforce separation, forming the extensional quotient completion. Both constructions are shown to be (lax) 2-monadic, with universal properties captured by left biadjoints, and their interplay yields a robust framework (EQ) for modeling algebras of monads as quotients of free algebras via projective covers. The work also clarifies how relational doctrines relate to ordered categories with involution and existential elementary doctrines, establishing equivalences and illustrating how these perspectives recover classical notions like setoids, exact completions, and algebraic theories in a unified, quantitative setting.
Abstract
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.