For example let us say we are in the setting of cartesian closed categories and the simply typed $\lambda$-calculus. Let $\mathtt{strCCCat}$ denote the $2$-category of strict cartesian closed categories. The $0$-cells are cartesian closed categories together with a choice of all of the relevant structure (terminal objects, finite products and exponentials). The $1$-cells are functors which strictly preserve the structure and the $2$-cells are natural transformations. There is a forgetful functor $\mathtt{strCCCat}\to \mathtt{drGraph}$ which sends such a category to its underlying directed graph. The category of directed graphs may be replaced by other appropiate categories of signatures. We denote the forgetful functor by $\operatorname{Sign}$. When viewed as a $1$-functor it has a left adjoint $\mathcal {Cl}$ which sends a signature $\Sigma$ to the free cartesian closed category $\mathcal {Cl}(\Sigma)$ build from it. It can be build using the simply typed $\lambda$-calculus. There is a natural bijection
\begin{align*} \mathtt{drGraph}(\Sigma, \operatorname{Sign}\mathbb B) = \mathtt{strCCCat}(\mathcal{Cl}(\Sigma), \mathbb B)\end{align*}
But the restriction to 1-cells which strictly preserve the cartesian closed structure on the right hand side seems wrong from the categorical (and from a practical) perspective. Hence one likes to consider the $2$-category $\mathtt{CCCat}$ where the functors only have to preserve the structure in the usual sense, and one likes to look at such functors $\mathcal {Cl}(\Sigma) \to \mathbb B$. Such a functor is only determined up to a canonical isomorphism by its underlying morphism of signatures. When we replace the strict version by the non-strict $\mathtt{CCCat}$ then $\mathcal{Cl}$ has no longer the nice universal property it has before.
I have read somewhere that $\mathcal{Cl}$ is left adjoint to $\operatorname{Sign}: \mathtt{CCCat}\to \mathtt{drGraph}$ in a suitable $2$-categorical sense. I don't know much about $2$-categories unfortunately. Here are my questions. In which sense is $\mathcal {Cl}$ left adjoint to $\operatorname{Sign}$? Does the $2$-categorical notion of adjunction determine $\mathcal{Cl}(\Sigma)$ up to a canonical equivalence of categories?
Edit: The exercises in 1.4 of Mike Shulmanâs Categorical logic from a categorical point of view seem to describe what I want. Also there are lecture notes by John Power, which discuss exactly the same issue.
Best Answer
Let $\mathcal{Doc}$ be a doctrine, such as the 2-category of categories with finite limits, the 2-category of cartesian closed categories or the 2-category of fibrations for higher order logic. Let $\mathbb T$ be a theory which fits to the doctrine. For simplicity let us say that $\mathcal{Doc}$ is the 2-category $\mathcal {Cart}$ of categories with finite limits, left exact functors and natural transformations, and let us say that $\mathbb T$ is a Lawvere theory. For any fixed category $C$ with finite products we get a category $Mod(\mathbb T,C)$ of models in $C$. A model of $\mathbb T$ in $C$ is just an interpretation of the symbols in the signature of $\mathbb T$ such that the axioms of the theory $\mathbb T$ are satisfied. A 2-cell between two models $M$ and $M'$ consists of a morphism $MX\to M'X$ for each sort $X$ in the signature such that diagrams commute. In case of a Lawvere theory there is only one sort. Depending on the doctrine and theory, one has to be a bit careful about what the 2-cells are. For example in case of the doctrine of cartesian closed categories and the simply typed $\lambda$-calculus one can only take the invertible transformations as $2$-cells. But let us stick with Lawvere theories and finite limit categories for a second.
A left exact functor $F:C\to D$ yields a functor $Mod(\mathbb T,C)\to Mod(\mathbb T,D$), and a transformation $\alpha:F\to F'$ yields a transformation $Mod(\mathbb T,F)\to Mod(\mathbb T,F')$. We get a strict 2-functor $Mod(\mathbb T,-):\mathcal {Cart}\to \mathcal {Cat}$. The syntactic category $C_\mathbb T$ of the theory $\mathbb T$ is by definition a representation of the functor $Mod(\mathbb T,-)$. This means it is an object $C_\mathbb T$ from the doctrine (in our case the doctrine of categories with finite limits) together with an equivalence $$\mathcal Cart(C_\mathbb T,-)\simeq Mod(\mathbb T,-)$$ of 2-functors. The 2-Yoneda lemma tells us that there is an equivalence of categories$$ev:2\mathcal{Cat}(\mathcal{Cart},\mathcal {Cat})(\mathbf y(C_\mathbb T), Mod(\mathbb T,-))\to Mod(\mathbb T,C_\mathbb T)$$ and the special model of $\mathbb T$ in $C_\mathbb T$ which we obtain through the 2-Yoneda lemma will be called the universal model $U$ of $\mathbb T$ in its syntactic category $C_\mathbb T$. The 2-Yoneda lemma also tells us how we can reconstruct the equivalence of 2-functors from the universal model. Its $D$th component is, up to an invertible modification, the functor $$\mathcal Cart(C_\mathbb T,D)\simeq Mod(\mathbb T,D)$$ which sends an object $F:C_\mathbb T\to D$ to the model $Mod(\mathbb T,F)(U)$ in $D$. So here is the correct universal property of the syntactic category.
A syntactic category for the theory $\mathbb T$ is a category $C_\mathbb T$ with finite limits together with a model $U\in Mod(\mathbb T,C_\mathbb T)$ such that the transformation $\mathcal Cart(C_\mathbb T, -)\to Mod(\mathbb T,-)$ of 2-functors is in equivalence.
It is in fact sufficient to show that each $D$th component of the transformation is an equivalence in the target $\mathcal{Cat}$. So proving that $U\in Mod(\mathbb T,C_\mathbb T)$ is a universal model amounts to constructing and inverse functor of $\mathcal Cart(C_\mathbb T,D) \to Mod(\mathbb T,D)$ for each $D$, and this is in essence the same as defining the meaning of all terms in the language of $\mathbb T$ relative to a given model by recursion.
Assume now $U\in Mod(\mathbb T, C_\mathbb T)$ and $U'\in Mod(\mathbb T,C'_\mathbb T)$ are two universal models. Then we see that $$\mathcal{Cart}(C_\mathbb T,D) \simeq Mod(\mathbb T, D)\simeq \mathcal{Cart}(C'_\mathbb T,D)$$ 2-naturally in $D$. By the $2$-Yoneda lemma there must be an equivalence in $\mathcal{Cart}(C'_\mathbb T,C_\mathbb T)$ which induces the equivalence of $2$-functors up to an invertible modification. We obtain it by chasing the identity of $C_\mathbb T$. It is the functor $C'_\mathbb T \to C_\mathbb T$ which extends the universal model $U$ in $C_\mathbb T$.