Useful ideas in category theory which violate the principle of equivalence

Question

Or an alternate title: using evil for the greater good.

In category theory, the principle of equivalence says that statements about things should be invariant under the appropriate notion of thing-equivalence. For example, if we have a group $G$ we shouldn't ask a question like "does the underlying set of $G$ contain $x$" because it's possible to have $x \in G$ and $x \notin H$ while $G \cong H$. One formalization of this principle is the univalence axiom.

I think the principle of equivalence is a reasonable guiding principle, but care must be taken when determining "the appropriate notion of thing-equivalence". The classic example is that categories themselves naturally assemble into a $2$-category, not just an ordinary $1$-category, and so the suitable notion of equivalence (equivalence of categories) is weaker than naïve version (isomorphism of categories). As a consequence, the definition "A group is a groupoid with a single object" (Joke 1.1 in Algebra: Chapter 0 by Paolo Aluffi) violates the principle of equivalence, because the property of "having a single object" is not invariant under equivalence. We can remedy this to the definition "A group is a pointed connected groupoid" (although perhaps even the notion of a pointed groupoid violates the principle of equivalence, so we really want to say it's an object of the under $2$-category $T/\mathsf{Grpd}$ whose underlying groupoid is connected, where $T$ is "the" $2$-terminal groupoid). Contemplating this does lead to some interesting ideas, e.g. if we view groups as groupoids in a naïve way they're more like torsors.

But I like groups! And I like doing algebra. Working with groupoids as strict, algebraic objects isn't inherently "evil". Ronald Brown's book Topology and Groupoids discusses cofibrations of groupoids, strict pushouts of groupoids, and groupoids defined by generators and relations, and I think it's genuinely interesting stuff. You certainly need to be careful when working with categories as strict objects, but I find it easier to think about strict things than weak things. I like that the framework of model categories lets me present weak things by strict things and I like working with strict $2$-categories over weak ones. Surely any category theorist would agree that the Grothendieck construction is of fundamental importance, and the usual statement of it in terms of Grothendieck fibrations violates the principle of equivalence (because Grothendieck fibrations involve equality of objects). It's no coincidence that the idea of a Grothendieck fibration was (I believe) historically prior to the idea of a Street fibration, or that strict $n$-categories are so much easier to define than weak ones. It's also frequently simpler to think about strict monoidal categories and strict monoidal functors than the maximally weak ones. We even have Lack's "Theorem", saying "naturally occurring bicategories tend to be equivalent to naturally occurring strict $2$-categories".

Although it's not always possible to get everything we want from strict categories (e.g. there is no strict $3$-groupoid equivalent as a weak $3$-category to $\Pi_{\leq 3} \mathbb{S}^2$) it can still be useful when studying categories to think about them strictly. See also the $(\mathrm{bo}, \mathrm{ff})-$factorization system, the canonical model structure on $\mathsf{Cat}$, the nerve construction, and the Thomason model structure on $\mathsf{Cat}$. What other examples are there within category theory where it's useful to treat categories themselves as strict objects? This question was motivated by looking at the paper "Amalgamations of Categories" by MacDonald and Scull (because I had a strict pullback square of categories and I wanted to know if it was also a strict pushout square).

Edit: One more use case I forgot to mention is the bar construction associated to a comonad. If $W$ is a comonad on $\mathsf{C}$ then we can view it as a comonoid object in the strict monoidal category $(\operatorname{Fun}(\mathsf{C}, \mathsf{C}), \circ, \operatorname{Id})$. This is classified by a unique strict monoidal functor $F : \Delta^{\mathrm{op}} \to \operatorname{Fun}(\mathsf{C}, \mathsf{C})$, where $\Delta^{\mathrm{op}}$ is the augmented simplex category under ordinal sum. We can view $F$ instead as a functor from $\mathsf{C}$ to the category of augmented simplicial objects of $\mathsf{C}$, and this functor takes an object to its simplicial bar resolution with respect to $W$. We could still basically make this work without strictness, since (I believe) if $\mathsf{M}$ is a not-necessarily strict monoidal category then a monoid object of $\mathsf{M}$ is classified by an essentially unique strong monoidal functor $\Delta \to \mathsf{M}$. But I find it easier to think about a unique strict monoidal functor than an essentially unique strong monoidal one.

Answer 1

I would think about this question in this way: If you have a construction that violates the equivalence principle then either (A) it is a strictified or simplified version of something that is compatible with the equivalence principle, and what you care about is the latter, but you study the former because it is more convenient, or (B) it is actually not a construction about categories.

Examples of (A) are very common, and I don't think anyone think there is anything wrong with them. You're just using some sort of "trick" to reduce the number of coherences and isomorphisms you need to deal with, and hence the complexity of the problems. These methods are not fundamentally categorical, but they are tool that allows to prove category theoretic theorem. Here I think of things like (most of them being mentioned in the OP):

• The whole theory of Grothendieck fibrations (the invariant version being the theory of Street fibration).

• Strict monoidal categries — which are equivalent to monoidal categories.

• The example of the bar construction — the "pseudo"-free bicategory generated by a monad is equivalent to the free strict 2-category generated by a monad.

• The Thomason model structure: The weak equivalences are compatible with the equivalence principle, but the rest of the model structure isn't, but I'm confident you could get rid of this by building a 2-categorical model structure on the 2-category of categories instead (I'm not completely sure this has been done though).

• A little more vague, but any definition of higher categories does this at some point. As long as your definition of higher categories is based in set theory or ordinary category theory you are going to need to consider some condition that are not invariant from the $n$-categorical point of view (like condition on the set of $n$-cells) and then prove that the resulting notion are actually nicely invariant in some appropriate sense. E.g. the theory of quasitheory uses a lot of non-invariant notion like (e.g. "inner fibrations") at the begining, and gradually when you advance though the theory you become more and more able to avoid them if you want too.

Then we have things that still fits in category A, but where you actually need a bit of work to realize it, and when you finally do that additional work you learn something interesting about how to think about the construction or objects you are looking at. Here I think of things like:

• Dagger categories, see this question and in particular Peter LeFanu Lumsdaine's answer.

• Strict $n$-categories. This one feels non-categorical, because for $n>2$ it doesn't give the "correct" things, but there is a way to understand it in a more categorically admissible way: A strict $n$-category is the data of a sequence $C_0 \to C_1 \to C_2 \to \dotsb C_n$ where $C_i$ is a (weak) $i$-category and the functor $C_i \to C_{i+1}$ is "$i$-full" (not sure this is the right word, I mean fully faithfull on k-cell for $k<i$ and full on $i$-cells). While this makes the notion of strict $n$-category no longer purely about $n$-categories (it involves things that are only $i$-category) it can be used to give meaning to some question like "why is this specific weak $n$-category representable by a strict one"?

• Contextual categories. These violate the equivalence principle pretty badly — that's why Voevodsky called them C-systems and not categories. But they are still very natural things to consider as they appear naturally from dependently type theory. And it turns out that the 1-category of contextual categories can be described naturally as a full subcategory of the bicategory of for example natural models or of categories with attributes with a terminal object, as the one that are "well founded" in a certain precise sense (up to isomorphism, each object is generated from the terminal object by a finite number of application of the comprehension scheme). And yes this involves an equivalence between a 1-category and something that at first sight is a bicategory.

Examples of (B) are of course much rarer, but I'm sure there are a few in the literature. And even then, maybe it is just that we haven't found the right point of view that make them categorical again.

• An example of this is the use of strict morphisms of prederivators to encodes $\infty$-categories by Kevin Arlin in On the $\infty$-categorical Whitehead theorem and the embedding of quasicategories in prederivators. This is a very interesting construction, but where you need to remember that it is not really about "derivators" seen as category theoretic objects as it breaks the equivalence principle (and if you look at the details of the construction it mostly focus on the set of objects and actually doesn't use the morphisms that much). (And this is not a criticism of the paper!)

• Maybe not as clear cut as the previous one, but as mentioned in the comments by Mike Shulman, another example is the notion of lax functor between 2-categories or bicategories. It is an interesting notion, for example a monad in a bicategory $C$ is a lax functor from the terminal category to $C$, and a $V$-enriched category with set of objects $X$ is a lax functor from the anti discrete category on $X$ to the bicategory $BV$ with one object and $V$ as endomorphism of that object. But as the second example shows the notion is not invariant under equivalence of bicategories. Though there are some explanation for this in the framework of double categories, so one could bring that back to (A) this way, but I'm not aware of a way to do this with just bicategories.

• In Relating first-order set theories, toposes and categories of classes, Awodey, Butz, Simpson, and Streicher interpret a membership-based set theory into an elementary topos by replacing the topos with an equivalent category that admits a non-equivalence-invariant structure called a "directed structural system of inclusions". This is a generalization of how in the category of sets (in a set theory like ZFC) we can single out those injections that are literally subset inclusions. This can be written more "categorically" as an M-category.