On a surprising property of free theories

Question

Yesterday I observed (and proved) the following odd fact, which I found very surprising. I'm very curious to know if this was known by some people, or if it follows from some other more general fact, or if anyone had any kind of comments about it. (for example "this is false" would be a very helpful comment ! ). I hope this is not to vague for MO.

My observation is the following:

$1^{st}$ Version: Let $T$ be a free Lawvere theory (i.e. freely generated by some operation in different arities) then when you see $T$ has a category, and freely add to it an initial object, the resulting category has all finite limits.

One can rephrase this in terms of model:

$2^{nd}$ version : Let $T$ be a free lawvere theory, or (equivalently) a free symmetric set-operad, then let $C$ be the category of free finitely generated model, then $C$ with a freely added terminal object has all finite colimits.

(note: "freely" added terminal object means that it is terminal and it has no morphism out of him except the identity)

In fact, one can obtain the same results far more generally:

$3^{rd}$ version: Let $T$ be a "free" Cartmell generalized algebraic theory. Here free means that it has no equality axioms, only terms and type introduction rules. Then the contextual category of $T$, together with a freely added initial object, has all finite limits.

I would also be interested to know if some example of non-free theory also have this properties (I believe the answer is no, but I don't really know)

---

Maybe I should give an example of those limits to give an idea of how it works, and how 'weird' these limits can be. In fact the following example gives a pretty good idea of how the proof works (though the version for Cartmell theories, or at least the only proof I know, involve a very messy and complicated induction to really makes it into a proof)

Let's look at the the Lawvere theory of "magmas", i.e. the theory with just one operation $m$ of arity $2$. I will look at colimits in the category of free finitely generated magma. Coproducts clearly exists, so I will focus on coequalizer. I denote by $M_k$ the free magma on $k$-generators.

• $M_1 \rightrightarrows M_2$ be the pair of map wich send the generators of $M_1$ to $m(x,y)$ and $m(x,x)$ where $x$ and $y$ are the generators of $M_2$. Then the colimits is $M_1$ where $x$ and $y$ are both sent to the generator of $M_1$. Indeed in a free magma the only way to have $m(f,g)=m(f,f)$ is if $f=g$.

• $M_1 \rightrightarrows M_2$ sending the generator to $m(x,y)$ and $m(x,m(x,x))$. Then the colimit is $M_1$ again, with $x$ being sent to the generator $t$ and $y$ to $m(t,t)$. Indeed in a free magma $m(f,g)=m(f,m(f,f))$ can hapen only if $g=m(f,f)$.

• $M_1 \rightrightarrows M_2$ sending the generator to $m(x,y)$ and $m(x,m(x,y))$ then the colimits is the freely added terminal object. Indeed in a free magma the relation $m(f,m(f,g)) = m(f,g)$ implies $m(f,g)=g$ which can never be satisfied in a free magma (for example by counting the number of $m$ that appears in the unique expression of $g$ in terms of the generators).

• Any colimits involving the freely added terminal object is the freely added terminal object itself (it is the only object that admit a map from it)

Answer 1

This is a consequence of first-order unification. The main issue is the existence of (co)equalizers, since (co)products are trivially seen to exist. Here is a brief explanation of how to translate calculating (co)equalizers into the language of unification. Your three setups have arrows pointing in different directions, I'll pick the colimit direction for simplicity but the reasoning below applies to all three setups equally well.

Work as in your magma examples but in the general case. Think of the generators of the free algebra $F_m$ with $m$-generators as variable symbols $x_1,\ldots,x_m$. Then we can think of morphisms $F_m \to F_n$ as variable substitutions $\{x_1 \mapsto t_1,\ldots,x_m \mapsto t_m\}$, where $t_1,\ldots,t_m$ are terms involving the $n$-variable symbols $y_1,\ldots,y_n$ from $F_n$.

Given a parallel pair $$\sigma =\{x_1 \mapsto s_1,\ldots,x_m \mapsto s_m\}, \tau =\{x_1 \mapsto t_1,\ldots,x_m \mapsto t_m\}:F_m \rightrightarrows F_n,$$ and a $$\upsilon = \{y_1 \mapsto u_1,\ldots,y_n \to u_n\}:F_n \to F_k,$$ we have $\upsilon\circ\sigma = \upsilon\circ\tau$ precisely if $s_1^\upsilon = t_1^\upsilon,\ldots,s_k^\upsilon = t_k^\upsilon$ (where I use superscripts to denote the application of a substitution to a term). In other words, when the substitution $\upsilon$ is a unifier for the unification problem $\{s_1 \doteq t_1,\ldots,s_k \doteq t_k\}$.

It was shown by J. A. Robinson that if the unification problem $\{s_1 \doteq t_1,\ldots,s_k \doteq t_k\}$ has a unifier, then it has a most general unifier $\nu$ in the sense that any other unifier is obtained from $\nu$ by applying a further substitution on top of it. Translating back into the language of category, this means that this $\nu$ is a coequalizer for the parallel pair $\sigma,\tau:F_m \rightrightarrows F_n$. Robinson privided an algorithm to decide whether a unifier exists and to find a most general unifier if there is one. A much more efficient algorithm was later found by Martelli and Montanari.

In response to your final query, yes, there are some non-free theories that allow unification; see Baader and Snyder for some common examples.

Robinson, J. A., A machine-oriented logic based on the resolution principle, J. Assoc. Comput. Mach. 12, 23-41 (1965). ZBL0139.12303.

Martelli, Alberto; Montanari, Ugo, An efficient unification algorithm, ACM Trans. Program. Lang. Syst. 4, 258-282 (1982). ZBL0478.68093.

Baader, Franz; Snyder, Wayne, Unification theory, Robinson, Alan (ed.) et al., Handbook of automated reasoning. In 2 vols. Amsterdam: North-Holland/ Elsevier; 0-444-50812-0 (vol. 2); 0-444-50813-9 (set)). 445-533 (2001). ZBL1011.68126.