I'm reading Saunders' book, Categories for the Working Mathematician and I would like to know if there is some formalization of the concept of a 'metacategory' (i.e. a 'system of arrows') without embedding it in set theory (what he calls a 'category'), just an embedding in some kind of natural logic.
A model for a category would be a set of arrows $C$ and a partial binary function $\circ$ (the composition) with the natural axioms. One problem is that the language of First Order Logic cannot express partial functions, just functions. This can be solved in first order logic by the adittion of a binary relation ("$f$ and $g$ can be composable") or just a ternary relation ("the composition of $f$ and $g$ is $h$").
Worse problems appear when you want to consider a logic for category theory. The language of this logic would have many kinds of variables as 'morphisms', 'categories', 'functors'... so that First Order Logic seems unapropiated for category theory. Also, formulas and proofs maybe need the concept of infinite collection of morphisms to talk about limits, coproducts, and First Order Logic only deals with finite formulas.
Does there exist some unifying language for category theory? Are there any good reference?
P.S.: I know set theory is a good model for category theory. But, in that formalization, you have to take care of the 'size' ('small' or 'large') of the category, which for me seems unnecesary and complicates the theory.