Category Theory
Zulip Server
Archive

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.


Stream: deprecated: logic

Topic: 2-dimensional essentially algebraic theories


view this post on Zulip Evan Patterson (May 19 2022 at 00:10):

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?

view this post on Zulip fosco (May 19 2022 at 13:53):

pseudo-category?

view this post on Zulip Evan Patterson (May 19 2022 at 17:54):

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.

view this post on Zulip Nathanael Arkor (May 19 2022 at 18:13):

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).

view this post on Zulip Evan Patterson (May 19 2022 at 18:45):

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.

view this post on Zulip Reid Barton (May 19 2022 at 18:55):

There is Kelly's "Structures defined by finite limits in the enriched context".

view this post on Zulip Evan Patterson (May 19 2022 at 18:59):

Thanks, that looks promising!

view this post on Zulip Mike Shulman (May 19 2022 at 19:30):

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.

view this post on Zulip Evan Patterson (May 19 2022 at 22:32):

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.

view this post on Zulip Mike Shulman (May 20 2022 at 04:21):

Yes, I think that's right.

view this post on Zulip Ivan Di Liberti (May 20 2022 at 05:16):

My paper with Osmond "Bi-accessible and bipresentable 2-categories" is very relevant to the discussion.