
Last time, I explained how, given any sort of mathematical structure that can be defined using operations (with finitely many inputs) and rules about what terms are equal, we can define a Lawvere theory that encodes that data in the form of a category. But not all mathematical structures can be defined in this way, so Lawvere theories don’t cover every possible mathematical structure. Categories themselves are an example of this, and one way of seeing this is by observing that arrow composition in a category is not an operation, since any two arrows in a given category are not necessarily composable; they need to line up tip-to-tail. By contrast, we can add or multiply any two numbers, since addition and multiplication are operations.
We could call something like arrow composition, where there are restrictions on inputs, a partial operation, or more generally, a relation. So how can we encode something like the theory of categories, which involves relations, into some categorical structure, while keeping the “Lawvere theory” spirit of the thing?
Enter double Lawvere theories, an analogue of Lawvere theories which uses double categories as the setting instead of classical categories. I wrote a sort of explainer on double categories a while back, but the basic idea is that, whereas ordinary categories have a single type of arrow, double categories have two, and they are organized into squares called “cells”, where adjacent sides are different kinds of arrows, as shown below:

The idea of double Lawvere theories is that the existence of this second type of arrow, sometimes called “proarrow” (marked with a dash in the above diagram), essentially gives us enough “space” to build a Lawvere theory out of the objects and arrows, while the proarrows represent any relations that we wish to include. Equality is probably the quintessential example of such a relation since, while it is implicitly involved in classical Lawvere theories, there is no explicit piece of structure dedicated to it there.
The cells (marked α above), then, roughly amount to true implications between relations. In the case of equality, this would include things like “a=b implies b=a”.
We can also try to make use of aspects of the double category to build more complex relations out of simpler ones, and place additional requirements on the double category to be able to say even more. For example, proarrows can be composed just like arrows to get new proarrows. If we have two proarrows representing equality, we would interpret their composite as saying “there exists some b such that a=b and b=c”. And, of course, we understand this to imply that a=c, and can represent this implication by a cell.
Double Lawvere theories are still very underdeveloped as a concept. I’m hoping to help fix that through my PhD research, and ideally bring a bit more attention to them in the process. This series of posts has been my first attempt at telling their story in a way that is (hopefully) understandable, and perhaps even mildly appealing, to an audience that hasn’t spent years of their adult lives studying these things.
If you’ve found any of the ideas that I’ve talked about over these past ten months interesting, consider this your sign to investigate them further. Or better yet, take some time to contemplate them yourself, to understand them and make them your own. One of my favourite things about abstract math is that you don’t need any sophisticated equipment to be able to do it — just your mind, and maybe a pad of paper and a pen. With those three simple things, the sky’s the limit.