Reference for "topos obtained by adjoining an indeterminate set' theorem

Question

From Lawvere's Continuously variable sets; algebraic geometry = geometric logic:

The following illuminating fact about topoi (long known for the case $\mathsf S$=constant sets) was (conjectured by me and) proved by Gavin Wraith for any base topos having a natural-numbers object.

Theorem 6. Suppose $\mathsf S$ is a topos having a natural-numbers object. Then there is a topos $\mathsf S[T]$ over $\mathsf S$ 'obtained by adjoining an indeterminate set $T$' such that for any topos $\mathsf X$ over $\mathsf S$ there is an equivalence $$\mathsf{Topos}_{/\mathsf S}(\mathsf X,\mathsf S[T])\overset{\simeq}{\longrightarrow}\mathsf X$$of categories (defined by $f\leadsto f^\ast T$). Specifically, $\mathsf S[T]$ is the (internal) functor category $\mathsf S^{\mathbb S_0}$, where $\mathbb S_0$ is a category object in $\mathsf S$ which may be interpreted as the category of finite sets with $\mathbb S_0\overset{T}{\longrightarrow} \mathsf S$ interpreted as the full inclusion.

1. Where can I find a reference for this theorem and its proof?
2. Suppose $\mathsf S=\mathsf{Set}$. What is $T$? Could it be "nothing"? That is, could the equivalence be true without writing $T$ at all? What's the intuition?
3. What are some interesting consequences of this theorem?

Answer 1

Here is some intuition. You can think of the opposite of the 2-category of Grothendieck topoi (that is, a morphism $f : X \to Y$ between topoi is an exact left adjoint) as a categorification of the category of commutative rings, where

1. Colimits categorify addition,
2. Finite limits categorify multiplication, and
3. Sheaves of sets on spaces categorify functions.

(A much more precise statement is that topoi with these morphisms categorify frames, but commutative rings are more familiar in a useful way.) Note, for example, that because topoi are cartesian closed, finite products distribute over colimits.

In this 2-category $\text{Set}$ is the initial object, so it categorifies the commutative ring $\mathbb{Z}$; the whole theory is "$\text{Set}$-linear." This may be clearer if you think of $\text{Set}$ as the topos of sheaves on a point.

$\text{Set}[T]$ then categorifies the polynomial ring $\mathbb{Z}[T]$ - it's the free topos on an object - and what the theorem says is that $\text{Set}[T]$ exists and can be explicitly realized as the functor category $[\text{FinSet}, \text{Set}]$. Loosely speaking, if $F$ is such a functor, the values $F(n)$ it takes on sets of size $n$ (which I am writing just "$n$" by abuse of notation) are the "coefficients" of the corresponding "polynomial." This can be made precise by writing every such functor $F$ as a weighted colimit of representable presheaves on $\text{FinSet}^{op}$ in the usual way, which here looks like (after messing with some $^{op}$s)

$$F(X) \cong \int^{n \in \text{FinSet}} F(n) \times X^n$$

where $X \in \text{FinSet}$. This coend also describes more generally how to compute the image of $F$ under the exact left adjoint $f : \text{Set}[T] \to C$ where $C$ is a topos and $f$ classifies an object $X \in C$; here $F(n) \times X^n$ should be understood as the tensoring, so it refers to $\coprod_{F(n)} X^n$.

(What this shows is that $S[T]$ is somewhat misleading notation for this topos, if the notion of morphism between topoi you're working with is geometric morphisms; it conflates the algebraic (topoi as "commutative rings") and geometric (topoi as "affine schemes") points of view. It would be nice to have two different words for topoi considered in these two senses, analogous to the distinction between affine schemes and commutative rings, and the distinction between locales and frames.)

To start understanding this result, the first observation is that $\text{FinSet}^{op}$ itself has an interesting universal property: it's the free category with finite limits on an object. This is a categorification of the free commutative monoid on a point, namely $\mathbb{N}$, which we then take the free abelian group / monoid ring on to get the free commutative ring on a point; this gets categorified to taking presheaves.

Once you believe this universal property then as mentioned in the comments the desired result follows from Diaconescu's theorem, which you can think of as a categorification of the universal property of the monoid ring.

---

A generalization of this perspective, where we replace cartesian monoidal categories with symmetric monoidal categories, is sometimes called "2-affine algebraic geometry," and is also a generalization of Tannaka duality; see for example Chirvasitu and Johnson-Freyd's The fundamental pro-groupoid of an affine 2-scheme or Brandenburg's Tensor categorical foundations of algebraic geometry.