So it says in the nlab page of doctrine.
Let's focus on first order theories for simplicity.
I have two questions, one regarding vertical categorification and another regarding horizontal categorification.
My final goal would be to understand first order hyperdoctrines as a vertical categorification of first order theories with possibly some extra conditions.
First I would like to write the vertical categorification of 'first order theory' down explicitly to see how it looks like, but if our definition of vertical categorification is $$(\text{Sets}\mapsto\text{Categories},\ \text{Elements}\mapsto\text{Objects},\ \text{Functions}\mapsto\text{Functors},\ \text{Equalities}\mapsto\text{Natural Isomorphisms})$$ then I don't understand how to write down a theory as sets with functions and equalities in a suitable manner.
Would we have a 'category of terms' and a 'category of formulas'?? What would these be?
(I remember seeing in some talk a monadic interpretation of 'theory', but I'm not finding any source of that right now. I put this in parenthesis because I don't want to overcomplicate things if a direct approach exists that resembles more the usual definition of theory that one sees in an introductory logic course.)
Secondly, it is common to consider first order hyperdoctrines as generalizations of many-sorted first order logic, not of the usual first order logic.
Is many-sorted logic the horizontal categorification of one-sorted logic?
This would mean thinking of first order logic as a one object category of some sort. (Where its one object would be its only sort.)
(This kind of works but predicates thought of as subobjects don't seem to work very well or at least I don't understand them.)
I feel understanding this would also help with the first question if the answer was positive.
