Project of the Applied Category Theory Adjoint School 2020
Mentor: Michael Johnson
TA: Bryce Clarke
Project description
Relations have many important applications, and correspondingly the category theoretic study of relations is well-developed. Typically, relations from X to Y are defined as subobjects of the product of X and Y, and if X and Y are objects in a regular category C then we can construct a bicategory rel(C) whose morphisms are relations in C. Conversely bicategories that arise as such a rel(C) were studied in a recent ACT School which examined the seminal paper “Cartesian Bicategories I” by Carboni and Walters.
In this project we study (bi)categories of maintainable relations between categories. In this situation, the X and Y of the last paragraph, will be categories, and C will be Cat, the category of (small) categories. Cat is not a regular category, so we need to take an alternative approach to relations that uses equivalence classes of spans in C. Maintainable relations, which are instances of bidirectional transformations (cf lenses), are relations R between categories X and Y with extra structure so that if objects x of X and y of Y are R-related by a specific witness r, and if f: x –> x’ is an arrow of X, then the extra structure gives (functorially) an arrow g: y –> y’ such that x’ and y’ are again R-related, and by a specific witness r’ (cf symmetric delta lenses). Commonly in applications the relation R is called a “consistency relation” and the extra structure is called “consistency restoration” (or in lens terms, change propagation).
This is a rich area with many interesting interactions involving bicategories of spans, lenses (both symmetric and asymmetric), fibrations and generalisations of fibred category theory, as well as direct (and motivating) applications in database design and system interoperation and even machine learning. It is a mix of interesting theoretical questions and concrete applications. We will attack open questions involving exactness properties of categories of maintainable relations, we will seek to understand the interactions with classical work such as that of Carboni and Walters, and we will develop concrete examples of system interactions that are modelled by maintainable relations.
Readings
- B. Clarke, Internal lenses as functors and cofunctors (2019). http://www.cs.ox.ac.uk/ACT2019/preproceedings/Bryce%20Clarke.pdf
- B. Fong and D. Spivak, Regular and relational categories: Revisiting ‘Cartesian bicategories I’ (2019). https://arxiv.org/abs/1909.00069
- M. Johnson and B. Rosebrugh, Unifying set-based, delta-based and edit-based lenses (2016). http://ceur-ws.org/Vol-1571/paper_13.pdf
The selected readings for the presentations will be [1] and [3].