You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.
A category is to a finite limits theory (aka, an essentially algebraic theory) as a 2-category is to... what?
I want to be able to say "essentially algebraic 2-theory," but if I say that, I should know what it actually means.
Here's a more specific question, which might be better posed: if the theory of a category is a finite limits theory, then the theory of a pseudo-category is... what kind of theory?
pseudo-category?
A pseudo-category is like a category except that associativity and unitality hold only up to invertible 2-cells. You can consider pseudo-category objects in any 2-category with 2-pullbacks. The most important example seems to be pseudo-categories in Cat, which are pseudo double categories.
Evan Patterson said:
A category is to a finite limits theory (aka, an essentially algebraic theory) as a 2-category is to... what?
I want to be able to say "essentially algebraic 2-theory," but if I say that, I should know what it actually means.
Here's a more specific question, which might be better posed: if the theory of a category is a finite limits theory, then the theory of a pseudo-category is... what kind of theory?
The answer to both questions should be something like "essentially algebraic 2-theory" or "2-limit sketch", but as far as I'm aware, no such notion has been defined in the literature yet. I suspect, as with algebraic 2-theories, that one could modify the definition of essentially algebraic theory to have rewrites between terms rather than just equalities, but there would be many details (and theorems one would expect to hold) to check. The definition of 2-limit sketch is also subtle, not least because there are many kinds of 2-categorical limit one could consider (though I imagine in your case strict 2-limits would be appropriate).
Thanks Nathanael. Yes, I think for my purposes strict 2-limits are enough. I'm a bit surprised nobody has worked through this in the literature, since it's the natural setting for higher categorical structures that people use a lot, such as (non-strict) monoidal categories, (pseudo) double categories, and monoidal double categories. I suppose one could forget about the syntactical aspects and define an "essentially algebraic 2-theory" to be a strict 2-category with finite strict 2-limits.
There is Kelly's "Structures defined by finite limits in the enriched context".
Thanks, that looks promising!
Kelly's work, applied to Cat-enrichment, would give entirely strict notions. But as usual in 2-category theory, one can probably access the weak notions using the strict ones, perhaps more conveniently than by using the weak notions throughout. There appears to be a start on this in section 9 of Bourke's Accessible aspects of 2-category theory, which promises "a followup paper on two-dimensional limit theories".
There's also been older work on algebraic 2-theories, e.g. Fiore's Pseudo Limits, Biadjoints, and Pseudo Algebras. I feel like sometime in the past I heard someone give a talk about essentially algebraic 2-theories and locally presentable 2-categories, but can't remember who or when.
Thanks for that elaboration, Mike. If I understand correctly, the Cat-enriched notion of finite limits theory can give the right objects (models) but only the strict morphisms, whereas Bourke's more refined notion also gives the right morphisms, which are the pseudo morphisms.
As prior work, Bourke mentions Lack and Power's work on Lawvere 2-theories.
Yes, I think that's right.
My paper with Osmond "Bi-accessible and bipresentable 2-categories" is very relevant to the discussion.