Category Theory with and without Objects

Question

Slight Motivation: In Mac Lane and Freyd's books (the latter being a reprint of an older book called "Abelian Categories") they note that instead of defining any Objects in a category we may define an "arrows only" approach by considering the identity morphism associated to an object to be the object itself.

Question: Is it computationally or syntactically easier in category theory to consider a category as objects and morphisms instead of as just as morphisms? In short, is there a reason we keep objects around?

Answer 1

Category theory without objects is a little easier to formalise as a first-order theory. For instance, here is a first-order formulation of Lawvere's elementary theory of the category of sets, which adopts the strategy of identifying objects with their identity arrows.

That said, I'm not sure category theory without objects is any easier to think about.

Answer 2

From a formalisation-in-a-proof-assistant point of view, I found formalising category theory without objects to be quite horrible, because it is so much easier to have objects which correspond directly to types, rather than objects which are simply special kinds of morphisms.