$$Form \dashv Lang : Hyp \rightarrow FOL$$
We consider an object of $FOL$ to be a signature made of sorts, function symbols and relation symbols, together with a set of axioms of first order logic.
We consider an object of $Hyp$ to be a first order hyperdoctrine formed by a cartesian category $C$ and a functor $C\rightarrow HA'$ where $HA'$ is the category of Heyting algebras with heyting algebra morphisms, with left and right adjoints adjointed (unlucky naming) such that these adjoints satisfy Beck-Chevalley and Frobenius conditions.
The functor $Form$ (assuming we know how to make $FOL$ a category ---I appreciate if someone has a comment on this) on objects constructs the free hyperdoctrine out of a signature and quotients a la Lindebaum.
For that we make $C$ the category of contexts out of our signature, and our functor $F : C \rightarrow HA'$ constructs the free Heyting algebra where $F\ [x_1:\sigma_1,\dots,x_n:\sigma_n]$ is thought of as the set of formulas that depend on $x_1,\dots,x_n$. (And it's easy to see what it does on terms.)
Question:
How do we define $Lang$?
We can consider the arrows of $C$ to be the function symbols of our theory (plus some quotenting), but what about the relation symbols?
Leaving the set of relation symbols empty seems wrong.
You include one relation symbol of sort $X$ for each element of the Heyting algebra $F(X)$.
The arrows in the category FOL are interpretations between theories.