In my opinion, a cool definition of "algebraic signature" is as follows:

An algebraic signature on the sort symbols $\mathcal{X} = \{X_0,...,X_{n-1}\}$ is precisely a quiver whose underlying set of vertexes is the free monoid (written $\times,1$) generated by $\mathcal{X}.$

(The idea is that the arrows of the quiver are your function symbols.)

Question. I suspect this definition has been considered already. Is there somewhere I can learn more about it? In particular, I'd like to know if there a slick way of defining models of such a signature in a finite-product category $\mathcal{C}$.

Furthermore, I've been thinking of late that we can move to higher-order logic by replacing the free monoid in the aforementioned definition with something else. In particular, to the signature of monoids (written $\times,1$), adjoin a binary operation symbol $X,Y \mapsto X^Y$ subject to the identities listed here. Call such a structure a DCCC (i.e. a decategorified cartesian closed category). Then we can define the notion of a higher-order algebraic signature in the obvious way.

A higher-order algebraic signature on the sort symbols $\mathcal{X} = \{X_0,...,X_{n-1}\}$ is precisely a quiver whose underlying set of vertexes is the free DCCC generated by $\mathcal{X}.$

Once again, I suspect this definition has been considered before. Is there somewhere I can learn more about it?

-

It seems to me that what you're looking for is a many sorted Lawvere algebraic theory.

In short a (multisorted) algebraic theory is a cartesian category whose objects are exactly the elements of a free monoid generated by some objects whose multiplication is the cartesian product.

Models of a such theory $\mathbf T$ can be considered in every product category: an $\mathcal S$-model of a theory (in this sense) is just a product preserving functor from the theory $\mathbf T$ to the category $\mathbf S$.

Of course natural transformation play an important role in this context being the (homo)morphisms of models.

As you suspected this approach can be further extended to more general theories, in particular to first order theories through the concept of elementary topos (a concept also due to Lawvere).

A topos is a sort of generalized category of sets well adapted for do semantics of a first order language/logic.

You can find much more in the nlab or in many different book (whose reference can be find to nlab too).

Some of this stuff can be found in Borceaux's "Handbook of categorical algebra", but in a very superficial way (at least in my opinion).

Another reference which seems more adapted could be (in my opinion) Barr and Wells' book "Topos Triples and Theories" which free downloadable as a reprint in Theory and application of Categories. In this books theories are defined as structured categories and models are defined as structure preserving functors.

A final reference is Johnstone "Sketches of an elephant" which I think is the most complete on the subject, although it treats theories in a syntactic way (i.e. a sets of formulas) and defines models for such syntactic theories in categories.

As for last comment there's also lot of stuff about the subject on the internet some key words for doing a search are categorical logic, topos theory, algebraic theory and Lawvere.

-