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?