has there be an effort to categorify first order logic? More particularly, structures in the sense of logic.
If so, then every structure of a first order theory is a category. so in particular, the universe of categories must be a (meta)-category itself. So I have another question: is there a development of a model theory of categorified logic?
The idea is like this. In modern set-theoretic based model theory, must of the interesting stuff comes by looking at different cardinalities. First order theory like Lowenheim-Skolem Theorem makes it easy to move up and down cardinalities, and after all the category SET is equivalent to CARDINALS. Very much this equivalence dictates the model theory.
So the universe of categories CAT, and whatever is a skeletal equivalent of it, will dictate the model theory of categorified logic.
Anyone aware of categorified logic?