Category Theory with and without Objects

soft-question category-theory

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.


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.

Related

Field Extension
What's the connection between the Laplace transform and the Fourier transform?
Homology of punctured projective space
Example of a rational function such that : $(f(x))^{3} + (g(x))^{3} + (h(x))^{3}=x$
Restriction to a normal subgroup
When can one expect a classical solution of a PDE?
Algorithm to sort based on a partial order
Non-standard geometry problem
Dominated convergence problems with Wald's identity for the Brownian Motion
Why is a matrix $A\in \operatorname{SL}(2,\mathbb{R})$ with $|\operatorname{tr}(A)|<2$ conjugate to a matrix of the following form?
Example of Sufficient and Insufficient Statistic?
Computing $\lim\limits_{n\to\infty} \int_{0}^{\infty}\frac{\sin(x/n)}{(1+x/n)^{n}}\, dx$