Cartesian double theories
This post is cross-posted at the Topos Institute blog.
Earlier this week, I arXived my paper, coauthored with Michael Lambert, titled “Cartesian double theories: A double-categorical framework for categorical doctrines” (Lambert and Patterson 2023). This paper has been in the works for so long that I was becoming anxious that it would ever be released. Needless to say, I’m glad it’s finally out there!
As the title suggests, the paper is about a new approach to doctrines. A doctrine is like a theory in logic, but categorified: it specifies categories with extra structure, analogous to how an ordinary theory specifies sets with extra structure. Doctrines, like theories, are a general idea that can be implemented in different ways. The standard approach to doctrines is based on 2-monads and their algebras (Blackwell, Kelly, and Power 1989), categorifying the story that monads and monad algebras encode algebraic structures through an abstract representation of their syntax.
My own preferred approach to universal algebra and categorical logic is the one pioneered by Lawvere, where an algebraic theory becomes a category with finite products and a model of the theory becomes a finite-product-preserving functor out of it, by default into the category \(\mathsf{Set}\) (Lawvere 1963; Crole 1993). Such functorial semantics is one of the big ideas in category theory, simple to state but with far-reaching implications. Having transformed our understanding of mathematical logic and programming language theory in the late 20th century, versions of the idea are now being used by applied category theorists to interpret models as they occur throughout science and engineering.
So it’s natural to wonder whether the story of functorial semantics can itself be categorified, giving a notion of doctrine based on two-dimensional functorial semantics. At first glance, it is surprising that there is so little work along these lines.1 One explanation for this absence is that certain obvious strategies founder due to difficulties with the theory of bicategories. If you try to define a two-dimensional functorial semantics based on lax functors into the bicategory \(\mathbf{Span}\), or normal lax functors into the bicategory \(\mathbf{Prof}\), you immediately encounter two problems. First, to incorporate cartesian products, you have to use cartesian bicategories, a notion that is already nontrivial in the locally posetal case and is quite formidable in general. Second, the well-behaved 2-cells between lax functors of bicategories are icons, which give too restrictive a notion of map between models.
If you are a regular reader of this blog, you won’t be surprised to learn that double categories provide the solution to both problems. Cartesian double categories are an elegant, usable axiomatization of double categories with finite products (Aleiferi 2018), and natural transformations between lax double functors generalize icons to give the correct notion of (strict) maps between models. In the paper, we develop a two-dimensional functorial semantics based on cartesian lax double functors into \(\mathbb{S}\mathsf{pan}\), or equivalently, cartesian unitary/normal lax double functors into \(\mathbb{P}\mathsf{rof}\). The domains of these lax functors are the titular cartesian double theories.
I hope you won’t be too put off by the length of the paper. The paper is long because we present many examples of double theories and we try to pay close attention to the details, but the main ideas should be accessible if you have some previous acquaintance with double categories. In fact, I find it remarkable that nearly all of the required concepts were already out there, ready to be employed for two-dimensional categorical logic with only a few modifications. The notion of double limit used in cartesian double categories goes back to Grandis and Paré (1999; Grandis 2019), and the modules and modulations between lax double functors that play a crucial role in our paper were also introduced by Paré (2011). This important line of work has long been underappreciated. Fortunately, that seems to be changing.
A longer introduction to cartesian double theories can be found in the paper. I also recently gave a talk about them in the Topos Institute Berkeley Seminar (slides).
I’m hoping that people will pick up these ideas, as they can doubtless be carried much further than Michael and I have taken them so far. The conclusion to the paper outlines a number of promising further directions.