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: theory: category theory

Topic: Cartesian 2-category


view this post on Zulip Bruno Gavranović (Apr 11 2023 at 16:03):

Is there a good reference for cartesian 2-categories?

I'm trying to understand the correct analogue of the universal property of the product, which I imagine would still be

C(X,A×B)C(X,A)×C(X,B)\mathcal{C}(X, A \times B) \cong \mathcal{C}(X, A) \times \mathcal{C}(X, B)

where this would be now an isomorphism of categories. I imagine one might want to potentially weaken this to an equivalence, though it's not clear whether one has to.

I'm interested in the strictest sensible version.

view this post on Zulip Mike Shulman (Apr 11 2023 at 16:13):

I don't know of a reference that deals specifically and abstractly with cartesian 2-categories; I don't know if there's enough to say about them to fill a paper. As with any 2-categorical limit, finite products have both a strict version with a universal property given by an isomorphism and a weak version ("bicategorical products") with a universal property given by an equivalence. Many naturally-arising 2-categories, such as Cat\rm Cat, have strict finite products; but others, such as Prof\rm Prof and Span\rm Span, only have weak bicategorical ones. However, because finite products are a [[flexible limit]], any bicategory with bicategorical finite products is equivalent to a strict 2-category having strict finite products, by a version of the [[coherence theorem for bicategories with finite bilimits]].

view this post on Zulip Niels van der Weide (Apr 11 2023 at 16:45):

Relevant references on this topic:

Note: both papers are about the strict version.

view this post on Zulip Bruno Gavranović (Apr 11 2023 at 17:38):

I see.
If I'm only interested in the strict version, it sounds like should be enough to prove the isomorphism between the categories holds, and nothing else.

view this post on Zulip Mike Shulman (Apr 11 2023 at 18:53):

Holds naturally, of course.