Regular and relational categories: Revisiting ‘Cartesian bicategories I’ — Brendan Fong & David I Spivak (2019). arXiv:1909.00069 (v1, PDF).
Gives a direct axiomatisation of bicategories of relations — relational po-categories — and proves that the 2-category of regular categories is equivalent to that of relational po-categories. Regular logic () is the internal logic of regular categories and exactly the logic needed to compose binary relations; the paper emphasises the graphical calculus throughout.
Sources: the paper, arXiv:1909.00069v1, checked against the arXiv listing. Index: Papers.
Key definitions and results
- Definitions 2.1, 2.6: po-categories and po-props
- Definition 3.3: regular category
- Definitions 4.10, 4.14, 4.15: prerelational po-category, tabulation, relational po-category
- Theorem 5.9: the 2-functor
- Theorem 6.25: the 2-functor back
- Theorem 7.3: the two form an equivalence of 2-categories
- Definitions 8.1, 8.4, 8.6–8.7: Carboni–Walters bicategories of relations, functional completeness, unital tabular allegories
Concept notes
Cartesian Bicategory, Conjunctive Query