Is there an "intrinsic" way to define categories, to prevent being able to break the principle of equivalence?

Question

The usual way categories are defined we get a set or class of objects. But for most purposes the notion of equivalence we use for categories is equivalence of categories and not isomorphism. This means that the usual way of defining categories comes with extra information that is not intrinsic to the categories themselves: a choice of underlying set of objects. This reminds of how manifolds are sometimes defined as special subsets of $\mathbb R^n$: while we can do all of manifold theory that way, the extra information contained in the choice of embedding is unnecessary and inelegant. This motivates studying manifolds abstractly so that they only come with information intrinsic to the manifold itself. Is there a way to do the same for categories, defining them in some more abstract way so that only information "intrinsic" to the category is kept (as in, information invariant up to equivalence of categories)?

Answer 1

Let me quote a paragraph from Shulman's paper Stack semantic and the comparison of material and structural set theories, starting from the last paragraph on page 11.

The theory of categories can, of course, be formulated in ordinary first-order logic, but this is unsatisfactory because it allows us to discuss equality of objects. We need all our formulas to express “category-theoretic” facts, and thus we must avoid ever asserting that two objects are equal (rather than isomorphic). However, we cannot simply remove the equality predicate on objects from the ordinary first-order theory, because there are situations in which we do need to know that two objects are the same. For example, to compose two arrows f and g, we need to know that the source of g is the same as the target of f.

The solution to this problem, which has seemingly been rediscovered many times (...) is to use a language of dependent types.

The paper then proceeds to describe such a language, and also cites other sources such as Makkai's FOLDS. So this should be exactly what you are looking for. In particular properties of categories which can be formulated in this language are automatically invariant under equivalences. For example, we can express that a category $\mathbb C$ has a terminal object in that language $$\exists t:\mathbb C.\forall y:\mathbb C.\exists !f:\mathbb C(y,t).\top$$ but we can not express that a category $\mathbb C$ has a single object.