# 2-categorical universal property of the classifying category of a type theory

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.

• Do you remember where you read that $\mathcal Cl$ is left adjoint to $\text{Sign}$? Also, what is $\mathbb B$? May 16, 2022 at 4:21
• @Couchy For example in Categorical logic from a categorical perspective by Mike Shulman. mikeshulman.github.io/catlog/catlog.pdf Theorem 1.4.13 states the analogue for finite product categories.
– Nico
May 16, 2022 at 6:09
• @Couchy actually the exercises seem to describe how I can obtain a suitable 2 categorical universal property. But I am a bit lost because 2 categories have so many definitions and axioms and diagrams.
– Nico
May 16, 2022 at 6:13
• @Couchy $\mathbb B$ is a variable for an arbitrary Cartesian closed category.
– Nico
May 16, 2022 at 6:33
• You might have more luck if you ask about a specific exercise. I'm having a hard time understanding what this question is asking. It might also be useful to generalize, and attempt this question with respect to the adjunction between categories and graphs, ie. "Does the 2-categorical notion of adjunction determine a free category on a graph up to canonical equivalence of categories?" May 18, 2022 at 14:49

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$$.