License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.FSCD.2023.25
URN: urn:nbn:de:0030-drops-180090
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2023/18009/
Go to the corresponding LIPIcs Volume Portal

Dagnino, Francesco ; Pasquali, Fabio

Quotients and Extensionality in Relational Doctrines

pdf-format:
LIPIcs-FSCD-2023-25.pdf (1.0 MB)

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. 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.

BibTeX - Entry

@InProceedings{dagnino_et_al:LIPIcs.FSCD.2023.25,
  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 =		{https://drops.dagstuhl.de/opus/volltexte/2023/18009},
  URN =		{urn:nbn:de:0030-drops-180090},
  doi =		{10.4230/LIPIcs.FSCD.2023.25},
  annote =	{Keywords: Quantitative Reasoning, Calculus of Relations, Hyperdoctrines, Metric Spaces}
}

Keywords: Quantitative Reasoning, Calculus of Relations, Hyperdoctrines, Metric Spaces
Collection: 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)
Issue Date: 2023
Date of publication: 28.06.2023

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI