"Locales and toposes as spaces": categories as theories

I am continuing the last three postings in this blog, and jumping to Section 5.3 of Vickers' text.

One can take a category and interpret it as a predicate theory. All objects A are interpreted as sorts, X_A, and all arrows f : A → B are interpreted as functional symbols, u_f : X_A → X_B.

Then for every object A one imposes an axiom (∀x:X_A) u_idA (x) = x.

And for every pair of morphisms f : A → B, g : B → C one considers the morphism h = g o f and imposes an axiom (∀x:X_A) u_g (u_f (x)) = u_h (x).

One often imposes additional axioms as well. Of course, this is a lot of sorts, functional symbols, and axioms. If one at least wants them to form sets rather than proper classes, one has to start with a small category.

Also we can't assume that objects are sets which have elements, so what would (∀x:X_A) even mean? One can think about this purely formally (until one starts to consider models of the theories), or one can recall from a first post in this series than a generalized point of A is simply a morphism x to A, then f (x) should be thought of as f o x, and one can think about quantifiers ranging over these generalized points.