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.
John Bourke, Joanna Ko, and I have a new preprint on arXiv: Enhanced 2-categorical structures, two-dimensional limit sketches and the symmetry of internalisation. Here's the abstract:
Many structures of interest in two-dimensional category theory have aspects that are inherently strict. This strictness is not a limitation, but rather plays a fundamental role in the theory of such structures. For instance, a monoidal fibration is – crucially – a strict monoidal functor, rather than a pseudo or lax monoidal functor. Other examples include monoidal double categories, double fibrations, and intercategories. We provide an explanation for this phenomenon from the perspective of enhanced 2-categories, which are 2-categories having a distinguished subclass of 1-cells representing the strict morphisms. As part of our development, we introduce enhanced 2-categorical limit sketches and explain how this setting addresses shortcomings in the theory of 2-categorical limit sketches. In particular, we establish the symmetry of internalisation for such structures, entailing, for instance, that a monoidal double category is equivalently a pseudomonoid in an enhanced 2-category of double categories, or a pseudocategory in an enhanced 2-category of monoidal categories.
There are also some slides on this work from John's talk at CT this year. I'm not going to summarise the paper here, because I think the introduction to the paper does a good job, but I'm very happy to answer any questions or receive any comments here!
Would you be able to say anything about why "a monoidal fibration is – crucially – a strict monoidal functor, rather than a pseudo or lax monoidal functor"? Why is this crucial?
One of the most important properties of fibrations is their relationship to pseudofunctors. It is therefore reasonable to expect that a good notion of fibration corresponds to a notion of pseudofunctor in a way extending the classical correspondence. This is indeed true for monoidal fibrations (see Shulman and Moeller–Vasilakopoulou); the fact that the underlying functors are strict monoidal corresponds to the fact that fibrations are, intuitively, projections, so that the monoidal structure on the total category is defined in terms of that on the base. If you drop the requirement that the monoidal functors are strict, you would lose this correspondence.
However, if a fibration is a pseudo monoidal functor, it seems it ought to be possible to modify the tensor product of its domain by transporting it along the monoidality constraints to make it a strict monoidal functor.
That does seem plausible. The "crucially" in the abstract was intended to correspond to the fact that it is the strict monoidal functors that are primitive rather than the pseudo monoidal ones (for instance, there are similar situations in which it is certainly not possible to strictify like this). But perhaps another word would be clearer there.
I don't object to the word "crucially".
So I think the non-strict versions still correspond to monoidal pseudofunctors, right? You should be able to replace the domain category with its pseudomorphism classifier to strictify the fibration and this should give something equivalent. Possibly there is also some thought required with using morphisms of fibrations that only commute up to isomorphism.
I bring this up since the nonstrict version seems to be pretty common in practice. For example, I believe the reflection from commutative monoids to abelian groups is a monoidal fibration in the weaker sense and making it strict seems like it would be quite painful.
Is it clear that the strict monoidal functor obtained by the pseudo morphism classifier would be a fibration if the original pseudo monoidal functor was?
I would be interested to see some examples of non-strict monoidal fibrations. However, our paper is not so much making an argument about the "correct" definition of structure-preserving fibration, as it is observing that people have already defined various notions of structure-preserving fibration in the literature, each of which does preserve the given structure strictly, and giving a context in which these structures can be defined and studied. It turns out that requiring strict structure preservation lends nice properties to such fibrations (e.g. monoidal fibrations are equivalent to pseudomonoids in fibrations), which lends credence to the definition being the most appropriate one, but I think the stronger evidence is how often this strictness condition is imposed in the literature.
Note that the notion of Grothedieck fibration (as opposed to "Street fibration") already involves equality of objects, but can be formulated without violating the principle of equivalence as a [[displayed category]]. Monoidal strictness can also be formulated for a displayed category in an invariant way, with the tensor product of the "domain" (the displayed category) being dependent/displayed over that of the "codomain" (the base).
My argument for strictification doesn't change either category or the functor, only the tensor product of the domain, so the functor is trivially still a fibration in that case.
IMO a good 'technical' reason to stick to strict morphisms is that non-strict morphisms often don't admit base change (e.g. you can't, in general, strictly pullback non-strictly monoidal functors along each other), which is weird for a notion of fibration
Of course one could argue iso/lax commas are more natural 'base change' operations in those cases so ultimately one is back to a 'conceptual' preference for strictness in display maps, albeit of a different nature