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: Cat(Mon(Cat)) vs Mon(Cat(Cat))

Matteo Capucci (he/him) (Apr 10 2024 at 14:44):

Monoidal double categories are pseudomonoids in pseudocategories in Cat, or, alternatively, pseudocategories in pseudomonoids in Cat.
A proof of this fact is that both are special kinds of degenerate triple categories (having only one 1-cells in one of the loose directions), and their equivalence is induced by exchanging loose directions.
Does anyone have a better proof? Or better still, a reference I can cite?

Matteo Capucci (he/him) (Apr 10 2024 at 14:45):

(cc'ing @Evan Patterson whom I expect to be able to help)

John Baez (Apr 10 2024 at 14:56):

Someday there may be a better proof based on "commutativity of internalization". This principle is well-established for structures definable by finite limits theories, like categories and monoids. Using this principle, we instantly know that for any category K with finite limits, the category of

monoids in (categories in K)

is equivalent to the category of

categories in (monoids in K)

We'd really like an equivalence of 2-categories here, because there happens to be a 2-category of categories in any category with finite limits. So there is more work to be done even at this level (if it hasn't been done already).

But anyway, someone should categorify "commutativity of internalization" so that it applies to algebraic structures definable by '"finite limits 2-theories"', such as pseudocategories and pseudomonoids.

John Baez (Apr 10 2024 at 14:59):

I'm putting '"finite limits 2-theories"' in quotes because it needs to be clarified a bit: there are several things one might mean, and one wants to pick the right one(s) to handle the examples that come up.

Nathanael Arkor (Apr 10 2024 at 16:12):

Matteo Capucci (he/him) said:

Monoidal double categories are pseudomonoids in pseudocategories in Cat, or, alternatively, pseudocategories in pseudomonoids in Cat.
A proof of this fact is that both are special kinds of degenerate triple categories (having only one 1-cells in one of the loose directions), and their equivalence is induced by exchanging loose directions.
Does anyone have a better proof? Or better still, a reference I can cite?

This isn't quite true – you need to be careful about strictness (as pointed out in Remark 2.12 of Shulman's Constructing symmetric monoidal bicategories). A monoidal double category is a pseudomonoid in the 2-category of double categories and pseudo double functors. Equivalently, it is a pseudocategory in the 2-category of monoidal categories and pseudo monoidal functors such that the source and target morphisms are strict monoidal.

Nathanael Arkor (Apr 10 2024 at 16:17):

Or better still, a reference I can cite?

John Bourke, Joanna Ko and I have been working on a paper on this topic; we have a symmetry result for a class of two-dimensional limit sketches, which includes monoidal double categories as an example. (John gave a talk about it at the Masaryk University Algebra Seminar, but it doesn't appear the slides have been uploaded yet.) I am hopeful it will be ready before too long; I will send you a link when it is available.

Kevin Carlson (Arlin) (Apr 10 2024 at 17:26):

That’ll be great to see, both for the specific result and more broadly to have a paper about 2-sketches finally in the literature!

Matteo Capucci (he/him) (Apr 11 2024 at 07:27):

Nathanael Arkor said:

Matteo Capucci (he/him) said:

Monoidal double categories are pseudomonoids in pseudocategories in Cat, or, alternatively, pseudocategories in pseudomonoids in Cat.
A proof of this fact is that both are special kinds of degenerate triple categories (having only one 1-cells in one of the loose directions), and their equivalence is induced by exchanging loose directions.
Does anyone have a better proof? Or better still, a reference I can cite?

This isn't quite true – you need to be careful about strictness (as pointed out in Remark 2.12 of Shulman's Constructing symmetric monoidal bicategories). A monoidal double category is a pseudomonoid in the 2-category of double categories and pseudo double functors. Equivalently, it is a pseudocategory in the 2-category of monoidal categories and pseudo monoidal functors such that the source and target morphisms are strict monoidal.

Uhm I see, thanks for pointing it out!

Matteo Capucci (he/him) (Apr 11 2024 at 07:58):

This is a very interesting thing to me.
I previously stumbled upon the fact that we are usually quite cavalier about strictness in $\bf Span(Cat)$ because we can just get away with it there, but as soon as you work in $\bf Span(\cal K)$ for some other 2-category $\cal K$ then strict pullbacks might become a luxury you can't afford. In fact the 'biblically accurate' version of $\bf Span(\cal K)$, described here, uses isocommas for compositions and maps of spans are maps between apexes with invertible fillers witnessing the commutativity of the two induced triangles.

This introduces a discrepancy between 'weak double categories' and 'pseudocategories in Cat', where the latter is taken to mean pseudmonad in $\bf Span(\cal K)$ for $\cal K=\bf Cat$; which amounts to the fact that the structural equations of weak double categories defining e.g. what a composable pair of loose arrows is, or what functoriality means, are weakened to mere isomorphisms.

This highlights an hypocrisy in the traditional usage of equality and isomorphism: we strongly believe equality in a categry should be isomorphism, but then in the definition of weak double category we insist we want strict equality! This is not to point fingers (I wouldn't know to whom anyway), just to notice an interesting conceptual issue here.

Anyway, the reason I'm bringing this up is that it seems that insisting on weak double categories introduces the hiccup @Nathanael Arkor pointed out. In fact, a pseudomonoid in pseudocategories would only satisfy $\partial_i(f \otimes g) \cong \partial_i(f)\otimes\partial_i(g)$, which is what we get from a pseudocategory in pseudomonoids, though I admit I didn't check if the rest of the data & coherence also matches up.

Matteo Capucci (he/him) (Apr 11 2024 at 08:09):

A possible way to get out of this is to work with isofibrant spans instead, meaning those spans which are two-sided isofibrations. Then a pseudomonad therein is an isofibrant double category, meaning isomorphisms can be traded freely between the tight and loose directions. It then seems one can produce an equivalent monoidal (in the strict sense) isofibrant double category for each monoidal (in the weak sense) double category

Nathanael Arkor (Apr 11 2024 at 08:22):

Matteo Capucci (he/him) said:

This highlights an hypocrisy in the traditional usage of equality and isomorphism: we strongly believe equality in a categry should be isomorphism, but then in the definition of weak double category we insist we want strict equality! This is not to point fingers (I wouldn't know to whom anyway), just to notice an interesting conceptual issue here.

I think there's a common misconception in category theory (due to some extent to the nLab, which at some point in the past used rather incendiary language) that in category theory it is always true that one should work with the weakest notion of "sameness" as possible. However, the "principle of equivalence" really amounts to saying that when you work with objects of a category, you should only identify objects up to isomorphism, not equality – in other words, that properties of categories should be invariant under equivalence. What it doesn't say is that, when you give a definition, the definition should only make use of isomorphism rather than equality.

Clearly, there are definitions for which we really do want to use equality rather than isomorphism. For instance, in a pseudofunctor, we want sources and targets to be preserved strictly, so that when we have two composable 1-cells in the domain, they are still composable in the codomain. The "pseudo" in "pseudofunctor" refers to the weak preservation of composition and identities, not source and target. There's a good heuristic to check whether one should expect certain data to be preserved strictly or not. If you present the structure in a metatheory that has a notion of type dependency, for instance a generalised algebraic theory, then the dependencies (a.k.a. display maps) should be preserved strictly, whereas the operations may be preserved only weakly. For instance, in the typical presentation of a category, you have a sort of morphisms, which is dependent on the source and target variables. Thus, these should be preserved strictly by homomorphisms.

Nathanael Arkor (Apr 11 2024 at 08:25):

In other words, I don't think there is anything wrong with the definitions of pseudocategory or monoidal double category: they capture the appropriate strictness for the examples we care about. However, the fact they they do involve differing levels of strictness needs we need to be a little more careful when we manipulate them.

Matteo Capucci (he/him) (Apr 11 2024 at 09:26):

I appreciate your argument on a practical level, but empirically and philosophically I have a hard time accepting it. Empirically, I observe that things work without hiccups when I work fully weakly and when you try to strictify it there's often some place where this strictification breaks or requires some clever workaround. Philosophically, when you say

[W]hen you work with objects of a category, you should only identify objects up to isomorphism, not equality – in other words, that properties of categories should be invariant under equivalence. What it doesn't say is that, when you give a definition, the definition should only make use of isomorphism rather than equality.

These seem in contradiction to me: when I define structure on top of categories, why is this in a privileged position to access strict equality rather than isomorphism only? In other words, 'properties of categories should be invariant under equivalence', why not structure?

Nathanael Arkor (Apr 11 2024 at 09:59):

From an empirical point of view, I would say these concepts are even easier to justify: they capture the examples we care about, and are convenient to work with, which makes them good definitions.

From an abstract point of view, in these examples the structures we are defining (e.g. monoidal double categories) involve morphisms of structures (e.g. pseudo double functors). This is true generally in functorial semantics. Morphisms of structures are not completely weak. For instance, a pseudo functor preserves source and target strictly. You could argue that this is too strong, but I think you will have difficulty finding examples of notions of morphism that do not preserve source and target strictly.

John Baez (Apr 11 2024 at 10:33):

People like Makkai have argued convincingly (to me) that source and target are fundamentally different than composition. For example, there's a definition of category where we start with a collection of objects and then for each pair of objects $x , y$ a set $\mathrm{hom}(x,y)$; after this we give composition and identities obeying equational laws. In this approach the homsets are a "dependent type", and saying $f : \mathrm{hom}(x,y)$ is a "typing judgement". This is conceptually different than starting with an undifferentiated collection of all morphisms, defining functions $s,t$ from this to the collection of objects, and then asserting equations $s(f) = x, t(f) = y$. In the dependently typed approach it makes no sense to talk about a morphism without first knowing its source and target. So, for example, it makes no sense to ask whether $f = g$ unless we already know $f, g: \mathrm{hom}(x,y)$ for some objects $x,y$.

This explains why it's not evil - to use incendiary language :smiling_devil: - to demand that functors preserve the source and target of morphisms.

Morgan Rogers (he/him) (Apr 11 2024 at 10:44):

It's a fun coincidence that @Jonas Frey was talking about that dependently typed presentation at LIPN this morning.

John Baez (Apr 11 2024 at 10:46):

Makkai developed his theory of $\omega$-categories based on his system FOLDS: "first-order logic with dependent sorts". This avoids "evil" in a very elegant way.

Matteo Capucci (he/him) (Apr 11 2024 at 12:27):

Nathanael Arkor said:

From an empirical point of view, I would say these concepts are even easier to justify: they capture the examples we care about, and are convenient to work with, which makes them good definitions.

Of course, I'm not arguing against that :) but we also observe that working up to the correct level of equivalence makes life easier from a technical standpoint, if messy. So I'm highlighting this... tension?

Matteo Capucci (he/him) (Apr 11 2024 at 12:48):

Actually I believe non-strictly consecutive morphisms are composed all the time in mathematical practice, since we rarely take care of precisely aligning boundaries of morphisms with e.g. structural morphisms we know to be coherent, and instead it is understood those morphisms are implicitly around. The very fact I'm asking this question is because I have some concrete construction that churns out double monoidal categories with possibly non-strictly monoidal source/target.

Morgan Rogers (he/him) (Apr 11 2024 at 12:50):

(eg. we are often happy to suppress the associators when composing morphisms in monoidal categories)

Matteo Capucci (he/him) (Apr 11 2024 at 12:58):

To answer @John Baez, the definition you bring up seems innocuous but it 'sneaks in' meta-level equality when one defines composition when $f: {\rm hom}(x,y)$ and $g:{\rm hom}(y,z)$. This is a way to say $y=y$ with notation, but then in practice we know this level of strictness can be hard to maintain, hence the struggle for univalent foundations and heterogeneous equality.

But it seems that this is always the culprit with strictness, at some point we draw a line between 'object theory' and 'metatheory' and we tacitly assume metatheory has oracle-like properties (like LEM, decidable equality) whereas object theory has to be 'constructive' somehow (so e.g. you have to witness equality judgments). So this seems an issue on where we draw the line for categories, is it at the 0-level or at the 1-level?

Morgan Rogers (he/him) (Apr 11 2024 at 13:09):

I think it's more of an inevitable problem with syntax requiring repetition. For a full specification of the composition operation you would write $x, y, z: {\rm ob}, \,g:{\rm hom}(y,z), \, f: {\rm hom}(x,y) \vdash g \circ f : {\rm hom}(x,z)$, and as such we already have a repetition of the object variables even before the $y$ is 'used' a second time in the type of $f$: we 'name' $x,y,z$ as terms of the type of objects and then 'use' those terms in the morphism type constructor. There are notions of linearity that prevent a variable from being used more than once (after it is named, that is), but if we wanted a weaker version where identical types are replaced with equivalent ones it would actually have the same amount of repetition, since we would need a further statement presenting the identity between the terms.

Morgan Rogers (he/him) (Apr 11 2024 at 13:11):

I suppose this observation is related to notions of identity type etc.

Nathanael Arkor (Apr 11 2024 at 13:33):

Yes, I agree with Morgan. You want to be able to duplicate variables without viewing that as identification of variables via a meta-level equality. It depends on your philosophy, but I would argue it is possible to refer to an object multiple times without having a notion of sameness of objects, other than the identity.

Nathanael Arkor (Apr 11 2024 at 13:35):

Having contraction in a type theory means you have invariance under some operation on a context; it does not require a meta-level equality.

Nathanael Arkor (Apr 11 2024 at 13:36):

I think if you distinguish identification of variables, and equality of terms, the apparent problem with strictness in the definition of functors, monoidal double categories, etc., goes away.

Mike Shulman (Apr 11 2024 at 15:20):

Matteo Capucci (he/him) said:

This highlights an hypocrisy in the traditional usage of equality and isomorphism: we strongly believe equality in a categry should be isomorphism, but then in the definition of weak double category we insist we want strict equality!

When I was a graduate student in Chicago back in the oughts, I met Bob Paré for the first time at a conference (I think it was the Mac Lane Memorial Conference), and this was the first question I asked him. If memory serves, he answered by asking me what I thought. I gave essentially the same two answers that have been given here: first, that many double categories are isofibrant and so we can strictify isomorphisms involving domains and codomains; and second, that we don't need to weaken when talking about "structure" (I didn't know the phrase "dependent types" back then, but I think this is essentially the same point).

Mike Shulman (Apr 11 2024 at 15:41):

Matteo Capucci (he/him) said:

Philosophically, when you say

[W]hen you work with objects of a category, you should only identify objects up to isomorphism, not equality – in other words, that properties of categories should be invariant under equivalence. What it doesn't say is that, when you give a definition, the definition should only make use of isomorphism rather than equality.

These seem in contradiction to me: when I define structure on top of categories, why is this in a privileged position to access strict equality rather than isomorphism only? In other words, 'properties of categories should be invariant under equivalence', why not structure?

Maybe this was answered already, but I think this is a misunderstanding. I think what Nathanael was saying is that talking about equality in its statement doesn't mean a definition (be it property or structure) isn't invariant under equivalence.

Mike Shulman (Apr 11 2024 at 15:42):

Rather, there are precise ways in which we can talk about equality -- namely, those that can be encoded using dependent types -- while still remaining invariant under equivalence.

Mike Shulman (Apr 11 2024 at 15:43):

Another point that I think hasn't been made yet is that it's impossible to avoid at least the dependent-types kind of equality. Suppose you weaken the composition operation so that when composing $f:x\to y$ with $g:y'\to z$ you only require $y$ and $y'$ to be isomorphic. But that means you have an isomorphism $h:y \cong y'$ whose domain is equal to $y$ and whose target is equal to $y'$!

Matteo Capucci (he/him) (Apr 11 2024 at 15:50):

Mike Shulman said:

Another point that I think hasn't been made yet is that it's impossible to avoid at least the dependent-types kind of equality. Suppose you weaken the composition operation so that when composing $f:x\to y$ with $g:y'\to z$ you only require $y$ and $y'$ to be isomorphic. But that means you have an isomorphism $h:y \cong y'$ whose domain is equal to $y$ and whose target is equal to $y'$!

Yeah I think this is the most 'convincing' issue with weakening everything (@Morgan Rogers (he/him) mentioned this earlier btw). I'm putting 'convincing' in quotes because I'm not arguing for dropping strictness in the definition of monoidal double category or double category, I'm just trying to grasp the nuances in the principle of equivalence.

Mike Shulman (Apr 11 2024 at 15:51):

Ok, sorry I missed it.

Matteo Capucci (he/him) (Apr 11 2024 at 15:54):

No problem!

Mike Shulman said:

Rather, there are precise ways in which we can talk about equality -- namely, those that can be encoded using dependent types -- while still remaining invariant under equivalence.

I think this perspective is the one that I like best. But then we shouldn't be using functors for things like source and target of a double category, which really should be thought as displaying maps, and instead have them being isofibrations.

Matteo Capucci (he/him) (Apr 11 2024 at 15:57):

If that's the case I'd say this vindicates my hunch that's there's a tension to be resolved, the resolution being adopting isofibrations for things that need to 'see' equality (better: display data invariant under equivalence)

Mike Shulman (Apr 11 2024 at 16:03):

Dependent types FTW!

Graham Manuell (Apr 12 2024 at 09:21):

I don't know if this is related or not, but I never know how to think of isomorphisms in double categories. Usually when two objects are isomorphic I think of them as the same thing, but what if they are, say, horizontally isomorphic, but not vertically isomorphic? Relatedly there doesn't appear to be one accepted notion of equivalence of double categories? I never know what to make of that. Things are bit simpler when you have companions and so there is a stronger and weaker version of isomorphism, but in general I don't really have any feeling for what is going on.