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: learning: questions

Topic: 2-dimensional Lawvere theories


view this post on Zulip fosco (Oct 13 2022 at 10:36):

To my surprise, there seems to be no such thing as "the analogue of a Lawvere theory, but the models interpreted in a 2-category with (say) finite products are pseudomonoids". Or rather, the precise definitions already in the literature seem to capture strict models (so, strict monoidal categories) but pseudo/lax model homomorphism (strong monoidal, or lax monoidal, functors): for example, Power's enriched Lawvere theories when the base of enrichment is Cat.

Do you have any pointer on this specific kind of 2-dimensional functorial semantics?

view this post on Zulip Nathanael Arkor (Oct 13 2022 at 14:25):

There was a project of Steve Lack and John Power on exactly this topic, but no paper has ever appeared. There are slides from a CT 2007 talk here.

view this post on Zulip Nathanael Arkor (Oct 13 2022 at 14:28):

There is also some consideration in Bourke–Gurski's The Gray tensor product via factorisation.

view this post on Zulip Nathanael Arkor (Oct 13 2022 at 14:29):

But I don't believe there's any general theory in the literature yet.

view this post on Zulip Joe Moeller (Oct 13 2022 at 15:13):

I was also surprised how little there was on this topic. I would actually really like to have such a framework available.

view this post on Zulip Mike Shulman (Oct 13 2022 at 18:16):

Strict models don't have to mean strict structures. There is a strict Cat-enriched Lawvere theory whose strict models are non-strict monoidal categories: you just put all the coherence isomorphisms into the theory. So, because strict theories are a lot easier to work with, a lot of the work on 2-dimensional universal algebra uses them, since there is no loss of generality in the kinds of structures you can describe.

view this post on Zulip fosco (Oct 13 2022 at 20:25):

Mike, I found a couple of papers by Yanofsky that make this a little bit more precise, but I must confess I still have to understand how this idea works! At first it seemed to me that he was considering only strict monoidal cats.

view this post on Zulip fosco (Oct 13 2022 at 20:27):

Given that Yanofsky was writing in 2000, I wonder if Power and Lack were aware of his work... no reference to "The syntax of coherence" appears in their talk

view this post on Zulip Nathanael Arkor (Oct 13 2022 at 20:59):

As I understand it, the point is not to capture weak models (for which, as Mike points out, strict models suffice), but to capture weak notions of morphisms, e.g. pseudo/lax/oplax, for which you genuinely do need a 2-categorical theory.

view this post on Zulip Nathanael Arkor (Oct 13 2022 at 21:00):

But I think it could be worth emailing Power and Lack to ask them about the work. I'd be interested to know too.

view this post on Zulip Nathanael Arkor (Oct 13 2022 at 21:10):

fosco said:

Given that Yanofsky was writing in 2000, I wonder if Power and Lack were aware of his work... no reference to "The syntax of coherence" appears in their talk

It's probably worth noting that Cat-enriched algebraic theories were considered by Power in 1999. (Though it goes back even further: Gray also has some papers on Cat-enriched algebraic theories, for instance.)

view this post on Zulip fosco (Oct 13 2022 at 21:38):

the upshot of this thread is then that strict, Cat-enriched 2-theories capture pseudo-structure. I see Yanofsky's paper contains all the relevant information, but there's still sometimes that flies over my head :smile: most likely, late night is the worst moment to keep doing maths

view this post on Zulip Mike Shulman (Oct 13 2022 at 23:53):

A lot more work has been done on 2D universal algebra using 2-monads rather than 2-theories. It's true that the fully strict Cat-enriched notions don't yield weak notions of morphism directly, but you can still define and characterize such morphisms using strict monads/theories. As Steve Lack wrote in his excellent 2-categories companion,

2-category theory is a “middle way” between [enriched] Cat-category theory and bicategory theory. It uses enriched category theory, but not in the simple minded way of Cat-category theory; and it cuts through some of the technical nightmares of bicategories.

view this post on Zulip John Baez (Oct 14 2022 at 10:08):

Another approach people have considered is looking at "homotopy algebras" of Lawvere theories: algebras in the category of simplicial sets, where all the laws hold up to coherent homotopy. Julia Bergner did this for multi-sorted Lawvere theories and showed that these homotopy algebras are all equivalent to strict algebras:

We define the notion of a multi-sorted algebraic theory, which is a generalization of an algebraic theory in which the objects are of different "sorts." We prove a rigidification result for simplicial algebras over these theories, showing that there is a Quillen equivalence between a model category structure on the category of strict algebras over a multi-sorted theory and an appropriate model category structure on the category of functors from a multi-sorted theory to the category of simplicial sets. In the latter model structure, the fibrant objects are homotopy algebras over that theory. Our two main examples of strict algebras are operads in the category of simplicial sets and simplicial categories with a given set of objects.

view this post on Zulip fosco (Oct 14 2022 at 10:22):

oh, this is very interesting: I wonder, can you apply Bergner result to the model structure on 2-categories?

view this post on Zulip John Baez (Oct 14 2022 at 11:14):

I don't know. She may only be looking at homotopy models of Lawvere theories in SimpSet with the Quillen model structure on SimpSet? Not sure. If so, one may need to generalize the argument to handle models in other model categories. It would be worth doing, since it might then handle the case you're interested in but also lots more.

view this post on Zulip fosco (Oct 14 2022 at 13:57):

each time I study Lawvere theories I stumble upon research projects :grinning:

view this post on Zulip Mike Shulman (Oct 14 2022 at 16:11):

There are also plenty of rigidification results in the 2-category theory literature. In particular, it seems fairly likely to me that rigidification for Lawvere 2-theories would follow from Power's general coherence result.