Search Results

Documents authored by Pasquali, Fabio

Quotients and Extensionality in Relational Doctrines

Authors: Francesco Dagnino and Fabio Pasquali

Published in: LIPIcs, Volume 260, 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)

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.

Cite as

Francesco Dagnino and Fabio Pasquali. Quotients and Extensionality in Relational Doctrines. In 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 260, pp. 25:1-25:23, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

  author =	{Dagnino, Francesco and Pasquali, Fabio},
  title =	{{Quotients and Extensionality in Relational Doctrines}},
  booktitle =	{8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)},
  pages =	{25:1--25:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-277-8},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{260},
  editor =	{Gaboardi, Marco and van Raamsdonk, Femke},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{},
  URN =		{urn:nbn:de:0030-drops-180090},
  doi =		{10.4230/LIPIcs.FSCD.2023.25},
  annote =	{Keywords: Quantitative Reasoning, Calculus of Relations, Hyperdoctrines, Metric Spaces}
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail