Regular and relational categories: Revisiting 'Cartesian bicategories I'

TL;DR

This paper provides a direct axiomatization of bicategories of relations called relational po-categories and proves their equivalence to regular categories, emphasizing their graphical nature.

Contribution

It introduces relational po-categories as a new axiomatization and establishes their equivalence with regular categories, clarifying the structure of bicategories of relations.

Findings

Relational po-categories are explicitly axiomatized.

The 2-category of regular categories is shown to be equivalent to that of relational po-categories.

Graphical representation of relational po-categories is emphasized.

Abstract

Regular logic is the fragment of first order logic generated by $=$, $\top$, $\wedge$, and $\exists$. A key feature of this logic is that it is the minimal fragment required to express composition of binary relations; another is that it is the internal logic of regular categories. The link between these two facts is that in any regular category, one may construct a notion of binary relation using jointly-monic spans; this results in what is known as the bicategory of relations of the regular category. In this paper we provide a direct axiomatization of bicategories of relations, which we term relational po-categories, reinterpreting the earlier work of Carboni and Walters along these lines. Our main contribution is an explicit proof that the 2-category of regular categories is equivalent to that of relational po-categories. Throughout, we emphasize the graphical nature of relational po-categories.