Why does the category of definable sets of $T^\mathrm{eq}$ have coproducts?

Question

For each first-order theory $T$ there is an associated weak syntactic category, sometimes also called "the category of definable sets of $T$" and denoted $\mathrm{Def}(T)$.

Also, for each theory $T$ there is an associated theory $T^\mathrm{eq}$ which can be obtained from $T$ by adding quotient sorts for each definable equivalence relation, see e.g. here 2.3.

The nLab claims that $\mathrm{Def}(T^\mathrm{eq})$ has coproducts.

Question: Why? Intuitively, coproducts correspond to the existence of sum types. But in $T^\mathrm{eq}$ we only added quotient types.

Answer 1

In general, a theory is called proper if every sort is nonempty (in every model) and there is a sort which has (in every model) at least two elements. Then we have the following theorem: if $\mathbb{T}$ is any proper theory, the syntactic category of $\mathbb{T}^{eq}$ is a pretopos. This is a consequence of the following (non trivial) theorem, which is a generalization of the result found in [1]: call a coherent category proper if every object is a subobject of a nonempty one and if there is a decidable object $D$ such that $D$ and $\neg D$ are nonempty, where $\neg D$ is the complement of the diagonal $\Delta: D \to D \times D$. Then the theorem says that any proper coherent exact category is a pretopos.

In the case of a classical first-order theory, whose models have at least two elements, the syntactic category of $\mathbb{T}^{eq}$ is an exact coherent category, and it will be proper, since $\mathbb{T}$ is. Hence, it is a pretopos and thus it has disjoint coproducts. In fact, for a proper coherent category, the exact completion and the coproduct completion are equivalent.

[1] Victor Harnik: "Model theory vs. categorical logic: two approaches to pretopos completion". In Bradd Hart et al., editor, Models, logics, and higher-dimensional categories: a tribute to the work of Mihaly Makkai, volume 53 of CRM Proceedings and Lecture Notes. American Mathematical Society, Providence, R.I., 2011.

Answer 2

Although godelian has already given a complete answer to this question, I personally like to see explicit constructions for things like this.

Given two definable sets $D_0$ and $D_1$ (in sorts $S_0$ and $S_1$, respectively), a typical construction of the coproduct (or disjoint union) of $D_0$ and $D_1$ assumes that we have some sort $S_2$ in which there are two distinct definable elements, $a_0$ and $a_1$, but it would be nice to not have to assume that there are any definable elements at all. We could also make our lives easier by assuming that the theory is complete, but we won't. I am, however, going to assume that every sort is always non-empty. If you don't have this assumption, I believe that the coproduct of definable sets can't actually be constructed in a uniform way across varying completions of $T$ in the standard version of $T^{eq}$ (i.e., closing the collection of sorts under products and definable quotients), so if you do want to allow for this possibility, I would recommend just modifying the definition of $T^{eq}$ (either adding an explicit two element sort or adding explicit coproduct sorts).

We need, as in godelian's answer, to assume that every model of the theory $T$ has a sort containing at least two elements. A small compactness argument shows that there is a finite sequence $O_0, \dots,O_{n-1}$ of sorts such that every model of $T$ has at least two elements in $O_i$ for some $i<n$.

A definable set equivalent to the disjoint union of $D_0$ and $D_1$ exists in a quotient of the product sort $P = S_0 \times S_1 \times O_0^2 \times \dots \times O_{n-1}^2$. We'll represent an element of this product sort as a tuple $(x,y,z_0,w_0,z_1,w_1,\dots,z_{n-1},w_{n-1})$ or $(x,y,\bar{z},\bar{w})$, where $z_i$ and $w_i$ are variables of sort $O_i$.

The specific equivalence relation we need is $$E(x,y,\bar{z},\bar{w};x',y',\bar{z}',\bar{w}') \equiv (\bar{z}=\bar{w} \wedge \bar{z}'=\bar{w}' \wedge x = x') \vee (\bar{z}\neq \bar{w} \wedge \bar{z}'\neq \bar{w}' \wedge y = y'),$$ where $\bar{z}=\bar{w}$ is short for $\bigwedge_{i<n} z_i =w_i$ and $\bar{z} \neq \bar{w}$ is short for $\neg(\bar{z}=\bar{w})$.

A little work shows that $E$ is an equivalence relation and that the quotient $P/E$ can be definably identified with $S_0 \sqcup S_1$. Specifically, there are definable injections from $S_0$ and $S_1$ into $P/E$ with disjoint images that cover $P/E$. The coproduct of $D_0$ and $D_1$ can now just be taken to be the union of their images under these injections.