I'm reading Pitts' Categorical logic and I'm having a hard time with some basic things.
My goal is to construct the classifying category and give its universal property, but I wanted to understand a bit more of what is happening underneath, categorically speaking, if that makes sense.
The theorem plus my understanding of what the universal property would look like in a diagram reads like this:
(Here $G$ is the generic model and $\mathcal Cl(Th)$ is the classifying category of a theory $Th$.)
The problem is that what I wrote as $Terms$ is not actually a category, it's something weaker.
At first I thought it was a multicategory, and that seems fine, and if that was correct, it looks like this universal property was that of the adjunction $Multicat \rightarrow StrMonCat \dashv StrMonCat \rightarrow Multicat$.
The problem is that just with multicategories, we don't seem to be able to write terms that repeat a variable, say $f(x,x)$. We can only do $f(x,y)$. (Always thinking up to $\alpha$-equivalence.)
So what is actually the structure necessary?
The book defines a structure in $\mathcal C$ ---a cartesian category--- for a given signature $Sg$ as mapping each sort to an object in $\mathcal C$ and each function symbol to an arrow in $\mathcal C$ with the appropiate domain and codomain. It never speaks of a functor (which should be product-preserving) because $Sg$ is not a category.
Then says that this extends to well-formed terms by induction, and says nothing else.
A model is one such mapping that also satisfies the axioms of your theory.
It's clear to me that a signature would be a quiver (or "multiquiver" if you want, i.e: the source map has as codomain lists of objects instead of just an object).
But then in what type of category-like structure should we think terms live in? It should have an adjunction with $StrMonCat$ as above.
Any ideas? Thanks in advance!