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?
Best Answer
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".