# Are evil properties really evil

I have this question for a moment now, so I think it is time that I sort it out.

I got into category theory and homotopy type theory at the same time, and so I have always read and been told that one should be careful about "evil" properties, i.e. the ones that are not invariant under equivalence of categories. So in order to try and disambiguate the terminology, what I will refer to as "categories" are up to equivalence, and I will call a precategory the objects up to isomorphism. In other words, categories are objects of the category $$\operatorname{Ho}(\operatorname{Cat})$$, for the folk model structure of $$\operatorname{Cat}$$, and the precategories are the objects of $$\operatorname{Cat}$$.

It is my understanding that category theory is in fact about categories and not precategories, and it makes perfect sense, since the point of category theory is to give the proper meaning to isomorphisms. The intuition that I always keep in mind is that it should not matter if I see the same object many times as long as I know that it is the same. In order to really talk about these categories, people have started looking at the appropriate language, which is a language in which evil property do not make sense, or are not expressible. This is a way to get to the theory of categories, or their internal language (I am not sure how to refer to this notion exactly).

However, there are many constructions that are used on precategories, the two main ones that I have in mind are the Reedy categories and the contextual categories (aka C-systems), and some results are proved by making heavy use of these constructions.

My understanding of the situation

The precatgories can be thought of as some sort of a "presentation" of a given category. It is of course not unique since many non-isomorphic can be equivalent, but that's fine, I am used to that in groups or vector spaces : A group can have different presentations. Now the using an "evil" notion would amount to working in a given presentation of a group, so whatever non-evil property you prove for a Reedy category is in fact a property of the category presented by my precategory which is Reedy. In group theory would be analogue to a theorem of the form

"If a group has a finite presentation, then it satisfies $$P$$"

And then I can freely state that $$\mathbb{Z}$$ satisfies $$P$$, since it is finitely presented as $$\langle x\rangle$$ , although I might as well give the (different) presentation $$\langle x_1,x_2,\ldots | x_1=x_2, x_1 =x_3,\ldots\rangle$$, which is not finite. It is sort of picking a representative in an equivalence class to prove a property which goes through the quotient. This is something we do a lot, and it gives a perfectly valid proof. So here I can very easily transform the property "being a Reedy category" to "being equivalent to a Reedy category", and I have changed my evil property into a non-evil one. Every non-evil property I can prove for Reedy categories is in fact provable for all the precategory that are categorically equivalent to a Reedy category

Possible limitations

There are two main "problems" that I can see using evil notions in order to prove non-evil ones

• Firstly the construction that I get may not be "canonical" or "natural" (again I am not sure what the proper terminology should be here). If I take the example of a Reedy model structure, there might be many equivalent precategory that present the same category and that are Reedy. The Reedy model structure I get using one might not agree with the Reedy model structure I get using the other - even up to the equivalence between them. This is in my intuition much like the fact that every finite dimensional vector space is isomorphic to its dual, but there is necessarily a choice of a basis, leading to really different isomorphisms. Here a choice of a basis is a given presentation. This also makes sense with my previous correction of Reedy to be non-evil : the property "being equivalent to a Reedy precategory" gives an equivalence of categories, and then a specific choice of a presentation, and there might be many ways to "be equivalent to a Reedy precategory", leading to different constructions for the model structure. But again, constructing something non-canonical is not that big of a deal, if we carry out the constructions everywhere. After it is true that all finite dimensional vector space is equivalent to its dual even if there is no canonical way to do it - Why not imagine properties in non-evil properties in categories that are true, but never "non-evily" true (i.e. never true in a canonical way)?

• The proof that we get is not in the language of categories (and I think this is basically saying the same thing). It is a proof in the language of precategories. But again it sounds fine to me, with finite dimensional vector spaces we usually say "take a basis", which is not expressible in their internal language. It does not make the fact true, it just makes it non-canonical.

My Question So firstly, I would like to know if my intuition is correct. If so, the "evil" properties do not seem too evil to me, and we can freely use them as long as we don't claim canonicity. I have seen examples of this in different areas of mathematics, so why not in category theory? If my intuition is incorrect, am I missing something that would make these concepts truly evil?

Then a related question that I have (assuming my understanding is correct) is are there any known examples of a property that is always true but never canonically in category theory? What I mean by that is a theorem that we can prove about categories but using precategories, and that is not provable in the internal language of categories? If we know for some reason that no such thing exists, then I would be convinced to avoid evil properties, as they are unnecessary, but otherwise how to know that we are not missing something by avoiding them?

• You should be careful of "evil" property, but that does not means you should avoid them completely. To keep your metaphor going: some construction involving basis of vector space are interesting, as long as you remember they might depends on the basis unless proved otherwise (and for example be non-functorial, or not apply to bundle of vector spaces). Similarly, evil construction on categories depends on the underlying pre-categories and might not be invariant under equivalence of categories and not be functorial in the 2-categorical sense. That does not mean they should be completely ignored. Feb 6, 2020 at 19:13
• There must be reasons why ncatlab.org/nlab/show/principle+of+equivalence was renamed and does not speak of evil concepts anymore (apart from a short remark). I have the feeling that the whole question is based on a tacit judgement of concepts which are not invariant under equivalences, based on the term "evil" which some people have used. But there is nothing wrong about these concepts. In particular when it comes to applications of small categories in combinatorics, representation theory etc. these concepts are useful, and by the way isomorphisms of categories are useful as well. Feb 7, 2020 at 0:12
• Homotopy type theorists would say that their point of view clarifies matters in a rather pleasant way. The HoTT book introduction to the chapter on category theory summarizes what happens. In essence, we've been using the wrong equality all along, and mistakenly blamed categories on the ensuing problems. Feb 7, 2020 at 8:53
• Ho(Cat)? Thunder? THUNDER! THUNDER! THUNDER CATS, HO!!!! Feb 7, 2020 at 23:32
• @AndrejBauer Are you refering to univalent categories, saying the type of equality has to be the same as the type of isomorphisms? I sort of get that point, but I believe that one could define strict categories in HoTT (whose type of object is a set). I believe using a 1-HIT one could define a univalent category from a strict category. Would that construction be completely useless, or would there be interesting properties that can be proved from this and that are not provable directly in univalent categories? Feb 10, 2020 at 11:10

Before I try to answer the question itself, let me make a few preliminary remarks.

Firstly, a minor point: it's not really correct to say that categories are the objects of Ho(Cat), if by Ho(Cat) you mean the homotopy 1-category of Cat; the correct thing to say is that categories are the objects of the 2-category Cat. The point is that in Ho(Cat), whose morphisms are isomorphism classes of functors, you lose the ability to distinguish between multiple isomorphisms between two isomorphic functors.

Secondly, it's perfectly correct, as you say, that there are some operations on things sometimes called "categories" that require treating them up to isomorphism rather than equivalence. But instead of your "precategories", I will call those things "strict categories", to match the nLab and the HoTT Book (of which the latter got the terminology from the former). So Reedy categories and contextual categories are best thought of as strict categories, rather than categories proper.

Thirdly, I would approach the problem of defining a "Reedy non-strict category" somewhat differently. It's true that a given category could be equivalent to a Reedy strict category in more than one way --- but even more than that, it's already true that a given strict category can be Reedy in more than one way! That is, being Reedy is structure on a strict category, not a property of it, and different choices of Reedy structure on the domain can yield different Reedy model structures, even before we start to worry about strictness of categories. So similarly, being Reedy must also be structure of a non-strict category, and once we realize that it is quite natural to say that a Reedy structure on a non-strict category $$C$$ consists of a specified strict category $$C'$$, a specified equivalence $$C\simeq C'$$, and a Reedy structure on $$C'$$. With this definition, a Reedy structure on a non-strict category induces a Reedy model structure in a canonical and equivalence-invariant way. (With that said, there seems relatively little reason to do such a thing, since most naturally-arising Reedy categories are in fact strict. There's nothing wrong with using strict categories, as long as we don't assume that every category is strict.)

Now, your question seems to be roughly "what is wrong with non-equivalence-invariant constructions on categories?" As you say, this is really the same question as "what is wrong with non-isomorphism-invariant constructions on vector spaces?".

The first answer is that in practice we don't keep track of "which equivalent/isomorphic copy" of an object we are using. For instance, the tangent space of a manifold at a point can be defined in many ways, yielding isomorphic but non-equal vector spaces. If we have a construction on vector spaces that is not isomorphism-invariant, then when someone wants to apply that construction to the tangent space of a manifold, we have to ask "which tangent space?" Or, even worse, if we have a construction on groups that is not isomorphism-invariant and someone wants to apply that construction to the two-element group (or even the one-element group!) we have to ask "which one?" The experience of abstract/structural mathematics over the past century strongly suggests that such constructions should not be considered part of linear algebra or group theory. (You seem to believe that such constructions are used in some areas of mathematics, but I would dispute that; can you give examples of the sort of thing you are thinking of?) Essentially the same is true for categories and equivalences.

The second answer, which to my mind is even more powerful, is that only invariant constructions can be generalized to "variable" objects. Consider for instance the notion of vector bundle over a space. Even though we can choose bases for each individual fiber, if the bundle is nontrivial it may not be possible to choose a family of global sections that form a basis at every point simultaneously. Thus, a construction on vector spaces which depends on the choice of basis cannot be performed on vector bundles. Another way of thinking about this is that a vector bundle can be represented by a functor into the groupoid of vector spaces, so any construction on vector spaces that is to be "composed" with such a functor must itself be functorial on the groupoid of vector spaces, i.e. respect isomorphism.

Exactly the same thing is true for categories, although the relevant kind of "variation" also has to be categorified. There are "categorified spaces" and "bundles of categories" over them such that although each individual "fiber" can be presented by some strict category, the entire bundle cannot be simultaneously so presented. Thus, a construction on categories that doesn't respect equivalence, or equivalently that depends on a choice of strict presentation, cannot be performed on such "bundles of categories".

• Re: examples of constructions that aren’t isomorphism-invariant, doesn’t the OP’s example of group presentations fit the bill? Indeed, the whole subject of combinatorial group theory studies groups that have presentations with particular properties. For many of these properties (eg small-cancellation conditions) I don’t know an isomorphism-invariant way of saying them.
– HJRW
Feb 8, 2020 at 4:54
• Thanks a lot, I didn't think about the "bundle of categories" argument, and it makes a lot of sense Feb 8, 2020 at 14:35
• @HJRW the property that "G has a presentation with X property" is isomorphism-invariant. Feb 9, 2020 at 16:25
• Yes, partly. The property "G has a presentation with X property" is isomorphism-invariant. So would you say that "G has a presentation with X property" is part of group theory? And if so, what about its consequences, of the form "If G has a presentatation with X property, then it satisfies Y", where the proof consists in proving an isomoprhism-invariant proposition Y from the given presentation? If these are part of group theory, then is it different for strict categories, shouldn't saying that a category is presented by a given strict category be part of category theory as well? Feb 10, 2020 at 10:58
• @ThibautBenjamin: if I understand you correctly, aren't you just talking about how to define a map out of a quotient (the quotient in question passes from "group presentations with X property" to "groups which have a presentation with X property")? Feb 10, 2020 at 13:22