# Ultrafilters, finite coproducts and locally
connected classifying toposes

Richard Garner  Centre of Australian Category Theory, Macquarie University,
NSW 2109, Australia<EMAIL_ADDRESS>
(Date: 2nd September 2024)

###### Abstract.

We prove a single category-theoretic result encapsulating the notions of
ultrafilters, ultrapower, ultraproduct, tensor product of ultrafilters, the
Rudin–Kiesler partial ordering on ultrafilters, and Blass’s category of
ultrafilters $\mathcal{UF}$. The result in its most basic form states that the
category $\mathsf{FC}(\mathrm{\mathcal{S}et},\mathrm{\mathcal{S}et})$ of
finite-coproduct-preserving endofunctors of $\mathrm{\mathcal{S}et}$ is
equivalent to the presheaf category $[\mathcal{UF},\mathrm{\mathcal{S}et}]$.
Using this result, and some of its evident generalisations, we re-find in a
natural manner the important model-theoretic _realisation_ relation between
$n$-types and $n$-tuples of model elements; and draw connections with Makkai
and Lurie’s work on conceptual completeness for first-order logic via
_ultracategories_.

As a further application of our main result, we use it to describe a first-
order analogue of Jónsson and Tarski’s _canonical extension_. Canonical
extension is an algebraic formulation of the link between Lindenbaum–Tarski
and Kripke semantics for intuitionistic and modal logic, and extending it to
first-order logic has precedent in the _topos of types_ construction studied
by Joyal, Reyes, Makkai, Pitts, Coumans and others. Here, we study the closely
related, but distinct, construction of the _locally connected classifying
topos_ of a first-order theory. The existence of this is known from work of
Funk, but the description is inexplicit; ours, by contrast, is quite concrete.

###### 2000 Mathematics Subject Classification:

Primary:

The support of Australian Research Council grants DP160101519 and FT160100393
is gratefully acknowledged. Thanks also to the referees and the editor for
helpful and constructive suggestions, which have improved the paper
significantly.

##  1\. Introduction

_Ultrafilters_ are important in many areas of mathematics, from Ramsey theory,
to topological dynamics, to universal algebra; see [7] for an overview. Around
the notion of ultrafilter is a circle of associated concepts: the ultrapower
of a set by an ultrafilter, or more generally, the ultraproduct of a family of
sets [17]; the tensor product of ultrafilters [30] and the more general
indexed sum; and the Rudin–Keisler partial ordering on ultrafilters, first
written down by Blass in [5] and immediately enhanced to a category of
ultrafilters.

Of course, ultrafilters are particularly important in model theory. One aspect
of this is that complete $n$-types of a first-order theory $\mathbb{T}$ are
precisely ultrafilters on the Lindenbaum–Tarski algebra of $\mathbb{T}$
extended by $n$ new constants; in particular, each $n$-tuple of elements of a
$\mathbb{T}$-model has an associated complete $n$-type, and this realisation
relation between $n$-tuples and $n$-types is central to many questions in
model theory.

Ultrafilters also provide the link between the semantics for modal logic
valued in modal algebras (Boolean algebras with operators), and the Kripke
semantics; indeed, the canonical Kripke model associated to a modal algebra
$B$ takes its frame of possible worlds to comprise exactly the ultrafilters on
$B$. A similar relation holds between the Lindenbaum–Tarski and Kripke
semantics for intuitionistic propositional logic [46, §2.6]; and these
relations have been expressed algebraically via Jónsson and Tarski’s notion of
_canonical extension_ [27, 21]. Canonical extension has been generalised from
propositional to first-order logic via the _topos of types_ construction
studied by Joyal and Reyes [29], Makkai [38] and Pitts [44]—and again,
ultrafilters play a key role.

Another key use of ultrafilters in model theory is via Łos’ theorem that the
models of a first-order theory $\mathbb{T}$ are closed under ultraproducts.
This is useful in its own right, for example in constructing saturated models,
but has also been exploited more structurally by Makkai [40] and Lurie [35]:
they prove a “conceptual completeness” theorem which can reconstruct a first-
order theory $\mathbb{T}$ (or at least, its completion
$\mathbb{T}^{\mathsf{eq}}$ under elimination of imaginaries) from the category
of models and elementary embeddings, together with the ultraproduct structure
on this category.

The objective of this paper is to describe a single category-theoretic result
from which the notions of ultrafilter, ultrapower, tensor product of
ultrafilters, and Blass’s category $\mathcal{UF}$ of ultrafilters, together
with their interrelations, all flow naturally—and which, with only a little
more effort, is able to speak towards the applications of ultrafilters in
model theory described above. This result, which is Theorem 13 and Corollary
14 below, may be stated as follows:

######  Theorem.

The category $\mathsf{FC}(\mathrm{\mathcal{S}et},\mathrm{\mathcal{S}et})$ of
finite-coproduct-preserving endofunctors of $\mathrm{\mathcal{S}et}$ is
equivalent to the category $[\mathcal{UF},\mathrm{\mathcal{S}et}]$ of functors
on Blass’ category [5] of ultrafilters $\mathcal{UF}$. Under this equivalence,
the ultrapower functor $({\mathord{\text{--}}})^{\mathcal{U}}$ corresponds to
the representable functor at the ultrafilter ${\mathcal{U}}$.

This builds on Börger’s characterisation [9] of the functor
$\beta\colon\mathrm{\mathcal{S}et}\rightarrow\mathrm{\mathcal{S}et}$, which
sends a set $X$ to its set of ultrafilters, as the terminal finite-coproduct-
preserving endofunctor of $\mathrm{\mathcal{S}et}$. (Though it will not play
any role here, we should also mention [32]’s different characterisation of
$\beta$ as the _codensity monad_ of the inclusion functor
$\mathrm{\mathcal{F}in{\mathcal{S}}et}\hookrightarrow\mathrm{\mathcal{S}et}$;
see [34] for a modern account.)

One way of seeing our result is that once we know what a finite coproduct-
preserving endofunctor of $\mathrm{\mathcal{S}et}$ is, everything else is
forced. The ultrapower endofunctors of $\mathrm{\mathcal{S}et}$ arise as the
projective indecomposable objects in
$\mathsf{FC}(\mathrm{\mathcal{S}et},\mathrm{\mathcal{S}et})$, and the full
subcategory they span is equivalent to $\mathcal{UF}^{\mathrm{op}}$. Moreover,
as we will see in Proposition 16, the composition monoidal structure on
$\mathsf{FC}(\mathrm{\mathcal{S}et},\mathrm{\mathcal{S}et})$ restricts to this
subcategory, and in this way recovers the tensor product of ultrafilters.

One thing this theorem does not capture is the notion of ultraproduct. For
this, we require a generalisation of the theorem dealing with ultrafilters not
on sets, but on objects of a category ${\mathcal{C}}$ which is _extensive_
[12], meaning that it has well-behaved finite coproducts. In this context, an
ultrafilter on $X\in{\mathcal{C}}$ can be defined as an ultrafilter on the
Boolean algebra of coproduct summands of $X$, giving rise to a category
$\mathcal{UF}_{\mathcal{C}}$ generalising Blass’ $\mathcal{UF}$. We now obtain
the following natural generalisation of our main theorem, to be proved as
Theorem 22:

######  Theorem.

Let ${\mathcal{C}}$ be extensive. The category
$\mathsf{FC}({\mathcal{C}},\mathrm{\mathcal{S}et})$ of finite-coproduct-
preserving functors from ${\mathcal{C}}$ to $\mathrm{\mathcal{S}et}$ is
equivalent to the functor category
$[\mathcal{UF}_{\mathcal{C}},\mathrm{\mathcal{S}et}]$.

As we will see in Section 4.2, we may recapture ultraproducts from this
theorem by taking ${\mathcal{C}}=\mathrm{\mathcal{S}et}^{X}$, yielding an
equivalence
$[\mathcal{UF}_{\mathrm{\mathcal{S}et}^{X}},\mathrm{\mathcal{S}et}]\simeq\mathsf{FC}(\mathrm{\mathcal{S}et}^{X},\mathrm{\mathcal{S}et})$;
now the ultraproduct functors
$\Pi_{\mathcal{U}}\colon\mathrm{\mathcal{S}et}^{X}\rightarrow\mathrm{\mathcal{S}et}$
correspond under this equivalence to suitable representable functors in
$[\mathcal{UF}_{\mathrm{\mathcal{S}et}^{X}},\mathrm{\mathcal{S}et}]$.

A second application, described in Section 4.3, takes ${\mathcal{C}}$ to be
the _classifying Boolean pretopos_ of a theory $\mathbb{T}$ of classical
first-order logic, which plays the same role for a first-order theory as does
the Lindenbaum–Tarski algebra of a propositional theory. In this case,
ultrafilters on $A\in{\mathcal{C}}$ correspond to model-theoretic types in
context $A$, and our result allows us to reconstruct a categorical treatment
of these [38]. Indeed, by the classifying property of ${\mathcal{C}}$, models
of $\mathbb{T}$ correspond to pretopos morphisms
${\mathcal{C}}\rightarrow\mathrm{\mathcal{S}et}$. As pretopos morphisms
preserve finite coproducts, the theorem thereby associates to each
$\mathbb{T}$-model $M$ a functor
$\mathcal{UF}_{\mathcal{C}}\rightarrow\mathrm{\mathcal{S}et}$—whose values
pick out the sets of $M$-elements that realise each type.

Our main theorem can be generalised further by varying the codomain category
as well as the domain category. Recall that a _Grothendieck topos_ is the
category of sheaves on a small site, and that a Grothendieck topos
${\mathcal{E}}$ is _locally connected_ when the left adjoint
$\Delta\colon\mathrm{\mathcal{S}et}\rightarrow{\mathcal{E}}$ of its global
sections functor
$\Gamma={\mathcal{E}}(1,{\mathord{\text{--}}})\colon{\mathcal{E}}\rightarrow\mathrm{\mathcal{S}et}$
has a further left adjoint
$\pi_{0}\colon{\mathcal{E}}\rightarrow\mathrm{\mathcal{S}et}$. The second
generalisation of our main theorem, to be proved as Theorem 26 below, is now:

######  Theorem.

Let ${\mathcal{C}}$ be extensive and ${\mathcal{E}}$ a locally connected
Grothendieck topos. The category $\mathsf{FC}({\mathcal{C}},{\mathcal{E}})$ of
finite-coproduct-preserving functors from ${\mathcal{C}}$ to ${\mathcal{E}}$
is equivalent to the functor category
$[\mathcal{UF}_{\mathcal{C}},{\mathcal{E}}]$.

One application of this theorem, described in Section 5.2, allows us to
reconstruct the indexed sum of ultrafilters. For any sets $X$ and $Y$, our
theorem yields an equivalence
$\mathsf{FC}(\mathrm{\mathcal{S}et}^{X},\mathrm{\mathcal{S}et}^{Y})\simeq[\mathcal{UF}_{\mathrm{\mathcal{S}et}^{X}},\mathrm{\mathcal{S}et}^{Y}]$,
and we define a _generalised ultraproduct_ functor
$\mathrm{\mathcal{S}et}^{X}\rightarrow\mathrm{\mathcal{S}et}^{Y}$ to be one
that corresponds under this equivalence to a pointwise representable functor
$\mathcal{UF}_{\mathrm{\mathcal{S}et}^{X}}\rightarrow\mathrm{\mathcal{S}et}^{Y}$.
Such functors have a representation as _ultraspans_ : that is, as diagrams

(1.1)
$\textstyle{M\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{f}$$\scriptstyle{(g,{\mathcal{U}})}$$\textstyle{X}$$\textstyle{Y}$

with left leg a function $f$ and right leg a function $g$ endowed with an
ultrafilter ${\mathcal{U}}_{y}$ on each fibre $g^{-1}y$. Moreover, it turns
out that generalised ultraproduct functors are closed under composition, so
inducing a composition law on ultraspans (1.1) which encodes perfectly the
indexed sum of ultrafilters.

Another potential application of the above theorem, sketched in Remark 32, is
to Makkai’s _ultracategories_ [40]. An ultracategory is a category
${\mathcal{C}}$ endowed with abstract ultraproduct functors
$\Pi_{\mathcal{U}}\colon{\mathcal{C}}^{X}\rightarrow{\mathcal{C}}$ together
with interpretations for any “definable map between ultraproducts”—the
_ultramorphisms_ of [40]. The key example of an ultracategory is the category
of models of a coherent theory $\mathbb{T}$ in intuitionistic first-order
logic, and [40]’s main result shows that, to within Morita equivalence,
$\mathbb{T}$ can be reconstructed from its ultracategory of models.

We expect to relate ultracategories to our main result via the machinery of
_enriched categories_ [31, 47]. We have calculated far enough to convince
ourselves that categories endowed with abstract ultraproduct functors can be
identified with certain categories enriched over the _bicategory_
$\mathsf{FC}_{\mathrm{\mathcal{S}et}}$ of finite-coproduct-preserving functors
between powers of $\mathrm{\mathcal{S}et}$ which admit certain copowers (a
kind of enriched colimit). The key point is that, in proving this, we exploit
the equivalences
$\mathsf{FC}(\mathrm{\mathcal{S}et}^{X},\mathrm{\mathcal{S}et}^{Y})\simeq[\mathcal{UF}_{\mathrm{\mathcal{S}et}^{X}},\mathrm{\mathcal{S}et}^{Y}]$
established above. We will develop this line of thought further in future
work.

Our final main result exploits the preceding theorems to construct the
_locally connected classifying topos_ of a suitable pretopos ${\mathcal{C}}$.
This construction is similar to the _toposes of types_ mentioned above [29,
38, 44], in that it provides a first-order analogue to the operation of
canonical extension [27, 21] on propositional theories. The existence of
locally connected classifying toposes follows from [18]; however, the
existence proof given there is somewhat inexplicit. We will improve on this by
showing that any small pretopos satisfying the _De Morgan_ property (recalled
in Definition 38 below) has a locally connected classifying topos given by the
topos of sheaves on $\mathcal{UF}_{\mathcal{C}}$ for a certain Grothendieck
topology, related to one found in [29]. Our final main result, proved as
Theorem 42 below, is thus:

######  Theorem.

Let ${\mathcal{C}}$ be a small De Morgan pretopos. The topos
$\mathrm{\mathcal{S}h}({\mathcal{UF}_{\mathcal{C}}})$ is a locally connected
classifying topos for ${\mathcal{C}}$, and is itself De Morgan.

While we discuss briefly the similarities and differences between this
construction, and the various toposes of types in the literature, we will,
once again, leave a more detailed comparison to future work.

##  2\. Background

###  2.1. Ultrafilters, ultraproducts and ultrapowers

In this section, we recall the notions that our main theorem is designed to
capture and their interrelations with each other. Before starting on this, we
first establish some notational conventions for indexed families which will be
used throughout the paper.

######  Definition 1.

Let $Y=(Y(x)\mid x\in X)$ be an $X$-indexed family of sets. We write $(\Sigma
x\,\mathord{\in}\,X)\,\\!Y(x)$ or more briefly $X.Y$ for the indexed sum of
this family, that is, the set of pairs $\\{\,(x,y):x\in X,y\in Y(x)\,\\}$. We
write $\pi_{Y}\colon X.Y\rightarrow X$ for the first projection map, and call
this map _the display family associated to $Y$_. We also write $(\Pi
x\,\mathord{\in}\,X)\,\\!Y(x)$ for the indexed product of the $Y(x)$’s: that
is, the set of functions $f\colon X\rightarrow X.Y$ which are sections of
$\pi_{Y}\colon X.Y\rightarrow X$.

More generally, a _display family over $X$_ is any function $\pi\colon
E\rightarrow X$, and the _$X$ -indexed family associated to $\pi$_ is the
family of fibres $(\pi^{-1}(x)\mid x\in X)$. As is well known, the passage
between $X$-indexed families and display families over $X$ underlies an
equivalence of categories

(2.1) $\mathrm{\mathcal{S}et}^{X}\simeq\mathrm{\mathcal{S}et}/X\hbox to0.0pt{
.\hss}$

This equivalence and its generalisations will play an important role in this
paper.

######  Definition 2.

An _ultrafilter_ on a set $X$ is a Boolean algebra homomorphism
$u\colon{\mathcal{P}}X\rightarrow 2$. Most often, we describe $u$ by
specifying the subset ${\mathcal{U}}=u^{-1}(\top)$ of ${\mathcal{P}}X$; so an
ultrafilter is equally a collection ${\mathcal{U}}$ of subsets of $X$ such
that:

  1. (i)

$X\in{\mathcal{U}}$, and $U\cap
V\in{\mathcal{U}}\Longleftrightarrow(U\in{\mathcal{U}}\text{ and
}V\in{\mathcal{U}})$;

  2. (ii)

$\bot\notin{\mathcal{U}}$, and $U\cup
V\in{\mathcal{U}}\Longleftrightarrow(U\in{\mathcal{U}}\text{ or
}V\in{\mathcal{U}})$.

Equivalently, we may replace condition (ii) with:

  1. (ii)′

$U\in{\mathcal{U}}\Longleftrightarrow X\setminus U\notin{\mathcal{U}}$.

We write $\beta X$ for the set of ultrafilters on the set $X$.

The _principal ultrafilter_ at $x\in X$ is $\mathord{\uparrow}x=\\{U\subseteq
X:x\in U\\}$. These are the only ultrafilters we can write down explicitly;
indeed, the existence of non-principal ultrafilters is a choice principle,
slightly weaker than the axiom of choice [23].

It is often useful to view ultrafilters as generalised quantifiers. Given a
predicate $\varphi(x)$ depending on $x\in X$ and an ultrafilter
${\mathcal{U}}$ on $X$, we write
$(\forall_{\mathcal{U}}x\,\mathord{\in}\,X)\,\\!\varphi(x)$ to indicate that
$\\{x\in X:\varphi(x)\\}\in{\mathcal{U}}$ and say that “for
${\mathcal{U}}$-almost all $x$, $\varphi(x)$ holds”.

######  Definition 3.

Let ${\mathcal{U}}\in\beta X$. If $Y$ is a set, then the _ultrapower_
$Y^{\mathcal{U}}$ is the set of $=_{\mathcal{U}}$-equivalence classes of
partial functions $X\rightharpoonup Y$ defined on a set in ${\mathcal{U}}$,
where

(2.2)
$f=_{\mathcal{U}}g\qquad\text{iff}\qquad(\forall_{\mathcal{U}}x\,\mathord{\in}\,X)\,\\!f(x)\equiv
g(x)\hbox to0.0pt{ .\hss}$

Here we write $f(x)\equiv g(x)$ to mean “$f$ and $g$ are defined at $x$ and
are equal”.

More generally, if $Y$ is an $X$-indexed family of sets, then the
_ultraproduct_ $(\Pi_{\mathcal{U}}x\,\mathord{\in}\,X)\,\\!Y(x)$ is the set of
$=_{\mathcal{U}}$-equivalence classes of partial sections, defined on a set in
${\mathcal{U}}$, of $\pi_{Y}\colon X.Y\rightarrow X$. Note that
$Y^{\mathcal{U}}=(\Pi_{\mathcal{U}}x\,\mathord{\in}\,X)\,\\!Y$.

We can take a topological view on ultraproducts. Given an $X$-indexed family
$Y$, we can view the projection $(\Sigma
x\,\mathord{\in}\,X)\,\\!Y(x)\rightarrow X$ as a local homeomorphism between
discrete spaces. Pushing this forward along the embedding $X\rightarrow\beta
X$ of $X$ into its Stone–Cěch compactification yields a local homeomorphism
over $\beta X$, whose fibre over an ultrafilter ${\mathcal{U}}\in\beta X$ is
the ultraproduct $(\Pi_{\mathcal{U}}x\,\mathord{\in}\,X)\,\\!Y(x)$.

The explicit formula for pushforward of local homeomorphisms—in terms of germs
of local sections—yields the following reformulation of ultrapowers and
ultraproducts in terms of colimits; herein, we view ${\mathcal{U}}$ as a poset
ordered by inclusion:

(2.3) $\displaystyle\ Y^{\mathcal{U}}$
$\displaystyle=\operatorname{colim}_{U\in{\mathcal{U}}}Y^{U}$
$\displaystyle(\Pi_{\mathcal{U}}x\,\mathord{\in}\,X)\,\\!Y(x)$
$\displaystyle=\operatorname{colim}_{U\in{\mathcal{U}}}(\Pi
x\,\mathord{\in}\,U)\,\\!Y(x)\hbox to0.0pt{ .\hss}$

This description makes it clear that ultraproduct and ultrapower are functors
$({\mathord{\text{--}}})^{\mathcal{U}}\colon\mathrm{\mathcal{S}et}\rightarrow\mathrm{\mathcal{S}et}$
and
$\Pi_{\mathcal{U}}\colon\mathrm{\mathcal{S}et}^{X}\rightarrow\mathrm{\mathcal{S}et}$
respectively.

###  2.2. The category of ultrafilters

Given ultrafilters ${\mathcal{U}}$ on $X$ and ${\mathcal{V}}$ on $Y$, we say
that $f\colon X\rightarrow Y$ is _continuous_ if $V\in{\mathcal{V}}$ implies
$f^{-1}(V)\in{\mathcal{U}}$. By axiom (ii)′ and the fact that $f^{-1}$
preserves complements, this is equally the condition that

(2.4) $V\in{\mathcal{V}}\Longleftrightarrow f^{-1}(V)\in{\mathcal{U}}\hbox
to0.0pt{ .\hss}$

The continuous maps play an important role in two natural categories of
ultrafilters, originally defined in [30, 33] in the more general context of
_filters_.

######  Definition 4.

The category $\mathcal{UE}$ of ultrafilters has pairs
$(X\in\mathrm{\mathcal{S}et},{\mathcal{U}}\in\beta X)$ as objects, and as maps
$(X,{\mathcal{U}})\rightarrow(Y,{\mathcal{V}})$ the continuous maps
$X\rightarrow Y$. The category $\mathcal{UF}$ of ultrafilters has the same
objects, and as morphisms $(X,{\mathcal{U}})\rightarrow(Y,{\mathcal{V}})$ the
$=_{\mathcal{U}}$-equivalence classes of partial continuous maps
$X\rightharpoonup Y$ defined on a set in ${\mathcal{U}}$.

Our naming reflects that $\mathcal{UF}$ is the “good” category of ultrafilters
and $\mathcal{UE}$ just a preliminary step to get there; for indeed,
$\mathcal{UF}$ arises by inverting the class ${\mathcal{M}}$ of continuous
injections in $\mathcal{UE}$. The proof of this fact given below mirrors that
given in [6, Theorem 16] for the category of filters; in its statement,
$\iota\colon\mathcal{UE}\rightarrow\mathcal{UF}$ is the identity-on-objects
functor taking $f$ to its $=_{\mathcal{U}}$-equivalence class.

######  Proposition 5.

$\iota\colon\mathcal{UE}\rightarrow\mathcal{UF}$ exhibits $\mathcal{UF}$ as
$\mathcal{UE}[{\mathcal{M}}^{-1}]$.

###### Proof.

Each map in ${\mathcal{M}}$ factors as an isomorphism followed by a continuous
subset inclusion; whence
$\mathcal{UE}[{\mathcal{M}}^{-1}]=\mathcal{UE}[{\mathcal{I}}^{-1}]$ where
${\mathcal{I}}$ is the class of all continuous subset inclusions in
$\mathcal{UE}$. It is easy to see that any map in ${\mathcal{I}}$ is of the
form

(2.5)
$m_{WY}\colon(W,\left.{{\mathcal{V}}}\right|_{W})\hookrightarrow(Y,{\mathcal{V}})$

where $W\in{\mathcal{V}}$ and $\left.{{\mathcal{V}}}\right|_{W}=\\{U\subseteq
W:U\in{\mathcal{V}}\\}$. Such maps are stable under composition and contain
the identities. Moreover, given a map (2.5) and
$f\colon(X,{\mathcal{U}})\rightarrow(Y,{\mathcal{V}})$ in $\mathcal{UE}$, we
have a commuting square (in fact a pullback) in $\mathcal{UE}$ of the form

$\textstyle{{(f^{-1}(W),\left.{{\mathcal{U}}}\right|_{f^{-1}W})}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{m_{f^{-1}W,X}}$$\textstyle{{(W,\left.{{\mathcal{V}}}\right|_{W})}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{m_{WY}}$$\textstyle{{(X,{\mathcal{U}})}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{f}$$\textstyle{{(Y,{\mathcal{V}})}}$

since $f^{-1}(W)\in{\mathcal{U}}$ by continuity of $f$. So ${\mathcal{I}}$
satisfies the first three of the four axioms for a calculus of right fractions
[19], and satisfies the final one trivially since it is a class of
monomorphisms. We may thus describe the localisation
$\mathcal{UE}[{\mathcal{I}}^{-1}]$ as follows. Objects are those of
$\mathcal{UE}$, and maps $(X,{\mathcal{U}})\rightarrow(Y,{\mathcal{V}})$ are
spans in $\mathcal{UE}$ as to the left below, with two such spans being
identified if they can be completed to a commuting diagram as to the right.

$\textstyle{(U,\left.{{\mathcal{U}}}\right|_{U})\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{m_{UX}}$$\scriptstyle{f}$$\textstyle{(X,{\mathcal{U}})}$$\textstyle{(Y,{\mathcal{V}})}$
---
$\textstyle{(U,\left.{{\mathcal{U}}}\right|_{U})\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{m_{UX}}$$\scriptstyle{f}$$\textstyle{(X,{\mathcal{U}})}$$\textstyle{(W,\left.{{\mathcal{U}}}\right|_{W})\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{m_{WU}}$$\scriptstyle{m_{WV}}$$\textstyle{(Y,{\mathcal{V}})}$$\textstyle{(V,\left.{{\mathcal{U}}}\right|_{V})\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{m_{VX}}$$\scriptstyle{g}$

Clearly these maps correspond to $=_{\mathcal{U}}$-equivalence classes of
partial continuous functions; moreover, under this identification, the
identity-on-objects functor
$\mathcal{UE}\rightarrow\mathcal{UE}[{\mathcal{I}}^{-1}]$ sends $f$ to
$(1,f)$, whence $\mathcal{UF}\cong\mathcal{UE}[{\mathcal{I}}^{-1}]$ under
$\mathcal{UE}$ as desired. ∎

###  2.3. Tensor product and indexed sum of ultrafilters

The _tensor product_ of ultrafilters is sometimes called the _product_. It is
most easily expressed in terms of generalised quantifiers.

######  Definition 6.

Let ${\mathcal{U}}$ and ${\mathcal{V}}$ be ultrafilters on $X$ and $Y$. The
_tensor product_ ${\mathcal{U}}\otimes{\mathcal{V}}$ is the unique ultrafilter
on $X\times Y$ which for all predicates $\varphi$ on $X\times Y$ satisfies:

(2.6) $(\forall_{{\mathcal{U}}\otimes{\mathcal{V}}}(x,y)\,\mathord{\in}X\times
Y)\varphi(x,y)\qquad\Longleftrightarrow\qquad(\forall_{{\mathcal{U}}}x\,\mathord{\in}X)(\forall_{{\mathcal{V}}}y\,\mathord{\in}Y)\varphi(x,y)\hbox
to0.0pt{ .\hss}$

Instantiating $\varphi$ at the characteristic predicates of subsets
$A\subseteq X\times Y$ yields the following explicit formula, wherein we write
$x^{*}A$ for $\\{y\in Y:(x,y)\in A\\}$:

${\mathcal{U}}\otimes{\mathcal{V}}=\\{A\subseteq X\times Y:\\{x\in
X:x^{*}A\in{\mathcal{V}}\\}\in{\mathcal{U}}\\}\hbox to0.0pt{ .\hss}$

Using this formula, we see that if
$f\colon(X,{\mathcal{U}})\rightarrow(X^{\prime},{\mathcal{U}}^{\prime})$ and
$g\colon(Y,{\mathcal{V}})\rightarrow(Y^{\prime},{\mathcal{V}}^{\prime})$ in
$\mathcal{UE}$ then also $f\times g\colon(X\times
Y,{\mathcal{U}}\otimes{\mathcal{V}})\rightarrow(X^{\prime}\times
Y^{\prime},{\mathcal{U}}^{\prime}\otimes{\mathcal{V}}^{\prime})$. So tensor
product of ultrafilters gives a monoidal structure on $\mathcal{UE}$, with as
unit the unique ultrafilter on the one-element set. Since maps in
${\mathcal{M}}$ are closed under the binary tensor, this monoidal structure
descends along $\iota$ to one on $\mathcal{UF}$.

The following result, which is a special case of [17, Theorem 1.10], describes
the interaction of the tensor product with ultrapowers and ultraproducts.

######  Proposition 7.

Given ${\mathcal{U}}\in\beta X$ and ${\mathcal{V}}\in\beta Y$ and an $X\times
Y$-indexed family of sets $Z$, currying of functions induces an isomorphism of
ultraproducts

(2.7) $(\Pi_{{\mathcal{U}}\otimes{\mathcal{V}}}(x,y)\,\mathord{\in}\,X\times
Y)Z(x,y)\cong(\Pi_{\mathcal{U}}x\,\mathord{\in}\,X)(\Pi_{\mathcal{V}}y\,\mathord{\in}\,Y)Z(x,y)\hbox
to0.0pt{ ,\hss}$

giving, when $Z$ is a constant family, isomorphisms
$Z^{{\mathcal{U}}\otimes{\mathcal{V}}}\cong(Z^{\mathcal{V}})^{\mathcal{U}}$.

A more general construction on ultrafilters is that of _indexed sum_.

######  Definition 8.

Let ${\mathcal{U}}$ be an ultrafilter on $X$ and, for each $x\in X$, let
${\mathcal{V}}(x)$ be an ultrafilter on $Y(x)$. The _indexed sum_
$(\Sigma_{\mathcal{U}}x\\!\in\\!X){\mathcal{V}}(x)$ or
${\mathcal{U}}.{\mathcal{V}}$ is the unique ultrafilter on $(\Sigma
x\,\mathord{\in}\,X)\,\\!Y(x)=X.Y$ which for all predicates $\varphi$ on $X.Y$
satisfies

$(\forall_{{\mathcal{U}}.{\mathcal{V}}}(x,y)\,\mathord{\in}X.Y)\varphi(x,y)\quad\Longleftrightarrow\quad(\forall_{{\mathcal{U}}}x\,\mathord{\in}X)(\forall_{{\mathcal{V}}(x)}y\,\mathord{\in}Y(x))\varphi(x,y)\hbox
to0.0pt{ .\hss}$

Note that when $Y$ and ${\mathcal{V}}$ are constant families, we have
$(\Sigma_{\mathcal{U}}x\in X){\mathcal{V}}={\mathcal{U}}\otimes{\mathcal{V}}$,
so that indexed sum really does generalise tensor product. Like before, we can
obtain an explicit formula for indexed sum by instantiating at the
characteristic functions of predicates, and like before, we have a formula
relating indexed sums with ultraproducts; this is now the general case of [17,
Theorem 1.10].

######  Proposition 9.

Given ${\mathcal{U}}\in\beta X$ and ${\mathcal{V}}\in(\Pi
x\,\mathord{\in}\,X)\,\\!\beta(Y(x))$ and an $X.Y$-indexed family of sets $Z$,
currying of functions induces an isomorphism of ultraproducts

(2.8)
$(\Pi_{{\mathcal{U}}.{\mathcal{V}}}(x,y)\,\mathord{\in}\,X.Y)Z(x,y)\cong(\Pi_{\mathcal{U}}x\,\mathord{\in}\,X)(\Pi_{{\mathcal{V}}(x)}\,y\,\mathord{\in}\,Y(x))Z(x,y)\hbox
to0.0pt{ .\hss}$

##  3\. The main theorem

In this section, we prove our main theorem. This makes essential use of
Börger’s characterisation [9] of the ultrafilter endofunctor, so we begin by
recalling this.

###  3.1. Börger’s theorem

If $u\colon{\mathcal{P}}X\rightarrow 2$ is a Boolean algebra homomorphism and
$f\colon X\rightarrow Y$, then
$u\circ(f^{-1})\colon{\mathcal{P}}Y\rightarrow{\mathcal{P}}X\rightarrow 2$ is
again a homomorphism, called the _pushforward_ of $u$ along $f$. Identifying
$u$ with the corresponding ${\mathcal{U}}\subseteq{\mathcal{P}}X$, its
pushforward along $f$ is given by:

(3.1) $f_{!}({\mathcal{U}})=\\{V\subseteq Y:f^{-1}(V)\in{\mathcal{U}}\\}\hbox
to0.0pt{ .\hss}$

######  Definition 10.

The _ultrafilter endofunctor_
$\beta\colon\mathrm{\mathcal{S}et}\rightarrow\mathrm{\mathcal{S}et}$ has
action on objects $X\mapsto\beta X$ and action on morphisms $\beta
f\colon\beta X\rightarrow\beta Y$ given by ${\mathcal{U}}\mapsto
f_{!}({\mathcal{U}})$.

In [9] Börger characterises $\beta$ as terminal in the category
$\mathsf{FC}(\mathrm{\mathcal{S}et},\mathrm{\mathcal{S}et})$ of finite-
coproduct-preserving endofunctors of $\mathrm{\mathcal{S}et}$. In reproducing
the proof, and subsequently, we will use the following lemma, whose proof is
either an easy exercise for the reader, or a consequence of the more general
Lemma 19 below. In the statement, we call a natural transformation
$\alpha\colon F\Rightarrow G\colon{\mathcal{C}}\rightarrow{\mathcal{D}}$
_monocartesian_ if the naturality square of $\alpha$ at any monomorphism
$f\colon X\rightarrowtail Y$ is a pullback.

######  Lemma 11.

Let $G\colon\mathrm{\mathcal{S}et}\rightarrow\mathrm{\mathcal{S}et}$ preserve
finite coproducts and let $\alpha\colon F\Rightarrow G$.

  1. (i)

$G$ preserves monomorphisms and pullbacks along monomorphisms;

  2. (ii)

$F$ preserves finite coproducts if and only if $\alpha$ is monocartesian.

######  Theorem 12.

[9, Theorem 2.1] $\beta$ is terminal in
$\mathsf{FC}(\mathrm{\mathcal{S}et},\mathrm{\mathcal{S}et})$.

###### Proof.

For an injection $f\colon X\rightarrow Y$, the map $\beta f\colon\beta
X\rightarrow\beta Y$ is also injective with

(3.2) $\operatorname{im}\beta f=\\{{\mathcal{V}}\in\beta
Y:f(X)\in{\mathcal{V}}\\}\hbox to0.0pt{ .\hss}$

Indeed, since $f$ is injective,
$f^{-1}\colon{\mathcal{P}}Y\rightarrow{\mathcal{P}}X$ is surjective and so
$\beta f=({\mathord{\text{--}}})\circ(f^{-1})$ is injective. As for its image:
each ${\mathcal{U}}\in\beta X$ contains $X=f^{-1}(f(X))$, so by (3.1) each
$f_{!}({\mathcal{U}})$ contains $f(X)$. Conversely, if ${\mathcal{V}}\in\beta
Y$ contains $f(X)$, then ${\mathcal{U}}=\\{U\subseteq
X:f(U)\in{\mathcal{V}}\\}$ is an ultrafilter on $X$ with
$f_{!}({\mathcal{U}})={\mathcal{V}}$.

We first use this to show
$\beta\in\mathsf{FC}(\mathrm{\mathcal{S}et},\mathrm{\mathcal{S}et})$. Clearly
$\beta(\emptyset)=\emptyset$; while if we have a coproduct ${y_{1}\colon
Y_{1}\rightarrow Y\leftarrow Y_{2}\colon y_{2}}$, then the maps $\beta
y_{1}\colon\beta Y_{1}\rightarrow\beta Y\leftarrow\beta Y_{2}\colon\beta
y_{2}$ are each injective with as images the sets
$A=\\{\,{\mathcal{U}}\in\beta Y:\operatorname{im}y_{1}\in{\mathcal{U}}\,\\}$
and $B=\\{\,{\mathcal{U}}\in\beta
Y:\operatorname{im}y_{2}\in{\mathcal{U}}\,\\}$. Since $\operatorname{im}y_{1}$
and $\operatorname{im}y_{2}$ partition $Y$, each ${\mathcal{U}}\in\beta Y$
lies in _exactly_ one of $A$ or $B$ whence $(\beta y_{1},\beta y_{2})$ is
again a coproduct cone.

We now show $\beta$ is terminal in
$\mathsf{FC}(\mathrm{\mathcal{S}et},\mathrm{\mathcal{S}et})$. Given
$T\in\mathsf{FC}(\mathrm{\mathcal{S}et},\mathrm{\mathcal{S}et})$ and $x\in
TX$, define the _type_ of $x$ as the ultrafilter on $X$ given by:

$\tau_{X}(x)=\\{U\subseteq X:\text{$x$ is in the image of the monic
$TU\rightarrowtail TX$}\\}\hbox to0.0pt{ .\hss}$

Here, $TU\rightarrowtail TX$ is the $T$-image of the inclusion $U\subseteq X$,
and so monic by Lemma 11. $\tau_{X}(x)$ satisfies axiom (i) for an ultrafilter
since $T$ preserves pullbacks of monics, and satisfies (ii)′ as
$TU\rightarrowtail TX\leftarrowtail T(X\setminus U)$ is the $T$-image of a
coproduct diagram and so itself a coproduct.

So we have functions $\tau_{X}\colon TX\rightarrow\beta X$. To verify their
naturality in $X$ we must show for any $x\in TX$ and $f\colon X\rightarrow Y$
that $\tau_{Y}(Tf(x))=f_{!}(\tau_{X}(x))$. So for any $V\subseteq Y$, we must
show $Tf(x)\in TY$ is in the image of $TV\rightarrowtail TY$ if and only if
$x\in TX$ is in the image of $T(f^{-1}(V))\rightarrowtail TX$; which is so
because $T$ preserves the pullback of $V\rightarrowtail Y$ along $f\colon
X\rightarrow Y$ by Lemma 11. So we have $\tau\colon T\Rightarrow\beta$.

Finally, we check uniqueness of $\tau$. Any $\sigma\colon T\Rightarrow\beta$
is monocartesian by Lemma 11; and so for each $m\colon U\subseteq X$ the
following square is a pullback:

$\textstyle{{TU}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{Tm}$$\scriptstyle{\sigma_{V}}$$\textstyle{{TX}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\sigma_{X}}$$\textstyle{{\beta
U}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\beta
m}$$\textstyle{{\beta X}\hbox to0.0pt{ .\hss}}$

Thus, $x\in TX$ factors through $Tm$ if and only if $\sigma_{X}(x)$ factors
through $\beta m$ which by (3.2) happens just when $U\in\sigma_{X}(x)$. So
$\sigma_{X}(x)=\tau_{X}(x)$ as desired. ∎

###  3.2. The main theorem

We now exploit Börger’s theorem to prove our main Theorem 13. In doing so, we
make use of the well-known generalisation of (2.1) stating that  _any slice of
a presheaf category is equivalent to a presheaf category_.

Indeed, given $X\in[{\mathcal{A}},\mathrm{\mathcal{S}et}]$, the _category of
elements_ $\operatorname{el}X$ has as objects, pairs $(A\in{\mathcal{A}},x\in
XA)$ and as morphisms $(A,x)\rightarrow(A^{\prime},x^{\prime})$, maps $f\colon
A\rightarrow A^{\prime}$ in ${\mathcal{A}}$ such that $x^{\prime}=Xf(x)$. The
equivalence in question is now

(3.3)
$[\operatorname{el}X,\mathrm{\mathcal{S}et}]\simeq[{\mathcal{A}},\mathrm{\mathcal{S}et}]/X\hbox
to0.0pt{ ,\hss}$

and is constructed by applying (2.1) componentwise as follows. Going from left
to right, $Y\colon\operatorname{el}X\rightarrow\mathrm{\mathcal{S}et}$ is sent
to $\pi\colon\int\\!Y\rightarrow X$ whose $A$-component is given by the first
projection map $(\Sigma x\,\mathord{\in}\,XA)\,\\!Y(A,x)\rightarrow XA$, and
where the action of $\int\\!Y$ on maps is induced from those of $X$ and $Y$.
Going from right to left, $p\colon E\rightarrow X$ in
$[{\mathcal{A}},\mathrm{\mathcal{S}et}]/X$ is sent to $\tilde{E}$ in
$[\operatorname{el}X,\mathrm{\mathcal{S}et}]$ with
$\smash{\tilde{E}(A,x)=p_{A}^{-1}(x)}\subseteq EA$ and action on maps
inherited from $E$. For a detailed proof of the equivalence, see for example
[25, Proposition A1.1.7].

######  Theorem 13.

The category $\mathsf{FC}(\mathrm{\mathcal{S}et},\mathrm{\mathcal{S}et})$ of
finite coproduct-preserving endofunctors of $\mathrm{\mathcal{S}et}$ is
equivalent to $[\mathcal{UF},\mathrm{\mathcal{S}et}]$.

###### Proof.

Note that $T\in[\mathrm{\mathcal{S}et},\mathrm{\mathcal{S}et}]$ preserves
finite coproducts if and only if it admits a monocartesian transformation to
$\beta$, which is then necessarily unique. The “if” direction of this claim
follows from Lemma 11; whereupon the “only if” direction and the unicity
follow from Theorem 12. So we have an isomorphism of categories

(3.4)
$\mathsf{FC}(\mathrm{\mathcal{S}et},\mathrm{\mathcal{S}et})\cong[\mathrm{\mathcal{S}et},\mathrm{\mathcal{S}et}]\mathop{/_{\\!\mathrm{mc}}}\beta$

where to the right we have the full, replete, subcategory
$[\mathrm{\mathcal{S}et},\mathrm{\mathcal{S}et}]\mathop{/_{\\!\mathrm{mc}}}\beta$
of $[\mathrm{\mathcal{S}et},\mathrm{\mathcal{S}et}]/\beta$ on the
monocartesian arrows.

Now, the full slice category
$[\mathrm{\mathcal{S}et},\mathrm{\mathcal{S}et}]/\beta$ is equivalent to
$[\operatorname{el}\beta,\mathrm{\mathcal{S}et}]$. Here, objects of
$\operatorname{el}\beta$ are pairs
$(X\in\mathrm{\mathcal{S}et},\,{\mathcal{U}}\in\beta X)$, while maps
$(X,{\mathcal{U}})\rightarrow(Y,{\mathcal{V}})$ are functions $f\colon
X\rightarrow Y$ such that $f_{!}({\mathcal{U}})={\mathcal{V}}$. Comparing
(2.4) with (3.1), these are exactly the _continuous_ maps, so that
$\operatorname{el}\beta\cong\mathcal{UE}$ and (3.3) becomes an equivalence:

(3.5)
$[\mathrm{\mathcal{S}et},\mathrm{\mathcal{S}et}]/\beta\simeq[\mathcal{UE},\mathrm{\mathcal{S}et}]\hbox
to0.0pt{ .\hss}$

An object $\tau\colon T\Rightarrow\beta$ to the left of this equivalence lies
in the full replete subcategory
$[\mathrm{\mathcal{S}et},\mathrm{\mathcal{S}et}]\mathop{/_{\\!\mathrm{mc}}}\beta$
just when for each monic $f\colon X\rightarrowtail Y$ and
${\mathcal{U}}\in\beta X$, the map on fibres
$\tau_{X}^{-1}({\mathcal{U}})\rightarrow\tau_{Y}^{-1}(f_{!}({\mathcal{U}}))$
is an isomorphism. This is equally the condition that the corresponding
$\bar{\tau}\in[\mathcal{UE},\mathrm{\mathcal{S}et}]$ to the right lies in the
full, replete subcategory of functors which send the class ${\mathcal{M}}$ of
continuous injective functions to isomorphisms. By Proposition 5, this
subcategory is isomorphic to $[\mathcal{UF},\mathrm{\mathcal{S}et}]$ via
restriction along $\iota\colon\mathcal{UE}\rightarrow\mathcal{UF}$. So (3.5)
restricts to an equivalence
$[\mathrm{\mathcal{S}et},\mathrm{\mathcal{S}et}]\mathop{/_{\\!\mathrm{mc}}}\beta\simeq[\mathcal{UF},\mathrm{\mathcal{S}et}]$,
and combining this with (3.4) yields the desired equivalence
$\mathsf{FC}(\mathrm{\mathcal{S}et},\mathrm{\mathcal{S}et})\simeq[\mathcal{UF},\mathrm{\mathcal{S}et}]$.
∎

Chasing through the above equivalences, we see that for each
$A\in\mathsf{FC}(\mathrm{\mathcal{S}et},\mathrm{\mathcal{S}et})$, the
corresponding $\tilde{A}\colon\mathcal{UF}\rightarrow\mathrm{\mathcal{S}et}$
is defined on objects by

(3.6) $\tilde{A}(X,{\mathcal{U}})=\\{\,x\in
AX:\tau_{X}(x)={\mathcal{U}}\,\\}\cong\textstyle\bigcap_{U\in{\mathcal{U}}}\operatorname{im}AU\subseteq
AX\hbox to0.0pt{ .\hss}$

For its definition on morphisms, let the map
$(X,{\mathcal{U}})\rightarrow(Y,{\mathcal{V}})$ of $\mathcal{UF}$ be
represented by the partial continuous $f\colon X\rightharpoonup Y$ defined on
$U\in{\mathcal{U}}$. Then the induced function
$\tilde{A}(X,{\mathcal{U}})\rightarrow\tilde{A}(Y,{\mathcal{V}})$ is defined
by $x\mapsto Af(x^{\prime})$, where $x^{\prime}\in AU$ is the lifting of $x$
through $AU\rightarrowtail AX$ guaranteed by the fact that $U\in\tau_{X}(x)$.

In the other direction, for any
$B\colon\mathcal{UF}\rightarrow\mathrm{\mathcal{S}et}$, the corresponding
finite-coproduct-preserving
$\int\\!B\colon\mathrm{\mathcal{S}et}\rightarrow\mathrm{\mathcal{S}et}$ is
defined by

(3.7) $(\textstyle\int\\!B)Y=\sum_{{\mathcal{V}}\in\beta
Y}B(Y,{\mathcal{V}})\quad\text{and}\quad(\int\\!B)f\colon({\mathcal{V}},a)\mapsto(f_{!}({\mathcal{V}}),Af(a))\hbox
to0.0pt{ .\hss}$

###  3.3. Relation to ultrapowers and tensor products

We now show that both ultrapowers and the tensor product of ultrafilters arise
naturally from the preceding equivalence. We begin with ultrapowers.

######  Corollary 14.

Under the equivalence of Theorem 13, the representable functor
$\mathcal{UF}((X,{\mathcal{U}}),{\mathord{\text{--}}})\colon\mathcal{UF}\rightarrow\mathrm{\mathcal{S}et}$
corresponds to the ultrapower functor
$({\mathord{\text{--}}})^{\mathcal{U}}\colon\mathrm{\mathcal{S}et}\rightarrow\mathrm{\mathcal{S}et}$.

###### Proof.

Taking $B$ to be
$y_{(X,{\mathcal{U}})}=\mathcal{UF}((X,{\mathcal{U}}),{\mathord{\text{--}}})$
in (3.7), we have that

$(\textstyle\int\\!y_{(X,{\mathcal{U}})})(X)=\textstyle\sum_{{\mathcal{V}}\in\beta
Y}\mathcal{UF}((X,{\mathcal{U}}),(Y,{\mathcal{V}}))\hbox to0.0pt{ .\hss}$

An element of this set is a pair ${\mathcal{V}}\in\beta Y$ together with an
$=_{\mathcal{U}}$-equivalence class of continuous partial functions
$f\colon(X,{\mathcal{U}})\rightharpoonup(Y,{\mathcal{V}})$ defined on a set in
${\mathcal{U}}$. The continuity condition (2.4) forces
${\mathcal{V}}=f_{!}({\mathcal{U}})$ and so this is equally a
$=_{\mathcal{U}}$-equivalence class of partial functions $f\colon
X\rightharpoonup Y$ defined on a set in ${\mathcal{U}}$; thus an element of
the ultrapower $Y^{\mathcal{U}}$. This proves that
$\textstyle\int\\!y_{(X,{\mathcal{U}})}\cong({\mathord{\text{--}}})^{\mathcal{U}}$
as desired. ∎

As remarked in the introduction, we can use this result to recover the
category $\mathcal{UF}$ from
$\mathsf{FC}(\mathrm{\mathcal{S}et},\mathrm{\mathcal{S}et})$. Recall that an
object $X$ of a category ${\mathcal{E}}$ is _small-projective_ if the hom-
functor
${\mathcal{E}}(X,{\mathord{\text{--}}})\colon{\mathcal{E}}\rightarrow\mathrm{\mathcal{S}et}$
preserves all small colimits.

######  Corollary 15.

The category $\mathcal{UF}^{\mathrm{op}}$ is equivalent to the full
subcategory of $\mathsf{FC}(\mathrm{\mathcal{S}et},\mathrm{\mathcal{S}et})$ on
the small-projectives.

###### Proof.

For any locally small ${\mathcal{A}}$, the small-projectives in
$[{\mathcal{A}},\mathrm{\mathcal{S}et}]$ are precisely the retracts of
representable functors; see, for example, [8, Lemma 6.5.10]. So if
representables are closed under retracts, then ${\mathcal{A}}^{\mathrm{op}}$
is equivalent to the full subcategory of
$[{\mathcal{A}},\mathrm{\mathcal{S}et}]$ on the small-projectives.

It thus suffices to show that representables in
$[\mathcal{UF},\mathrm{\mathcal{S}et}]$ are closed under retracts. But if
$i\colon A\rightarrowtail y_{(X,{\mathcal{U}})}$ and $p\colon
y_{(X,{\mathcal{U}})}\twoheadrightarrow A$ with $pi=1$, then $ip\colon
y_{(X,{\mathcal{U}})}\rightarrow y_{(X,{\mathcal{U}})}$ is the image under $y$
of an idempotent on $(X,{\mathcal{U}})$. Since by [5, Theorem 5], the only
idempotents (indeed, the only endomorphisms) in $\mathcal{UF}$ are the
identities, we thus have $ip=1$ as well as $pi=1$, so that $A\cong
y_{(X,{\mathcal{U}})}$ is again representable. ∎

We now turn to the tensor product of ultrafilters. The category
$\mathsf{FC}(\mathrm{\mathcal{S}et},\mathrm{\mathcal{S}et})$ has a monoidal
structure given by composition, and transporting this across the equivalence
of Theorem 13 yields a monoidal structure $(I,\otimes)$ on
$[\mathcal{UF},\mathrm{\mathcal{S}et}]$.

######  Proposition 16.

The representables in $[\mathcal{UF},\mathrm{\mathcal{S}et}]$ are closed under
the monoidal structure, and the induced monoidal structure on $\mathcal{UF}$
is that given by tensor product of ultrafilters.

###### Proof.

The identity functor $\mathrm{\mathcal{S}et}\rightarrow\mathrm{\mathcal{S}et}$
corresponds to the functor $\mathcal{UF}\rightarrow\mathrm{\mathcal{S}et}$
represented by the unique ultrafilter on a one-element set, which is the unit
for the monoidal structure on $\mathcal{UF}$. On the other hand, if
$A,B\in[\mathcal{UF},\mathrm{\mathcal{S}et}]$ are represented by
$(X,{\mathcal{U}})$ and $(Y,{\mathcal{V}})$ respectively, then by Theorem 13
we have $\textstyle\int\\!A\cong({\mathord{\text{--}}})^{\mathcal{U}}$ and
$\textstyle\int\\!B\cong({\mathord{\text{--}}})^{\mathcal{V}}$, and so
$\textstyle\int\\!A\circ\textstyle\int\\!B\cong(({\mathord{\text{--}}})^{\mathcal{V}})^{\mathcal{U}}\cong({\mathord{\text{--}}})^{{\mathcal{U}}\otimes{\mathcal{V}}}$
by Proposition 7. It follows that $A\otimes B$ is represented by $(X\times
Y,{\mathcal{U}}\otimes{\mathcal{V}})=(X,{\mathcal{U}})\otimes(Y,{\mathcal{V}})$
in $\mathcal{UF}$. ∎

The monoidal structure on $[\mathcal{UF},\mathrm{\mathcal{S}et}]$ is easy to
write down explicitly. As already noted, the unit $I$ is the functor
representable at the unique ultrafilter on the one-element set, while the
binary tensor can be given as $A\otimes B=\int\\!A\circ B$, where $\int\\!A$
is defined as in (3.7). This yields the formulae:

$\displaystyle I(X,{\mathcal{U}})$ $\displaystyle=\begin{cases}1&\text{if
${\mathcal{U}}$ is principal;}\\\ 0&\text{otherwise.}\end{cases}$
$\displaystyle(A\otimes B)(X,{\mathcal{U}})$
$\displaystyle=\textstyle\sum_{{\mathcal{V}}\in\beta(B(X,{\mathcal{U}}))}A(B(X,{\mathcal{U}}),{\mathcal{V}})\hbox
to0.0pt{ .\hss}$

We have an alternative description of the binary tensor product by exploiting
the fact that, since the composition product on
$\mathsf{FC}(\mathrm{\mathcal{S}et},\mathrm{\mathcal{S}et})$ preserves
colimits in its first variable, so too does the tensor product $\otimes$ on
$[\mathcal{UF},\mathrm{\mathcal{S}et}]$:

(3.8) $\displaystyle(A\otimes B)(X,{\mathcal{U}})$
$\displaystyle\cong\left((\textstyle\int^{(Y,{\mathcal{V}})\in\mathcal{UF}}A(Y,{\mathcal{V}})\times
y_{(Y,{\mathcal{V}})})\otimes B\right)(X,{\mathcal{U}})$
$\displaystyle\cong\textstyle\int^{(Y,{\mathcal{V}})\in\mathcal{UF}}A(Y,{\mathcal{V}})\times(y_{(Y,{\mathcal{V}})}\otimes
B)(X,{\mathcal{U}})$
$\displaystyle\cong\textstyle\int^{(Y,{\mathcal{V}})\in\mathcal{UF}}A(Y,{\mathcal{V}})\times
B(X,{\mathcal{U}})^{\mathcal{V}}\hbox to0.0pt{ .\hss}$

Compare this with the well-known _substitution monoidal structure_ on
$[\mathrm{\mathcal{F}},\mathrm{\mathcal{S}et}]$—for $\mathrm{\mathcal{F}}$ the
category of functions between finite cardinals—defined by:

(3.9) $(A\otimes B)(m)=\textstyle\int^{n\in\mathrm{\mathcal{F}}}An\times
Bm^{n}\hbox to0.0pt{ .\hss}$

######  Remark 17.

Given a monoidal category ${\mathcal{V}}$, one may consider categories
_enriched_ over ${\mathcal{V}}$ in the sense of [31]. A
${\mathcal{V}}$-enriched category ${\mathcal{C}}$ involves a set of objects
$A,B,C,\dots$ as usual, but instead of hom-sets of morphisms, one has hom-
_objects_ ${\mathcal{C}}(A,B)$ in ${\mathcal{V}}$. In the enriched context,
one has a new kind of colimit available, namely the _copower_ $V\cdot A$ of an
object $A\in{\mathcal{C}}$ by an object $V\in{\mathcal{V}}$, characterised by
natural isomorphisms ${\mathcal{C}}(V\cdot A,B)\cong[V,{\mathcal{C}}(A,B)]$ in
${\mathcal{V}}$.

In [20], the author considered categories enriched over
$[{\mathcal{F}},\mathrm{\mathcal{S}et}]$ with the substitution monoidal
structure, and showed that such
$[{\mathcal{F}},\mathrm{\mathcal{S}et}]$-categories admitting copowers by
representables correspond to ordinary categories ${\mathcal{C}}$ admitting
finite powers
$({\mathord{\text{--}}})^{n}\colon{\mathcal{C}}\rightarrow{\mathcal{C}}$. The
analogy between (3.8) and (3.9) suggests that something similar should be
possible with $[\mathcal{UF},\mathrm{\mathcal{S}et}]$ in place of
$[{\mathcal{F}},\mathrm{\mathcal{S}et}]$, and this is indeed so: categories
enriched over $[\mathcal{UF},\mathrm{\mathcal{S}et}]$ with copowers by
representables correspond to ordinary categories ${\mathcal{C}}$ equipped with
_abstract ultrapower_ functors
$({\mathord{\text{--}}})^{\mathcal{U}}\colon{\mathcal{C}}\rightarrow{\mathcal{C}}$.
The details of this will be left for future work, but we discuss an extension
to categories endowed with _abstract ultraproduct_ functors in Remark 32
below.

##  4\. First generalisation

In this section, we give our first generalisation of Theorem 13. This will
show that, for any extensive category ${\mathcal{C}}$, there is an equivalence
$\mathsf{FC}({\mathcal{C}},\mathrm{\mathcal{S}et})\simeq[\mathcal{UF}_{\mathcal{C}},\mathrm{\mathcal{S}et}]$
where $\mathcal{UF}_{\mathcal{C}}$ is a suitably defined category of
ultrafilters on ${\mathcal{C}}$-objects. We then describe how this result
captures the notion of ultraproduct, and how it reconstructs the categorical
treatment in [38] of types in model theory.

###  4.1. Generalising the domain category

We begin by recalling from [12] that a category ${\mathcal{C}}$ with finite
coproducts is _extensive_ if for every $A,B\in{\mathcal{C}}$, the functor
$+\colon{\mathcal{C}}/A\times{\mathcal{C}}/B\rightarrow{\mathcal{C}}/(A+B)$ is
an equivalence of categories. Equally, by [12, Proposition 2.2],
${\mathcal{C}}$ is extensive just when it has pullbacks along coproduct
coprojections, and, for every diagram

(4.1)
$\textstyle{A^{\prime}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{a}$$\scriptstyle{i^{\prime}}$$\textstyle{C^{\prime}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{c}$$\textstyle{\ignorespaces\ignorespaces\ignorespaces\ignorespaces
B^{\prime}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{j^{\prime}}$$\scriptstyle{b}$$\textstyle{A\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{i}$$\textstyle{C}$$\textstyle{B\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{j}$

in which the bottom row is a coproduct diagram, the top row is a coproduct
diagram if and only if the two squares are pullbacks.

Note the “if” direction says that binary coproducts in ${\mathcal{C}}$ are
pullback-stable. In fact, a category with finite coproducts and pullbacks
along their coprojections is extensive just when binary coproducts are
pullback-stable and _disjoint_ ; see [12, Proposition 2.14]. Disjointness
means that coproduct coprojections are monic, and the pullback of the two
coprojections of a binary coproduct is initial.

This characterisation implies that any topos is extensive; see [25,
Proposition A2.3.4 & Corollary A2.4.4]. In particular,
$\mathrm{\mathcal{S}et}$ is extensive, as is any presheaf category. Other
examples of extensive categories include the categories of topological spaces,
of small categories and of affine schemes.

Let us write $\mathrm{Sum}_{\mathcal{C}}(X)$ for the poset of coproduct
summands of $X\in{\mathcal{C}}$: that is, the poset of isomorphism-classes of
coproduct coprojections with codomain $X$.

######  Proposition 18.

If ${\mathcal{C}}$ is extensive, then for each $X\in{\mathcal{C}}$ the poset
$\mathrm{Sum}_{\mathcal{C}}(X)$ is a Boolean algebra, and for each $f\colon
X\rightarrow Y$, pullback along $f$ defines a Boolean algebra homomorphism
$f^{-1}\colon\mathrm{Sum}_{\mathcal{C}}(Y)\rightarrow\mathrm{Sum}_{\mathcal{C}}(X)$.

###### Proof.

Since binary coproducts in ${\mathcal{C}}$ are stable under pullback, so are
coproduct coprojections; since they are also composition-closed, each
$\mathrm{Sum}_{\mathcal{C}}(X)$ has finite meets, and
$f^{-1}\colon\mathrm{Sum}_{\mathcal{C}}(Y)\rightarrow\mathrm{Sum}_{\mathcal{C}}(X)$
is well-defined and finite-meet-preserving. Now any $Y_{1}\rightarrowtail Y$
in $\mathrm{Sum}_{\mathcal{C}}(X)$ is part of a coproduct
$Y_{1}\rightarrowtail Y\leftarrowtail Y_{2}$. Of course $Y_{1}\cup
Y_{2}=\top_{Y}$ in $\mathrm{Sum}_{\mathcal{C}}(Y)$, and $Y_{1}\cap
Y_{2}=\bot_{Y}$ by disjointness; so $\mathrm{Sum}_{\mathcal{C}}(X)$ has
complements and so is a Boolean algebra. Further,
$f^{-1}\colon\mathrm{Sum}_{\mathcal{C}}(Y)\rightarrow\mathrm{Sum}_{\mathcal{C}}(X)$
preserves these complements as binary coproducts are pullback-stable. ∎

A case worth noting is that where ${\mathcal{C}}$ is _Boolean extensive_ ,
meaning that every monic in ${\mathcal{C}}$ is a coproduct coprojection; in
this situation $\mathrm{Sum}_{\mathcal{C}}(X)$ coincides with the full
subobject lattice $\mathrm{Sub}_{\mathcal{C}}(X)$, so that all subobject
lattices in ${\mathcal{C}}$ are Boolean algebras—whence the nomenclature. In
particular, the category of sets is Boolean extensive, so that the following
result is a generalisation of Lemma 11 above. In the last part of the
statement, a natural transformation $\alpha$ is called _sum-cartesian_ if its
naturality square at every coproduct coprojection is a pullback.

######  Lemma 19.

Let ${\mathcal{C}}$ and ${\mathcal{D}}$ be extensive, let
$G\colon{\mathcal{C}}\rightarrow{\mathcal{D}}$ be finite-coproduct-preserving
and let $\alpha\colon F\Rightarrow
G\colon{\mathcal{C}}\rightarrow{\mathcal{D}}$.

  1. (i)

$G$ preserves both coproduct coprojections and pullbacks along such;

  2. (ii)

$F$ preserves finite coproducts just when $\alpha\colon F\Rightarrow G$ is
sum-cartesian.

###### Proof.

The first part of (i) is clear. For the second, any pullback along a coproduct
coprojection in ${\mathcal{C}}$ is the left square of a diagram like (4.1) in
which both rows are coproducts. Applying $F$, both rows remain coproducts and
so by extensivity of ${\mathcal{D}}$, both squares remain pullbacks. As for
(ii), given a coproduct diagram $i\colon A\rightarrow C\leftarrow B\colon j$
in ${\mathcal{C}}$, we consider the diagram

$\textstyle{FA\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\alpha_{A}}$$\scriptstyle{Fi}$$\textstyle{FC\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\alpha_{C}}$$\textstyle{\ignorespaces\ignorespaces\ignorespaces\ignorespaces
FB\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{Fj}$$\scriptstyle{\alpha_{B}}$$\textstyle{GA\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{Gi}$$\textstyle{GC}$$\textstyle{GB\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{Gj}$

in ${\mathcal{D}}$. The bottom row is a coproduct since $G$ preserves such;
so, by extensivity of ${\mathcal{D}}$, the top row is a coproduct (i.e., $F$
preserves finite coproducts) just when both squares are pullbacks (i.e.,
$\alpha$ is sum-cartesian). ∎

If ${\mathcal{C}}$ is extensive, then we define an _ultrafilter_ on
$X\in{\mathcal{C}}$ to be a Boolean algebra homomorphism
$\mathrm{Sum}_{\mathcal{C}}(X)\rightarrow 2$; equivalently, a subset
${\mathcal{U}}\subseteq\mathrm{Sum}_{\mathcal{C}}(X)$ satisfying the analogue
of conditions (i) and (ii) or (i) and (ii)′ of Definition 2. Like before, we
write $\beta X$ for the set of ultrafilters on $X\in{\mathcal{C}}$. Since each
$f^{-1}\colon\mathrm{Sum}_{\mathcal{C}}(Y)\rightarrow\mathrm{Sum}_{\mathcal{C}}(X)$
is a Boolean algebra homomorphism, precomposition with $f^{-1}$ yields a
function $\beta f\colon\beta X\rightarrow\beta Y$; in this way, we define an
ultrafilter functor
$\beta\colon{\mathcal{C}}\rightarrow\mathrm{\mathcal{S}et}$.

######  Proposition 20.

$\beta\colon{\mathcal{C}}\rightarrow\mathrm{\mathcal{S}et}$ is terminal in
$\mathsf{FC}({\mathcal{C}},\mathrm{\mathcal{S}et})$.

###### Proof.

The proof in Theorem 12 adapts without difficulty to show that
$\beta\colon{\mathcal{C}}\rightarrow\mathrm{\mathcal{S}et}$ preserves finite
coproducts. To show terminality in
$\mathsf{FC}({\mathcal{C}},\mathrm{\mathcal{S}et})$, we suppose given
$T\in\mathsf{FC}({\mathcal{C}},\mathrm{\mathcal{S}et})$. For any
$X\in{\mathcal{C}}$ and $x\in TX$, we again define the _type_ of $x$ to be:

$\tau_{X}(x)=\\{U\ext@arrow
0055{\arrowfill@{\Yright\joinrel\relbar}\relbar\rightarrow}{}{m}X\in\mathrm{Sum}_{\mathcal{C}}(X):\text{$x$
factors through }FU\ext@arrow
0055{\arrowfill@{\Yright\joinrel\relbar}\relbar\rightarrow}{}{Fm}FX\\}\hbox
to0.0pt{ .\hss}$

The same argument as before, but now exploiting Lemma 19 in place of Lemma 11,
shows that this definition gives the values of a well-defined natural
transformation $\tau\colon
T\Rightarrow\beta\colon{\mathcal{C}}\rightarrow\mathrm{\mathcal{S}et}$, and
that this $\tau$ is unique. ∎

Like before, given objects $X,Y\in{\mathcal{C}}$ endowed with ultrafilters
${\mathcal{U}}$ and ${\mathcal{V}}$, we call $f\colon X\rightarrow Y$
_continuous_ if for all $V\in\mathrm{Sum}_{\mathcal{C}}(Y)$ we have
$V\in{\mathcal{V}}\Leftrightarrow f^{-1}(V)\in{\mathcal{U}}$. More generally,
a map $f\colon U\rightarrow Y$ defined on the domain of some $U\rightarrowtail
X$ in ${\mathcal{U}}$ is _continuous_ if $V\rightarrowtail Y\in{\mathcal{V}}$
just when $f^{-1}(V)\rightarrowtail U\rightarrowtail X\in{\mathcal{U}}$. Two
partial maps defined on $U$ and $U^{\prime}$ are _$=_{\mathcal{U}}$
-equivalent_ if their restrictions to some $W\subseteq U\cap U^{\prime}$ in
${\mathcal{U}}$ coincide.

######  Definition 21.

The category $\mathcal{UE}_{\mathcal{C}}$ has pairs
$(X\in{\mathcal{C}},{\mathcal{U}}\in\beta X)$ as objects, and as morphisms
$(X,{\mathcal{U}})\rightarrow(Y,{\mathcal{V}})$ the continuous maps
$X\rightarrow Y$. The category $\mathcal{UF}_{\mathcal{C}}$ has the same
objects, and as morphisms $(X,{\mathcal{U}})\rightarrow(Y,{\mathcal{V}})$ the
$=_{\mathcal{U}}$-equivalence classes of partial continuous maps
$X\rightharpoonup Y$ defined on the domain of some $U\rightarrowtail X$ in
${\mathcal{U}}$.

Writing ${\mathcal{M}}_{\Sigma}$ for the maps in $\mathcal{UE}_{\mathcal{C}}$
whose underlying map in ${\mathcal{C}}$ is a coproduct coprojection, we have
as in Proposition 5, that
$\mathcal{UF}_{\mathcal{C}}\cong\mathcal{UE}_{\mathcal{C}}[{\mathcal{M}}_{\Sigma}^{-1}]$.
Now transcribing the proof of Theorem 13 and Corollary 14, but exploiting
Proposition 20 and Lemma 19 in place of Theorem 12 and Lemma 11, gives the
following.

######  Theorem 22.

Let ${\mathcal{C}}$ be extensive. The category
$\mathsf{FC}({\mathcal{C}},\mathrm{\mathcal{S}et})$ of finite coproduct-
preserving functors ${\mathcal{C}}\rightarrow\mathrm{\mathcal{S}et}$ is
equivalent to $[\mathcal{UF}_{\mathcal{C}},\mathrm{\mathcal{S}et}]$. Under
this equivalence, the representable presheaf at
$(X,{\mathcal{U}})\in\mathcal{UF}_{\mathcal{C}}$ corresponds to the “ultrahom
functor”

${\mathcal{C}}(X,{\mathord{\text{--}}})_{\mathcal{U}}=\mathrm{colim}_{U\in{\mathcal{U}}}{\mathcal{C}}(U,{\mathord{\text{--}}})\colon{\mathcal{C}}\rightarrow\mathrm{\mathcal{S}et}\hbox
to0.0pt{ .\hss}$

The formulae for the two directions of the equivalence
$\mathsf{FC}({\mathcal{C}},\mathrm{\mathcal{S}et})\simeq[\mathcal{UF}_{\mathcal{C}},\mathrm{\mathcal{S}et}]$
are once again given by (3.6) and (3.7).

######  Example 23.

The category $\mathrm{\mathcal{S}tone}$ of Stone spaces is extensive and
$\mathrm{Sum}_{\mathrm{\mathcal{S}tone}}(X)$ is the Boolean algebra of clopen
sets of $X$. It follows by Stone duality that ultrafilters on
$X\in\mathrm{\mathcal{S}tone}$ correspond exactly to points of $X$, so that
the category $\mathcal{UF}_{\mathrm{\mathcal{S}tone}}$ has pointed Stone
spaces $(X,x)$ as objects, and as maps $f\colon(X,x)\rightarrow(Y,y)$, germs
at $x$ of point-preserving continuous functions $X\rightarrow Y$. Under the
equivalence
$[\mathcal{UF}_{\mathrm{\mathcal{S}tone}},\mathrm{\mathcal{S}et}]\simeq\mathsf{FC}(\mathrm{\mathcal{S}tone},\mathrm{\mathcal{S}et})$,
the representable at $(X,x)$ corresponds to the functor which sends a Stone
space $Y$ to the stalk at $x$ of the sheaf of continuous functions
$X\rightarrow Y$.

###  4.2. Relation to ultraproducts

We now explain how Theorem 22 allows us to reconstruct the notion of
ultraproduct. Taking ${\mathcal{C}}=\mathrm{\mathcal{S}et}^{X}$ therein yields
the equivalence
$[\mathcal{UF}_{\mathrm{\mathcal{S}et}^{X}},\mathrm{\mathcal{S}et}]\simeq\mathsf{FC}(\mathrm{\mathcal{S}et}^{X},\mathrm{\mathcal{S}et})$,
and we will obtain the ultraproduct functors as correlates to the right of
suitable _representable_ functors to the left.

Note first that, via (2.1), we have for any $A\in\mathrm{\mathcal{S}et}^{X}$
that

$\mathrm{Sum}_{\mathrm{\mathcal{S}et}^{X}}(A)\cong\mathrm{Sum}_{\mathrm{\mathcal{S}et}/X}(\pi_{A}\colon
X.A\rightarrow X)\cong{\mathcal{P}}(X.A)\hbox to0.0pt{ ,\hss}$

so that ultrafilters on $A\in\mathrm{\mathcal{S}et}^{X}$ can be identified
with ultrafilters on $X.A$ in $\mathrm{\mathcal{S}et}$. Under this
identification, the ultrafilter ${\mathcal{U}}$ on $X.A$ corresponds to the
ultrafilter $\tilde{\mathcal{U}}=\\{\tilde{U}:U\in{\mathcal{U}}\\}$ on $A$
composed of the subobjects $\tilde{U}\rightarrowtail A$ obtained by passing
the subobjects $U\rightarrowtail X.A\rightarrow X$ of $\pi_{A}\colon
X.A\rightarrow X$ across the equivalence (2.1).

######  Proposition 24.

Under the equivalence
$[\mathcal{UF}_{\mathrm{\mathcal{S}et}^{X}},\mathrm{\mathcal{S}et}]\simeq\mathsf{FC}(\mathrm{\mathcal{S}et}^{X},\mathrm{\mathcal{S}et})$,
the representable functor at
$(A\in\mathrm{\mathcal{S}et}^{X},{\mathcal{U}}\in\beta(X.A))$ corresponds to
the composite

(4.2) $\mathrm{\mathcal{S}et}^{X}\ext@arrow 01{20}0\rightarrowfill@{}{\ \
\textstyle\mathrm{\mathcal{S}et}^{\pi_{A}}\ \
}\mathrm{\mathcal{S}et}^{X.A}\ext@arrow 01{20}0\rightarrowfill@{}{\ \
\textstyle\Pi_{\mathcal{U}}\ \ }\mathrm{\mathcal{S}et}\hbox to0.0pt{ .\hss}$

In particular, the representable at $(1,{\mathcal{U}})$ corresponds to
$\Pi_{\mathcal{U}}\colon\mathrm{\mathcal{S}et}^{X}\rightarrow\mathrm{\mathcal{S}et}$.

###### Proof.

From Theorem 22 and the above remarks, we know that $y_{(A,{\mathcal{U}})}$
corresponds to the ultrahom functor
$\mathrm{\mathcal{S}et}^{X}(A,{\mathord{\text{--}}})_{\tilde{\mathcal{U}}}$.
We now calculate that:

$\displaystyle\mathrm{\mathcal{S}et}^{X}(A,Y)_{\tilde{\mathcal{U}}}$
$\displaystyle=\mathop{\mathrm{colim}}\nolimits_{\tilde{U}\in\tilde{\mathcal{U}}}\mathrm{\mathcal{S}et}^{X}(\smash{\tilde{U}},Y)$
$\displaystyle\cong\mathop{\mathrm{colim}}\nolimits_{U\in{\mathcal{U}}}\mathrm{\mathcal{S}et}/X(\,U\rightarrowtail
X.A\ext@arrow 01{20}0\rightarrowfill@{}{\pi_{A}}X,\,X.Y\ext@arrow
01{20}0\rightarrowfill@{}{\pi_{Y}}X\,)$
$\displaystyle\cong\mathop{\mathrm{colim}}\nolimits_{U\in{\mathcal{U}}}\mathrm{\mathcal{S}et}/X.A(\,U\rightarrowtail
X.A,\,\pi_{A}^{\ast}(X.Y)\ext@arrow
01{20}0\rightarrowfill@{}{\smash{{\pi_{A}}^{\ast}\pi_{Y}}}X.A\,)$
$\displaystyle\cong\mathop{\mathrm{colim}}\nolimits_{U\in{\mathcal{U}}}(\Pi
x\,\mathord{\in}\,U)\,\\!Y(\pi_{A}(x))=(\Pi_{\mathcal{U}}x\,\mathord{\in}\,X.A)\,\\!Y(\pi_{A}(x))\hbox
to0.0pt{ ,\hss}$

so that $y_{(A,{\mathcal{U}})}$ corresponds to the composite (4.2) as desired.
∎

###  4.3. Relation to model theory

Finally in this section, we relate Theorem 22 to _types_ in model theory.
Recall that, if $\mathbb{T}$ is a (classical, single-sorted) first-order
theory, and we write $\mathbb{T}[x_{1},\dots,x_{n}]$ for the theory obtained
by adjoining new constants $x_{1},\dots,x_{n}$ to $\mathbb{T}$, then a
_complete $n$-type_ of $\mathbb{T}$ is a complete theory extending
$\mathbb{T}[x_{1},\dots,x_{n}]$; equally, it is an ultrafilter on the
Lindenbaum–Tarski algebra $B_{\mathbb{T}[x_{1},\dots,x_{n}]}$ of sentences in
$\mathbb{T}[x_{1},\dots,x_{n}]$ identified up to provable equivalence.

Each $n$-tuple of elements $\vec{a}=a_{1},\dots,a_{n}$ in a $\mathbb{T}$-model
$A$ yields a complete $n$-type $\tau(\vec{a})$, namely the set of all
sentences $\varphi(x_{1},\dots,x_{n})$ of $\mathbb{T}[x_{1},\dots,x_{n}]$ such
that $A\vDash\varphi(a_{1},\dots,a_{n})$; we say that the $n$-tuple $\vec{a}$
_realises_ the type $\tau(\vec{a})$. Many important questions in model theory
revolve around the existence, or otherwise, of tuples of elements which
realise a given type. As we now show, we can obtain the realisation relation
between $n$-types of $\mathbb{T}$ and $n$-tuples in a $\mathbb{T}$-model by
applying Theorem 22 with ${\mathcal{C}}$ taken to be the _classifying Boolean
pretopos_ of $\mathbb{T}$.

The classifying Boolean pretopos of a first-order theory has a characterising
property analogous to that of the Lindenbaum–Tarski algebra $B_{\mathbb{P}}$
of a (classical) propositional theory $\mathbb{P}$. Indeed, there is a
standard notion of _model_ of a propositional theory $\mathbb{P}$ in a Boolean
algebra $C$, and the Lindenbaum–Tarski algebra $B_{\mathbb{P}}$ of all
$\mathbb{P}$-sentences modulo $\mathbb{P}$-provable equality, is the
_universal_ Boolean algebra which models $\mathbb{P}$. By this, we mean that
models of $\mathbb{P}$ in a Boolean algebra $C$ are in bijection with Boolean
homomorphisms $B_{\mathbb{P}}\rightarrow C$.

The classifying Boolean pretopos of a first-order theory $\mathbb{T}$ has a
similar property: it is the universal Boolean pretopos which models
$\mathbb{T}$. We now make this precise. First, a _pretopos_ is a category
which is finitely complete, extensive and also _Barr-exact_ [1], meaning that
it has well-behaved quotients of equivalence relations; while a pretopos is
_Boolean_ if it is so _qua_ extensive category. If ${\mathcal{C}}$ and
${\mathcal{D}}$ are pretoposes, then a _pretopos morphism_
$F\colon{\mathcal{C}}\rightarrow{\mathcal{D}}$ is a functor preserving finite
limits, finite coproducts and regular epimorphisms; we write
$\mathsf{Pretop}({\mathcal{C}},{\mathcal{D}})$ for the category of pretopos
morphisms and all natural transformations.

There is a standard notion of _model_ of a first-order theory $\mathbb{T}$ in
a Boolean pretopos ${\mathcal{C}}$—see, for example [26, §D1.2]—and these
comprise the objects of a category
$\mathbb{T}\text{-}\mathrm{\mathcal{M}od}_{e}({\mathcal{C}})$ whose maps are
elementary embeddings. If ${\mathcal{C}}$ and ${\mathcal{D}}$ are Boolean
pretoposes, then any pretopos morphism
$F\colon{\mathcal{C}}\rightarrow{\mathcal{D}}$ preserves $\mathbb{T}$-models
and so induces a functor
$F_{\ast}\colon\mathbb{T}\text{-}\mathrm{\mathcal{M}od}_{e}({\mathcal{C}})\rightarrow\mathbb{T}\text{-}\mathrm{\mathcal{M}od}_{e}({\mathcal{D}})$.

######  Definition 25.

A _classifying Boolean pretopos_ for a first-order theory $\mathbb{T}$ is a
Boolean pretopos $\mathcal{C}l(\mathbb{T})$ endowed with a $\mathbb{T}$-model
$\mathbf{G}\in\mathbb{T}\text{-}\mathrm{\mathcal{M}od}_{e}(\mathcal{C}l(\mathbb{T}))$
such that, for any Boolean pretopos ${\mathcal{D}}$, the following functor is
an equivalence:

(4.3) $\displaystyle\mathsf{Pretop}(\mathcal{C}l(\mathbb{T}),{\mathcal{D}})$
$\displaystyle\rightarrow\mathbb{T}\text{-}\mathrm{\mathcal{M}od}_{e}({\mathcal{D}})$
$\displaystyle F$ $\displaystyle\mapsto F_{*}(\mathbf{G})\hbox to0.0pt{
.\hss}$

To construct the classifying Boolean pretopos of a first-order theory
$\mathbb{T}$, we first form its _first-order syntactic category_
${\mathcal{C}}_{\mathbb{T}}^{\mathrm{fo}}$ whose objects are “formal
$\mathbb{T}$-definable sets” $\\{\vec{x}:\varphi(\vec{x})\\}$ (i.e., first-
order formulae-in-context) and whose maps are $\mathbb{T}$-provable
equivalence classes of $\mathbb{T}$-provably functional relations from
$\\{\vec{x}:\varphi(\vec{x})\\}$ to $\\{\vec{y}:\psi(\vec{y})\\}$; see, for
example [26, §D1.4]. The classifying Boolean pretopos
$\mathcal{C}l(\mathbb{T})$ is now obtained by freely adjoining finite
coproducts and coequalisers of equivalence relations to
${\mathcal{C}}_{\mathbb{T}}^{\mathrm{fo}}$ while preserving its existing
finite unions and image factorisations—see [25, Proposition A1.4.5 & Corollary
A3.3.10] for the necessary constructions. Alternatively, we can obtain
$\mathcal{C}l(\mathbb{T})$ as the first-order syntactic category of
$\mathbb{T}^{\mathsf{eq}}$, where $({\mathord{\text{--}}})^{\mathsf{eq}}$ is
Shelah’s _elimination of imaginaries_ ; this observation is due to Makkai and
Reyes [42], and is explained in detail in [24].

We will not describe the generic $\mathbb{T}$-model $\mathbf{G}$ in
$\mathcal{C}l(\mathbb{T})$ explicitly; however, part of its genericity is the
fact that $\mathrm{Sum}_{\mathcal{C}l(\mathbb{T})}(G)$ is the
Lindenbaum–Tarski algebra $B_{\mathbb{T}[x]}$. More generally
$\mathrm{Sub}_{\mathcal{C}l(\mathbb{T})}(G^{n})$ is the corresponding
Lindenbaum–Tarski algebra $B_{\mathbb{T}[x_{1},\dots,x_{n}]}$. It follows that
an ultrafilter on $G^{n}\in\mathcal{C}l(\mathbb{T})$ is exactly a complete
$n$-type of $\mathbb{T}$. Now, since ${\mathcal{D}}=\mathrm{\mathcal{S}et}$ is
a Boolean pretopos, we obtain from (4.3) and Theorem 22 a string of functors

$\mathbb{T}\text{-}\mathrm{\mathcal{M}od}_{e}(\mathrm{\mathcal{S}et})\ext@arrow
01{20}0\rightarrowfill@{}{\simeq}\mathsf{Pretop}(\mathcal{C}l(\mathbb{T}),\mathrm{\mathcal{S}et})\ext@arrow
01{20}0\rightarrowfill@{}{\subseteq}\mathsf{FC}(\mathcal{C}l(\mathbb{T}),\mathrm{\mathcal{S}et})\ext@arrow
01{20}0\rightarrowfill@{}{\simeq}[\mathcal{UF}_{\mathcal{C}l(\mathbb{T})},\mathrm{\mathcal{S}et}]$

assigning to each (ordinary) $\mathbb{T}$-model $\mathbf{M}$ both a functor
$M\colon\mathcal{C}l(\mathbb{T})\rightarrow\mathrm{\mathcal{S}et}$ and a
functor
$\tilde{M}\colon\mathcal{UF}_{\mathcal{C}l(\mathbb{T})}\rightarrow\mathrm{\mathcal{S}et}$.
In this context, the passage from $M$ to $\tilde{M}$ was described by Makkai
in [38], who also observed its model-theoretic import: it encodes the types
realised by tuples of elements of the model $\mathbf{M}$.

Indeed, the pretopos morphsim
$M\colon\mathcal{C}l(\mathbb{T})\rightarrow\mathrm{\mathcal{S}et}$
corresponding to the model $\mathbf{M}$ sends $G$ to the underlying set
${\left|{\mathbf{M}}\right|}$ of the model, sends $G^{n}$ to
${{\left|{\mathbf{M}}\right|}}^{n}$ and sends
$\varphi\in\mathrm{Sum}_{\mathcal{C}l(\mathbb{T})}(G^{n})$ to the set
$\\{\,\vec{m}\in{{\left|{\mathbf{M}}\right|}}^{n}:\mathbf{M}\vDash\varphi(\vec{m})\,\\}$.
Thus, by (3.6), the value of the corresponding
$\tilde{M}\in[\mathcal{UF}_{\mathcal{C}l(\mathbb{T})},\mathrm{\mathcal{S}et}]$
at a complete $n$-type ${\mathcal{U}}$ is given by the set of $n$-tuples of
elements of $\mathbf{M}$ which realise the type ${\mathcal{U}}$:

$\tilde{M}(X^{n},{\mathcal{U}})=\\{\vec{m}\in{\left|{\mathbf{M}}\right|}^{n}:\varphi\in{\mathcal{U}}\,\Longleftrightarrow\,\mathbf{M}\vDash\varphi(\vec{m})\\}\hbox
to0.0pt{ .\hss}$

##  5\. Second generalisation

In this section, we give our second generalisation of Theorem 13, which
extends the first one to an equivalence
$\mathsf{FC}({\mathcal{C}},{\mathcal{E}})\simeq[\mathcal{UF}_{\mathcal{C}},{\mathcal{E}}]$,
where ${\mathcal{C}}$ is extensive as before, and now ${\mathcal{E}}$ is any
locally connected Grothendieck topos. We then use this result to reconstruct
the indexed sum of ultrafilters, and in the process of doing so construct
interesting and natural bicategories of _ultramatrices_ and _ultraspans_.
Finally, we describe how this relates to the _ultracategories_ of [40].

###  5.1. Generalising the codomain category

A locally small category ${\mathcal{E}}$ is a _Grothendieck topos_ if it is
equivalent to the category of sheaves on a small site; see, for example, [36,
Chapter III]. Equivalently, by Giraud’s theorem (cf. [36, Appendix]),
${\mathcal{E}}$ is a Grothendieck topos just when it is finitely complete,
Barr-exact and infinitary extensive with a small generating set.

In any Grothendieck topos ${\mathcal{E}}$, the functor
$\Gamma={\mathcal{E}}(1,{\mathord{\text{--}}})\colon{\mathcal{E}}\rightarrow\mathrm{\mathcal{S}et}$
has a left adjoint
$\Delta\colon\mathrm{\mathcal{S}et}\rightarrow{\mathcal{E}}$ which sends a set
$X$ to the coproduct $\Sigma_{x\in X}1$. We say that ${\mathcal{E}}$ is
_locally connected_ (or _molecular_ [3]) if $\Delta$ has a further left
adjoint $\pi_{0}\colon{\mathcal{E}}\rightarrow\mathrm{\mathcal{S}et}$. For
example, by [14, p.414, Ex. 7.6], the topos of sheaves on a space $X$ is
locally connected just when $X$ is locally connected in the usual sense; in
this case,
$\pi_{0}\colon\mathrm{\mathcal{S}h}(X)\rightarrow\mathrm{\mathcal{S}et}$ sends
a sheaf to the set of connected components of the corresponding étale space
over $X$.

######  Theorem 26.

Let ${\mathcal{C}}$ be extensive and ${\mathcal{E}}$ a locally connected
Grothendieck topos. The category $\mathsf{FC}({\mathcal{C}},{\mathcal{E}})$ is
equivalent to $[\mathcal{UF}_{\mathcal{C}},{\mathcal{E}}]$ via an equivalence
whose two directions are given by the formulae (3.6) and (3.7).

In proving this, we require a straightforward generalisation of the
equivalence
$[\operatorname{el}X,\mathrm{\mathcal{S}et}]\simeq[{\mathcal{A}},\mathrm{\mathcal{S}et}]/X$
of (3.3) to an equivalence

(5.1)
$[\operatorname{el}X,{\mathcal{E}}]\simeq[{\mathcal{A}},{\mathcal{E}}]/\Delta
X$

for any Grothendieck topos ${\mathcal{E}}$. The generalisation makes use of
the fact that ${\mathcal{E}}$ is infinitary extensive; this means that it has
all small coproducts, and that for any set $X$, the coproduct functor
$\Sigma\colon\textstyle\prod_{x\in
X}({\mathcal{E}}/A_{x})\rightarrow{\mathcal{E}}/(\Sigma_{i\in X}A_{x})$ is an
equivalence of categories. Taking each $A_{x}$ to be terminal and using
${\mathcal{E}}/1\cong{\mathcal{E}}$, we deduce that

$\Sigma\colon{\mathcal{E}}^{X}\rightarrow{\mathcal{E}}/\Delta X$

is an equivalence for any set $X$, with pseudoinverse given (necessarily) by
pullback along the coproduct coprojections. By using this equivalence in place
of (2.1), we may generalise (3.3) to the desired equivalence (5.1). Much as
before, $Y\in[\operatorname{el}X,{\mathcal{E}}]$ is sent to
$\pi\colon\int\\!Y\rightarrow\Delta X$ whose component
$\pi_{A}\colon(\int\\!Y)A\rightarrow\Delta XA$ is the coproduct of the family
of maps $(Y(A,x)\rightarrow 1)_{x\in XA}$; while conversely, $p\colon
E\rightarrow X$ in $[{\mathcal{A}},{\mathcal{E}}]/\Delta X$ is sent to
$\tilde{E}\in[\operatorname{el}X,{\mathcal{E}}]$ wherein $\tilde{E}(A,x)$ is
the pullback of $p_{A}\colon EA\rightarrow\Delta XA$ along $\Delta
x\colon\Delta 1\rightarrow\Delta XA$.

###### Proof of Theorem 26.

Since
$\pi_{0}\dashv\Delta\dashv\Gamma\colon{\mathcal{E}}\rightarrow\mathrm{\mathcal{S}et}$,
both $\pi_{0}$ and $\Delta$ preserve finite coproducts, so inducing an
adjunction
$\pi_{0}\circ({\mathord{\text{--}}})\dashv\Delta\circ({\mathord{\text{--}}})\colon\mathsf{FC}({\mathcal{C}},\mathrm{\mathcal{S}et})\rightarrow\mathsf{FC}({\mathcal{C}},{\mathcal{E}})$,
whose right adjoint must send the terminal object
$\beta\in[{\mathcal{C}},\mathrm{\mathcal{S}et}]$ to a terminal object
$\Delta\beta\in\mathsf{FC}({\mathcal{C}},{\mathcal{E}})$. As ${\mathcal{C}}$
and ${\mathcal{E}}$ are extensive, it follows from this and Lemma 19 that
$\mathsf{FC}({\mathcal{C}},{\mathcal{E}})\cong[{\mathcal{C}},{\mathcal{E}}]\,/_{\mathrm{sc}}\,\Delta\beta$
where to the right we have the full subcategory of the slice category on the
sum-cartesian transformations; recall that _sum-cartesian_ means that the
naturality squares at coproduct coprojections are pullbacks.

Using (5.1) we have, like before, an equivalence
$[{\mathcal{C}},{\mathcal{E}}]/\Delta\beta\simeq[\operatorname{el}\beta,{\mathcal{E}}]\cong[\mathcal{UE}_{\mathcal{C}},{\mathcal{E}}]$;
and, like before, an object $p\colon E\rightarrow\Delta\beta$ to the left is
sum-cartesian just when the corresponding
$\tilde{E}\in[\mathcal{UE}_{\mathcal{C}},{\mathcal{E}}]$ inverts the class
${\mathcal{M}}_{\Sigma}$ of continuous coproduct coprojections. Thus
$\mathsf{FC}({\mathcal{C}},{\mathcal{E}})\cong[{\mathcal{C}},{\mathcal{E}}]\,/_{\mathrm{sc}}\,\Delta\beta\simeq[\mathcal{UF}_{\mathcal{C}},{\mathcal{E}}]$
as desired.

It remains to show that the two directions of the equivalence are given as in
(3.6) and (3.7). In the latter case this is clear from the construction using
(5.1). In the other direction, if
$A\in\mathsf{FC}({\mathcal{C}},{\mathcal{E}})$, then the corresponding
$\smash{\tilde{A}}\in[\mathcal{UE}_{\mathcal{C}},{\mathcal{E}}]$ has its value
at $(X,{\mathcal{U}})$ given by the pullback to the left in:

$\textstyle{{\tilde{A}(X,{\mathcal{U}})}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{{AX}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\tau_{X}}$$\textstyle{{\Delta
1}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\Delta{\mathcal{U}}}$$\textstyle{{\Delta\beta
X}}$
$\textstyle{{AU}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{Am}$$\scriptstyle{\tau_{U}}$$\textstyle{{AX}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\tau_{X}}$$\textstyle{{\Delta\beta
U}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\Delta\beta
m}$$\textstyle{{\Delta\beta X}\hbox to0.0pt{ ,\hss}}$

where $\tau\colon A\rightarrow\Delta\beta$ is induced by terminality of
$\Delta\beta$ in $\mathsf{FC}({\mathcal{C}},{\mathcal{E}})$. Note, however,
that ${\mathcal{U}}\colon 1\rightarrow\beta X$ in $\mathrm{\mathcal{S}et}$ is
the meet of the subobjects $(\beta U\rightarrowtail\beta
X)_{U\in{\mathcal{U}}}$. Since $\Delta$ is a right adjoint, it preserves
meets, as does pullback along $\tau_{X}$; consequently,
$\tilde{A}(X,{\mathcal{U}})$ is the meet of the subobjects
$(\tau_{X}^{-1}(\Delta\beta U)\rightarrowtail AX)_{U\in{\mathcal{U}}}$. But
since $\tau$ is sum-cartesian by Lemma 19, the square right above is a
pullback for any $m\colon U\rightarrowtail X$ in ${\mathcal{U}}$, and so we
conclude that $\tilde{A}$ is given as in (3.6) by

$\tilde{A}(X,{\mathcal{U}})\cong\bigcap_{U\in{\mathcal{U}}}AU\subseteq AX\hbox
to0.0pt{ .\hss}\qed$

###  5.2. Ultramatrices, ultraspans and the relation to indexed sums

We now wish to describe how this result recaptures the indexed sum of
ultrafilters. In fact, we will do something slightly more general to draw as
perfect an analogy as possible with Proposition 16. The first step there was
to transport the strict monoidal structure on the category
$\mathsf{FC}(\mathrm{\mathcal{S}et},\mathrm{\mathcal{S}et})$ to obtain a
monoidal structure on the equivalent $[\mathcal{UF},\mathrm{\mathcal{S}et}]$.
The analogue here is to transport the compositional structure of a
$2$-category of finite-coproduct-preserving functors along equivalences of
each of its hom-categories to obtain an equivalent _bicategory_ [4].

######  Definition 27.

  1. (i)

The $2$-category $\mathsf{FC}_{\mathrm{\mathcal{S}et}}$ has sets $X,Y,Z,\dots$
as objects; hom-categories given by
$\mathsf{FC}_{\mathrm{\mathcal{S}et}}(X,Y)=\mathsf{FC}(\mathrm{\mathcal{S}et}^{X},\mathrm{\mathcal{S}et}^{Y})$;
and composition given by the usual composition of functors and natural
transformations.

  2. (ii)

The bicategory $\mathsf{UEsp}$ of _ultrafilter species_ has sets as objects;
hom-categories
$\mathsf{UEsp}(X,Y)=[\mathcal{UF}_{\mathrm{\mathcal{S}et}^{X}},\mathrm{\mathcal{S}et}^{Y}]$;
and composition obtained from that of $\mathsf{FC}_{\mathrm{\mathcal{S}et}}$
by transporting across the equivalences
$\mathsf{FC}(\smash{\mathrm{\mathcal{S}et}^{X}},\smash{\mathrm{\mathcal{S}et}^{Y}})\simeq[\mathcal{UF}_{\mathrm{\mathcal{S}et}^{X}},\smash{\mathrm{\mathcal{S}et}^{Y}}]$.

The nomenclature “ultrafilter species” echoes Joyal’s notion of a species of
structures (_espéces de structures_ [28]), and its generalisation in [16] to a
bicategory $\mathsf{Esp}$ of _generalised species of structures_. We will not
labour the comparison, but suffice it to say that in both bicategories,
composition is given by a substitution formula, which in the case of
$\mathsf{Esp}$ is given by equation (9) of [16], and for $\mathsf{UEsp}$ is
given by a suitable generalisation of (3.8).

In Proposition 16, we reconstructed the tensor product of ultrafilters by
showing the representables in $[\mathcal{UF},\mathrm{\mathcal{S}et}]$ to be
closed under the tensor product. To reconstruct the indexed sum of
ultrafilters, we will similarly show that _pointwise representable_ $1$-cells
in $\mathsf{UEsp}$ are closed under composition. Here,
$F\in\mathsf{UEsp}(X,Y)=[\mathcal{UF}_{\mathrm{\mathcal{S}et}^{X}},\mathrm{\mathcal{S}et}^{Y}]$
is pointwise representable if each functor
$F({\mathord{\text{--}}})(y)\colon\mathcal{UF}_{\mathrm{\mathcal{S}et}^{X}}\rightarrow\mathrm{\mathcal{S}et}$
is representable. The subcategory of pointwise representable functors is
equivalent (via pointwise Yoneda) to the category
$(\mathcal{UF}_{\mathrm{\mathcal{S}et}^{X}})^{Y}$, and so a typical pointwise
representable $1$-cell is presented by a $Y$-indexed family of pairs
$(M_{y}\in\mathrm{\mathcal{S}et}^{X},{\mathcal{U}}_{y}\in\beta(X.M_{y}))$. In
fact, we prefer to think of these data in either one of the following two
alternative ways.

######  Definition 28.

Let $X$ and $Y$ be sets.

  1. (i)

An _ultramatrix_ from $X$ to $Y$ is a pair $(M,{\mathcal{U}})$ composed of a
matrix of sets $M\in\mathrm{\mathcal{S}et}^{X\times Y}$ together with a
$Y$-indexed family of ultrafilters ${\mathcal{U}}_{y}$ on each column sum
$M_{y}\mathrel{\mathop{:}}=(\Sigma x\,\mathord{\in}\,X)\,\\!M(x,y)$.

  2. (ii)

An _ultrafamily_ $(g,{\mathcal{U}})\colon M\rightsquigarrow Y$ is a function
$g\colon M\rightarrow Y$ together with an ultrafilter ${\mathcal{U}}_{y}$ on
each fibre $g^{-1}(y)$. An _ultraspan_ from $X$ to $Y$ is a span with left leg
a function and right leg an ultrafamily:

(5.2)
$\textstyle{M\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{f}$$\scriptstyle{(g,{\mathcal{U}})}$$\textstyle{X}$$\textstyle{Y\hbox
to0.0pt{ .\hss}}$

It is easy to see using (2.1) that both ultramatrices and ultraspans from $X$
to $Y$ correspond to pointwise representables in $\mathsf{UEsp}(X,Y)$, and so
to certain finite-coproduct-preserving functors
$\mathrm{\mathcal{S}et}^{X}\rightarrow\mathrm{\mathcal{S}et}^{Y}$. As in the
introduction, we may call these _generalised ultraproduct functors_. Using
Proposition 24, we see that, one the one hand, the generalised ultraproduct
functor $\mathrm{\mathcal{S}et}^{X}\rightarrow\mathrm{\mathcal{S}et}^{Y}$
encoded by the ultramatrix $(M,{\mathcal{U}})$ is given by:

(5.3) $(\,H(x)\mid x\in
X\,)\qquad\mapsto\qquad\big{(}\,(\Pi_{{\mathcal{U}}_{y}}(x,m)\,\mathord{\in}\,M_{y})\,\\!H(x)\mid
y\in Y\,\big{)}\hbox to0.0pt{ .\hss}$

On the other hand, the ultraspan $(f,(g,{\mathcal{U}}))\colon X\rightarrow Y$
encodes the functor

$\mathrm{\mathcal{S}et}^{X}\ext@arrow
01{20}0\rightarrowfill@{}{\mathrm{\mathcal{S}et}^{f}}\mathrm{\mathcal{S}et}^{M}\ext@arrow
01{20}0\rightarrowfill@{}{\Pi_{(g,{\mathcal{U}})}}\mathrm{\mathcal{S}et}^{Y}$

where $\Pi_{(g,{\mathcal{U}})}$ is given by “ultraproduct on each fibre”;
i.e., its $y$-component is given by restriction
$\mathrm{\mathcal{S}et}^{M}\rightarrow\mathrm{\mathcal{S}et}^{g^{-1}y}$
followed by ultraproduct
$\Pi_{{\mathcal{U}}_{y}}\colon\mathrm{\mathcal{S}et}^{g^{-1}y}\rightarrow\mathrm{\mathcal{S}et}$.

The next two definitions are intended to describe how pointwise representable
$1$-cells in $\mathsf{UEsp}$ compose in terms of the representing
ultramatrices or ultraspans.

######  Definition 29.

If $(M,{\mathcal{U}})$ and $(N,{\mathcal{V}})$ are ultramatrices from $X$ to
$Y$ and from $Y$ to $Z$, then their _composition_ is the ultramatrix $(N\cdot
M,{\mathcal{V}}\cdot{\mathcal{U}})$ from $X$ to $Z$ whose first component is
given by the usual matrix multiplication:

$(N\cdot M)(x,z)=(\Sigma y\,\mathord{\in}\,Y)\,\\!(N(y,z)\times M(x,y))\hbox
to0.0pt{ .\hss}$

As for the second component, note that for each $z\in Z$ we have an
isomorphism

(5.4) $(\Sigma(y,n)\,\mathord{\in}\,N_{z})\,\\!M_{y}\cong(N\cdot M)_{z}$

sending $(y,n,x,m)$ to $(x,y,n,m)$. We can therefore define the ultrafilter
$({\mathcal{V}}\cdot{\mathcal{U}})_{z}$ on $(N\cdot M)_{z}$ to be the
transport across (5.4) of the ultrafilter on
$(\Sigma(y,n)\,\mathord{\in}\,N_{z})\,\\!M_{y}$ given by the indexed sum
$(\Sigma_{{\mathcal{V}}_{z}}(y,n)\\!\in\\!N_{z})\,\\!{\mathcal{U}}_{y}$.

######  Definition 30.

Given ultraspans $(f,(g,{\mathcal{U}}))\colon X\rightarrow Y$ and
$(h,(k,{\mathcal{V}}))\colon Y\rightarrow Z$, their _composition_ is the
ultraspan whose legs are given by the outer composites in:

$\textstyle{M\times_{Y}N\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{p}$$\scriptstyle{(q,{\mathcal{W}})}$$\textstyle{M\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{f}$$\scriptstyle{(g,{\mathcal{U}})}$$\textstyle{N\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{h}$$\scriptstyle{\scriptstyle(k,{\mathcal{V}})}$$\textstyle{X}$$\textstyle{Y}$$\textstyle{Z\hbox
to0.0pt{ .\hss}}$

Here, $p$ and $q$ constitute a pullback of $g$ and $h$ in
$\mathrm{\mathcal{S}et}$. To the top right, the pullback ultrafamily
$(q,{\mathcal{W}})\colon M\times_{Y}N\rightsquigarrow N$ has
${\mathcal{W}}_{n}$ given by the transport of ${\mathcal{U}}_{hn}$ across the
isomorphism $g^{-1}(hn)\cong q^{-1}(n)$. Finally, the composite
$(kq,{\mathcal{V}}{\mathcal{W}})$ of the ultrafamilies $(q,{\mathcal{W}})$ and
$(k,{\mathcal{V}})$ has $({\mathcal{V}}{\mathcal{W}})_{z}$ given by the
transport of
$(\Sigma_{{\mathcal{V}}_{z}}n\\!\in\\!k^{-1}z)\,\\!{\mathcal{W}}_{n}$ across
the isomorphism $(\Sigma n\\!\in\\!k^{-1}z)\,\\!q^{-1}n\cong(kq)^{-1}z$.

The validity of these descriptions is confirmed by:

######  Proposition 31.

The pointwise representable $1$-cells in $\mathsf{UEsp}$ are closed under
composition, with the induced composition on ultramatrices and ultraspans
given as in Definition 29 and Definition 30 respectively.

###### Proof.

The identity $1$-cells in $\mathsf{UEsp}$ are easily seen to be pointwise
representable. As for binary composition, the composition laws in Definitions
29 and 30 correspond under (2.1), so that it suffices to check the claim on
ultramatrices. So let $F\in\mathsf{UEsp}(X,Y)$ and $G\in\mathsf{UEsp}(Y,Z)$ be
represented by the respective ultramatrices $(M,{\mathcal{U}})$ and
$(N,{\mathcal{V}})$. By (5.3), the corresponding generalised ultraproduct
functors
$\int\\!F\in\mathsf{FC}(\mathrm{\mathcal{S}et}^{X},\mathrm{\mathcal{S}et}^{Y})$
and
$\int\\!G\in\mathsf{FC}(\mathrm{\mathcal{S}et}^{Y},\mathrm{\mathcal{S}et}^{Z})$
have respective actions on objects

$\textstyle(\int\\!F)(H)(y)=(\Pi_{{\mathcal{U}}_{y}}(x,m)\,\mathord{\in}\,M_{y})\,\\!H(x)\
\text{ and }\
\textstyle(\int\\!G)(K)(z)=(\Pi_{{\mathcal{V}}_{z}}(y,n)\,\mathord{\in}\,N_{z})\,\\!K(y)\hbox
to0.0pt{ .\hss}$

Therefore $\int
GF\cong\int\\!G\circ\int\\!F\colon\mathrm{\mathcal{S}et}^{X}\rightarrow\mathrm{\mathcal{S}et}^{Z}$
satisfies

$\displaystyle\textstyle(\int\\!GF)(H)(z)$
$\displaystyle\cong(\Pi_{{\mathcal{V}}_{z}}(y,n)\,\mathord{\in}\,N_{z})(\Pi_{{\mathcal{U}}_{y}}(x,m)\,\mathord{\in}\,M_{y})\,\\!H(x)$
$\displaystyle\cong(\Pi_{(\Sigma_{{\mathcal{V}}_{z}}(y,n)\\!\in\\!N_{z})\,\\!{\mathcal{U}}_{y}}(y,n,x,m)\,\mathord{\in}\,(\Sigma(y,n)\,\mathord{\in}\,N_{z})\,\\!M_{y})\,\\!H(x)$
$\displaystyle\cong(\Pi_{({\mathcal{V}}\cdot{\mathcal{U}})_{z}}(x,y,n,m)\,\mathord{\in}\,(N\cdot
M)_{z})\,\\!H(x)\hbox to0.0pt{ ,\hss}$

using Proposition 9 and the definition of
$({\mathcal{V}}\cdot{\mathcal{U}})_{z}$. Thus, by (5.3) again, the pointwise
representability of $GF$ is witnessed by the ultramatrix $(N\cdot
M,{\mathcal{V}}\cdot{\mathcal{U}})$. ∎

It follows from this result that there are bicategories $\mathsf{UMtx}$
(resp., $\mathsf{US}$) in which objects are sets; $1$-cells are ultramatrices
(resp., ultraspans) composing as in Definition 29 (resp., Definition 30); and
$2$-cells are determined by the requirement that each bicategory be
biequivalent to the locally full sub-bicategory of $\mathsf{UEsp}$ on the
pointwise representable $1$-cells.

It remains to show that the composition laws in $\mathsf{UMtx}$ and
$\mathsf{US}$ allow us to reconstruct the indexed sum of ultrafilters, so
fulfilling the objective of this section. This is easiest to see in the case
of $\mathsf{US}$. Suppose that we are given a set $X$ equipped with an
ultrafilter ${\mathcal{U}}$ and an $X$-indexed family of sets $Y(x)$ each
equipped with an ultrafilter ${\mathcal{V}}(x)$. We can represent these data
as a pair of composable ultraspans as to the left in:

$\textstyle{X.Y\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{1}$$\scriptstyle{(\pi_{Y},{\mathcal{V}})}$$\textstyle{X\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{1}$$\scriptstyle{(!,{\mathcal{U}})}$$\textstyle{X.Y}$$\textstyle{X}$$\textstyle{1}$
$\textstyle{X.Y\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{1}$$\scriptstyle{(!,{\mathcal{U}}.{\mathcal{V}})}$$\textstyle{X.Y}$$\textstyle{1\hbox
to0.0pt{ ,\hss}}$

whose composite encodes the indexed sum ${\mathcal{U}}.{\mathcal{V}}$ as right
above.

######  Remark 32.

In Remark 17 above, we explained how categories _enriched_ over the monoidal
category $[\mathcal{UF},\mathrm{\mathcal{S}et}]$ can be thought of as ordinary
categories endowed with abstract ultrapower functors. It is possible to extend
this so as to capture categories endowed with abstract _ultraproduct_ functors
by using the theory of _categories enriched in a bicategory_ as in [47].

Rather than $[\mathcal{UF},\mathrm{\mathcal{S}et}]$-enriched categories with
copowers by representables, we consider $\mathsf{UEsp}$-enriched categories
with copowers by pointwise representable $1$-cells. We might guess that such
enriched categories correspond to ordinary categories ${\mathcal{C}}$
admitting abstract ultraproduct functors
$\Pi_{\mathcal{U}}\colon{\mathcal{C}}^{X}\rightarrow{\mathcal{C}}$. The
reality is slightly more subtle; while some details still require sorting out,
it appears that the $\mathsf{UEsp}$-enriched categories with copowers as above
correspond to _$\mathrm{\mathcal{S}et}$ -indexed prestacks_—i.e., pseudo-
functors
$\mathbb{C}\colon\mathrm{\mathcal{S}et}^{\mathrm{op}}\rightarrow\mathsf{CAT}$
satisfying a descent condition—equipped with suitably coherent abstract
ultrapower functors
$\Pi_{(f,{\mathcal{U}})}\colon\mathbb{C}_{X}\rightarrow\mathbb{C}_{Y}$ for
each ultrafamily $(f,{\mathcal{U}})\colon X\rightsquigarrow Y$.

While the details must await a further paper, these observations draw an
interesting link to Makkai’s _ultracategories_ [40, 41]. As in the
introduction, an ultracategory is a category endowed with abstract
ultraproduct structure, as well as interpretations for any _ultramorphism_ ,
i.e., “definable map between ultraproducts”. Makkai’s main result is that the
ultracategory structure on the category of models of a coherent theory
$\mathbb{T}$ in either intuitionistic or classical first-order logic is
sufficient to reconstruct $\mathbb{T}$ to within Morita equivalence; more
precisely, it suffices to reconstruct the classifying pretopos of
$\mathbb{T}$.

These results of Makkai were given new proofs by Lurie in [35], with a
significantly simplified definition of what it means for an ultracategory to
admit interpretations of any ultramorphism; and although we have not yet
completed the analysis, it seems that this additional structure is exactly
what $\mathsf{UEsp}$-enrichment provides besides the existence of abstract
ultraproduct functors. In future work we hope to investigate this further with
a view to giving a purely enriched-categorical proof of Makkai’s
reconstruction result.

##  6\. Locally connected classifying toposes

In Section 4.3, we discussed the algebraic semantics for _classical_
propositional theories in Boolean algebras, and for first-order theories in
Boolean pretoposes. There are similar semantics for certain fragments of
intuitionistic logic: in particular, the _coherent_ fragment, which allows
only the logical connectives $\exists,\vee,\wedge,\top,\bot$, has an algebraic
semantics in distributive lattices (for the propositional case) and in
pretoposes (for the first-order case); see, for example [42].

Now for classical propositional theories, there is a restricted semantics
valued not in Boolean algebras but _complete atomic_ Boolean algebras. Rather
than the Lindenbaum–Tarski algebra $B_{\mathbb{P}}$, the appropriate universal
model in this context is the power-set algebra ${\mathcal{P}}(T_{\mathbb{P}})$
on the set $T_{\mathbb{P}}$ of complete theories extending $\mathbb{P}$, with
the universal valuation of $\mathbb{P}$ in ${\mathcal{P}}(T_{\mathbb{P}})$
sending each primitive proposition $\varphi$ to the set of complete extensions
which validate it. Since $T_{\mathbb{P}}$ is equally the set
$\beta(B_{\mathbb{P}})$ of ultrafilters on $B_{\mathbb{P}}$, the passage from
$B_{\mathbb{P}}$ to ${\mathcal{P}}(T_{\mathbb{P}})$ can be understood in terms
of the lattice-theoretic construction of _canonical extension_ [27]: in
general, for a Boolean algebra $B$, its canonical extension is the power-set
algebra $B^{\delta}\mathrel{\mathop{:}}={\mathcal{P}}(\beta B)$.

Similarly, for coherent intuitionistic propositional theories, the semantics
in distributive lattices restricts to one valued in completely distributive
algebraic lattices; these are equally well the down-set lattices of posets,
and posets are the same thing as symmetric, transitive Kripke frames, so this
is really another view on the _Kripke semantics_ of intuitionistic logic [46,
§2.5]. In this context, the classifying distributive lattice $D_{\mathbb{P}}$
of a theory $\mathbb{P}$ is replaced by its canonical extension
$D_{\mathbb{P}}^{\delta}$, constructible as in [21] as the downset-lattice of
the poset of prime filters in $D_{\mathbb{P}}$ (ordered by reverse inclusion);
this is an algebraic reformulation of the construction of the canonical Kripke
model [46, Definition 2.6.4] of an intuitionistic propositional theory.

An obvious question is whether the alternate semantics detailed above lift
from propositional to first-order logic. A variety of positive answers have
been given to this question. One positive answer is given in [39]; there,
Makkai introduces the notion of a _prime-generated topos_ , as a Grothendieck
topos whose subobject lattices are completely distributive algebraic111This is
not the original definition of prime-generation from [38], but an equivalent
one from [2, §3].. He then considers semantics for a coherent intuitionistic
first-order theory $\mathbb{T}$ valued in prime-generated toposes, and
constructs the universal such model in what he calls the _topos of types_ of
$\mathbb{T}$. This is obtained from the classifying pretopos
${\mathcal{C}}=\mathcal{C}l(\mathbb{T})$ of $\mathbb{T}$ by a “categorified
canonical extension”, obtained by first forming a category
${\mathcal{P}}{\mathcal{F}}_{\mathcal{C}}$ of _prime filters_ in
${\mathcal{C}}$, defined similarly to our $\mathcal{UF}_{\mathcal{C}}$, and
then taking a suitable sheaf subcategory $\tau(\mathcal{C}l(\mathbb{T}))$ of
$[{\mathcal{P}}{\mathcal{F}}_{\mathcal{C}}^{\mathrm{op}},\mathrm{\mathcal{S}et}]$.
The name “topos of types” for $\tau(\mathcal{C}l(\mathbb{T}))$ derives from
the fact that, as Makkai puts it, it gives ‘a reasonable codification of the
‘discrete’ (non topological) syntactical structure of types of the theory”
[38, p.196]. The idea that the passage
$\mathcal{C}l(\mathbb{T})\mapsto\tau(\mathcal{C}l(\mathbb{T}))$ should be seen
as a kind of canonical extension was made precise by Coumans in [13].

In this section, we take a slightly different view on lifting canonical
extension to the first-order coherent context. In Makkai’s approach, the
distributive subobject lattices of $\mathcal{C}l(\mathbb{T})$ are completed
via canonical extension to the completely distributive algebraic subobject
lattices of $\tau(\mathcal{C}l(\mathbb{T}))$. For us, the focus will instead
be on the Boolean algebras of coproduct summands in
$\mathcal{C}l(\mathbb{T})$—corresponding logically to decidable predicates in
$\mathbb{T}$—which will be completed via canonical extension to complete
atomic Boolean algebras of coproduct-summands. The property of having complete
atomic Boolean algebras of coproduct-summands is, by [3, Theorem 15],
characteristic of locally connected Grothendieck toposes, and so what we aim
to describe in the _locally connected classifying topos_ of a given pretopos
${\mathcal{C}}$. The existence of this follows from results of [18], but the
description there is rather inexplicit; we aim to give a concrete construction
in terms of sheaves on the category of ultrafilters, and to compare this to
the toposes of types of Makkai and others.

###  6.1. The lextensive case

In this section, as a warm-up to our main result, we construct the locally
connected classifying topos of a small _lextensive_ category—that is, a
category which is both finitely complete and extensive.

We first make precise what we mean by this. Recall that a _geometric morphism_
$f\colon{\mathcal{E}}\rightarrow{\mathcal{F}}$ between toposes is an adjoint
pair of functors $f^{\ast}\dashv
f_{\ast}\colon{\mathcal{E}}\rightarrow{\mathcal{F}}$ such that $f^{\ast}$ (the
_inverse image functor_) preserves finite limits. We write $\mathsf{LCGTop}$
for the $2$-category of locally connected Grothendieck toposes, geometric
morphisms and natural transformations $f^{\ast}\Rightarrow g^{\ast}$, and
write $\mathsf{Lext}$ for the $2$-category of lextensive categories,
lextensive functors (i.e., ones preserving finite limits and finite
coproducts) and arbitrary natural transformations. As every locally connected
Grothendieck topos and every inverse image functor between such is lextensive,
we have a forgetful $2$-functor
$\mathsf{LCGTop}^{\mathrm{op}}\rightarrow\mathsf{Lext}$.

######  Definition 33.

A _locally connected classifying topos_ for an extensive category
${\mathcal{C}}$ is a left biadjoint at ${\mathcal{C}}$ for the forgetful
$2$-functor $\mathsf{LCGTop}^{\mathrm{op}}\rightarrow\mathsf{Lext}$.

Here, and in what follows, when we speak of a _left biadjoint at $X$_ for a
$2$-functor $U\colon\mathsf{A}\rightarrow\mathsf{B}$, we mean a
birepresentation (in the sense of [45]) for the $2$-functor
$\mathsf{B}(X,U{\mathord{\text{--}}})\colon\mathsf{A}\rightarrow\mathsf{CAT}$.
More concretely, then, a locally connected classifying topos for the
lextensive ${\mathcal{C}}$ comprises a locally connected Grothendieck topos
$\mathrm{\mathcal{L}c}({\mathcal{C}})$ and a lextensive functor
$\eta\colon{\mathcal{C}}\rightarrow\mathrm{\mathcal{L}c}({\mathcal{C}})$ which
is _universal_ in the sense that, for each locally connected Grothendieck
topos ${\mathcal{E}}$, we have an equivalence:

(6.1)
$\mathsf{LCGTop}({\mathcal{E}},\mathrm{\mathcal{L}c}({\mathcal{C}}))\simeq\mathsf{Lext}({\mathcal{C}},{\mathcal{E}})\\\
$

induced by the assignment $f\mapsto f^{\ast}\circ\eta$.

Our goal is to give an explicit construction of a locally connected
classifying topos for any small lextensive category ${\mathcal{C}}$. For this,
we require the result sometimes known as _Diaconescu’s theorem_ ; it can be
found proved in, for example, [36, Theorem VII.7.2].

######  Proposition 34.

If ${\mathcal{A}}$ is a small category, then the presheaf topos
$[{\mathcal{A}}^{\mathrm{op}},\mathrm{\mathcal{S}et}]$ classifies flat
functors out of ${\mathcal{A}}$. More precisely, for each Grothendieck topos
${\mathcal{E}}$, the assignment $f\mapsto f^{\ast}\circ y$ induces an
equivalence of categories

(6.2)
$\mathsf{GTop}({\mathcal{E}},[{\mathcal{A}}^{\mathrm{op}},\mathrm{\mathcal{S}et}])\simeq\mathsf{Flat}({\mathcal{A}},{\mathcal{E}})\hbox
to0.0pt{ .\hss}$

Here, we define $\mathsf{Flat}({\mathcal{A}},{\mathcal{E}})$ as the full
subcategory of $[{\mathcal{A}},{\mathcal{E}}]$ on the flat functors, but for
this we should clarify what “flat” means. One definition is that
$F\colon{\mathcal{A}}\rightarrow{\mathcal{E}}$ is flat just when
$\mathrm{Lan}_{y}F\colon[{\mathcal{A}}^{\mathrm{op}},\mathrm{\mathcal{S}et}]\rightarrow{\mathcal{E}}$,
its left Kan extension along the Yoneda embedding of
$[{\mathcal{A}}^{\mathrm{op}},\mathrm{\mathcal{S}et}]$, preserves finite
limits; this is a general categorical definition which makes sense for any
small ${\mathcal{A}}$ and cocomplete ${\mathcal{E}}$. On the other hand, when
${\mathcal{E}}$ is a Grothendieck topos as above, a more explicit
characterisation is possible which generalises a well-known characterisation
when ${\mathcal{E}}=\mathrm{\mathcal{S}et}$.

Given $F\in[{\mathcal{A}},{\mathcal{E}}]$, we write $\operatorname{el}F$ for
the _category of elements_ of $F$: the internal category in ${\mathcal{E}}$
with underlying graph

$\textstyle{\textstyle\sum_{a,b\in{\mathcal{A}}}\sum_{f\in{\mathcal{A}}(a,b)}Da\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{s}$$\scriptstyle{t}$$\textstyle{\textstyle\sum_{a\in{\mathcal{A}}}Da}$

where $s$ maps the $(a,b,f)$-summand to the $a$-summand via $1_{Da}$, and
where $t$ maps the $(a,b,f)$-summand to the $b$-summand via $Df$. There is a
standard notion—see, for example [25, Definition B2.6.2]—of what it means for
an internal category $\mathbb{C}$ in a topos to be _cofiltered_ ; in the
internal language of the topos, it says that “every finite diagram in
$\mathbb{C}$ has a cocone under it”. The key result we will need is the
following; for a proof, see [25, Theorem B3.2.7].

######  Proposition 35.

If ${\mathcal{A}}$ is a small category and ${\mathcal{E}}$ is a Grothendieck
topos, then $F\colon{\mathcal{A}}\rightarrow{\mathcal{E}}$ is flat if and only
if the internal category $\operatorname{el}F$ in ${\mathcal{E}}$ is
cofiltered.

With these preliminaries in place, we can now give:

######  Proposition 36.

If ${\mathcal{C}}$ is small and lextensive, then
$[{\mathcal{UF}_{\mathcal{C}}}^{\mathrm{op}},\mathrm{\mathcal{S}et}]$ is a
locally connected classifying topos for ${\mathcal{C}}$.

###### Proof.

Like any presheaf topos,
$[{\mathcal{UF}_{\mathcal{C}}}^{\mathrm{op}},\mathrm{\mathcal{S}et}]$ is
locally connected. For the classifying property, we must exhibit equivalences
$\mathsf{LCGTop}({\mathcal{E}},[{\mathcal{UF}_{\mathcal{C}}}^{\mathrm{op}},\mathrm{\mathcal{S}et}])\simeq\mathsf{Lext}({\mathcal{C}},{\mathcal{E}})$,
pseudonaturally in ${\mathcal{E}}$, which we will do by composing
pseudonatural equivalences:

(6.3)
$\mathsf{LCGTop}({\mathcal{E}},[{\mathcal{UF}_{\mathcal{C}}}^{\mathrm{op}},\mathrm{\mathcal{S}et}])\ext@arrow
01{20}0\rightarrowfill@{}{\simeq}\mathsf{Flat}(\mathcal{UF}_{\mathcal{C}},{\mathcal{E}})\ext@arrow
01{20}0\rightarrowfill@{}{\simeq}\mathsf{Lext}({\mathcal{C}},{\mathcal{E}})\hbox
to0.0pt{ .\hss}$

The first of these is (6.2). As for the second, we have by Theorem 26 that

(6.4)
$[\mathcal{UF}_{\mathcal{C}},{\mathcal{E}}]\simeq\mathsf{FC}({\mathcal{C}},{\mathcal{E}})$

for any locally connected Grothendieck topos ${\mathcal{E}}$, and by
considering the explicit formula (3.7) for the rightward direction, we see
that these equivalences are pseudonatural in inverse image functors. We will
thus have the desired pseudonatural equivalence if we can show that, in (6.4),
the flat functors on the left-hand side correspond to the finite-limit-
preserving ones on the right.

Towards this goal, we recall from Definition 21 the category
$\mathcal{UE}_{\mathcal{C}}$ of which $\mathcal{UF}_{\mathcal{C}}$ is a
localisation, and consider the span
$\pi\colon{\mathcal{C}}\leftarrow\mathcal{UE}_{\mathcal{C}}\rightarrow\mathcal{UF}_{\mathcal{C}}\colon\iota$
whose two legs are the forgetful functor and the localisation functor
respectively. It is easy to see from the formula (3.7) that the left-to-right
direction of (6.4) sends
$B\colon\mathcal{UF}_{\mathcal{C}}\rightarrow{\mathcal{E}}$ to its image under
the composite functor

$[\mathcal{UF}_{\mathcal{C}},{\mathcal{E}}]\ext@arrow
01{20}0\rightarrowfill@{}{\iota^{\ast}}[\mathcal{UE}_{\mathcal{C}},{\mathcal{E}}]\ext@arrow
01{20}0\rightarrowfill@{}{\mathrm{Lan}_{\pi}}[{\mathcal{C}},{\mathcal{E}}]\hbox
to0.0pt{ .\hss}$

It therefore suffices to prove that:

(i) $B\colon\mathcal{UF}_{\mathcal{C}}\rightarrow{\mathcal{E}}$ is flat if and
only if $B\iota\colon\mathcal{UE}_{\mathcal{C}}\rightarrow{\mathcal{E}}$ is
flat. We saw above that
$\mathcal{UF}_{\mathcal{C}}\cong\mathcal{UE}_{\mathcal{C}}[{\mathcal{M}}_{\Sigma}^{-1}]$,
the localisation at the class of continuous coproduct coprojections. Since
${\mathcal{M}}_{\Sigma}$ is a pullback-stable, composition-closed class of
arrows, there is (for example by [26, Proposition C2.1.9]) a Grothendieck
topology $J$ on $\mathcal{UE}_{\mathcal{C}}$ whose covering sieves are those
which contain any map in ${\mathcal{M}}_{\Sigma}$. The condition for a functor
$F\colon\mathcal{UE}_{\mathcal{C}}^{\mathrm{op}}\rightarrow\mathrm{\mathcal{S}et}$
to be a $J$-sheaf is now precisely the condition that it inverts each
$m\in{\mathcal{M}}_{\Sigma}$, and so we may identify
$[{\mathcal{UF}_{\mathcal{C}}}^{\mathrm{op}},\mathrm{\mathcal{S}et}]$ with
$\mathrm{\mathcal{S}h}(\mathcal{UE}_{\mathcal{C}})$, and the sheafification
adjunction with the adjunction
$\mathrm{Lan}_{\iota}\dashv\iota^{\ast}\colon[{\mathcal{UF}_{\mathcal{C}}}^{\mathrm{op}},\mathrm{\mathcal{S}et}]\rightarrow[{\mathcal{UE}_{\mathcal{C}}}^{\mathrm{op}},\mathrm{\mathcal{S}et}]$;
so in particular, $\mathrm{Lan}_{\iota}$ preserves finite limits. We now use
this to prove the claim. Note that
$\mathrm{Lan}_{y}(B\iota)\cong(\mathrm{Lan}_{y}B)\circ\mathrm{Lan}_{\iota}$,
so that if $B$ is flat, then so too is $B\iota$. On the other hand, since
$\mathrm{Lan}_{\iota}\circ\iota^{\ast}\cong 1$, we have that
$\mathrm{Lan}_{y}B\cong\mathrm{Lan}_{y}(B\iota)\circ\iota^{\ast}$ so that if
$B\iota$ is flat then so too is $B$.

(ii) $F\colon\mathcal{UE}_{\mathcal{C}}\rightarrow{\mathcal{E}}$ is flat if
and only if $\mathrm{Lan}_{\pi}F\colon{\mathcal{C}}\rightarrow{\mathcal{E}}$
preserves finite limits. Since the value of
$\mathrm{Lan}_{\pi}F\colon{\mathcal{C}}\rightarrow{\mathcal{E}}$ at $X$ is
$\sum_{{\mathcal{U}}\in\beta X}F(X,{\mathcal{U}})$, it is an easy calculation
to see that the internal categories $\operatorname{el}F$ and
$\operatorname{el}(\mathrm{Lan}_{\pi}F)$ are isomorphic. So $F$ is flat if and
only if $\mathrm{Lan}_{\pi}F$ is flat. But since ${\mathcal{C}}$ admits all
finite limits, $\mathrm{Lan}_{\pi}F$ is flat if and only if it is finite-
limit-preserving; see, for example [25, Lemma B3.2.5].∎

By tracing the identity geometric morphism on
$[{\mathcal{UF}_{\mathcal{C}}}^{\mathrm{op}},\mathrm{\mathcal{S}et}]$ through
this proof, we see that the universal lextensive functor
$\eta\colon{\mathcal{C}}\rightarrow[{\mathcal{UF}_{\mathcal{C}}}^{\mathrm{op}},\mathrm{\mathcal{S}et}]$
is the image under (3.7) of the Yoneda embedding
$\mathcal{UF}_{\mathcal{C}}\rightarrow[{\mathcal{UF}_{\mathcal{C}}}^{\mathrm{op}},\mathrm{\mathcal{S}et}]$,
and so given by:

$\eta(X)=\textstyle\sum_{{\mathcal{U}}\in\beta X}y_{(X,{\mathcal{U}})}\hbox
to0.0pt{ .\hss}$

###  6.2. The pretopos case

Let us now write $\mathsf{Pretop}$ for the $2$-category of pretoposes,
pretopos morphisms and all natural transformations. Like before, every locally
connected Grothendieck topos is a pretopos and every inverse image functor is
a pretopos morphism, so that we have a forgetful $2$-functor
$\mathsf{LCGTop}^{\mathrm{op}}\rightarrow\mathsf{Pretop}$.

######  Definition 37.

A _locally connected classifying topos_ for a pretopos ${\mathcal{C}}$ is a
left biadjoint at ${\mathcal{C}}$ for the forgetful $2$-functor
$\mathsf{LCGTop}^{\mathrm{op}}\rightarrow\mathsf{Pretop}$.

It is known that every small pretopos ${\mathcal{C}}$ has a locally connected
classifying topos. To see this, we factor the forgetful $2$-functor of the
preceding definition as the composite of the two forgetful $2$-functors

$\mathsf{LCGTop}^{\mathrm{op}}\rightarrow\mathsf{GTop}^{\mathrm{op}}\rightarrow\mathsf{Pretop}$

viewing a locally connected Grothendieck topos as a Grothendieck topos, and a
Grothendieck topos as a pretopos. The second factor is well-known to have a
left biadjoint at every small pretopos ${\mathcal{C}}$, given by the topos of
sheaves $\mathrm{\mathcal{S}h}({\mathcal{C}})$ for the topology of finite
jointly epimorphic families. On the other hand, the first factor is known to
have a left biadjoint given by the _locally connected coclosure_ of [18]. It
follows that the composite has a left biadjoint at every small pretopos.

One difficulty with the preceding argument is that the construction of the
locally connected coclosure in [18] is inexplicit, relying at a crucial point
on the adjoint functor theorem. Our objective in this section is to give a
concrete description of the locally connected classifying topos of any small
_De Morgan_ pretopos. The notion of De Morgan pretopos is an obvious
generalisation of the notion of _De Morgan topos_ described, for example in
[26, §D4.6]. In giving the definition, we recall a _pseudocomplement_ of an
element $a$ in a distributive lattice is an element $\neg a$ which is disjoint
from $a$, and is moreover the maximal such element; i.e., such that $a\wedge
b=\bot$ if and only if $b\leqslant\neg a$.

######  Definition 38.

A distributive lattice $A$ is a _Stone algebra_ [22] if it admits all
pseudocomplements and satisfies $\neg a\vee\neg\neg a=\top$ for all $a\in A$.
A pretopos ${\mathcal{C}}$ is _De Morgan_ if each subobject lattice
$\mathrm{Sub}_{\mathcal{C}}(X)$ is a Stone algebra.

An equivalent characterisation of a De Morgan pretopos is as one in which each
inclusion of meet semi-lattices
$\mathrm{Sum}_{\mathcal{C}}(X)\rightarrow\mathrm{Sub}_{\mathcal{C}}(X)$ has a
left adjoint sending $A$ to $\neg\neg A$. The relevance of the condition to
our investigations is isolated in the following result, whose significance
will become clear shortly. In its proof, we use the operation
$\exists_{f}\colon\mathrm{Sub}_{\mathcal{C}}(X)\rightarrow\mathrm{Sub}_{\mathcal{C}}(Y)$
of _direct image_ along a map $f\colon X\rightarrow Y$ of a pretopos
${\mathcal{C}}$. This operation is left adjoint to pullback
$f^{-1}\colon\mathrm{Sub}_{\mathcal{C}}(Y)\rightarrow\mathrm{Sub}_{\mathcal{C}}(X)$
and satisfies the _Beck–Chevalley_ and _Frobenius_ conditions; see [25,
§A1.3].

######  Proposition 39.

If ${\mathcal{C}}$ is a De Morgan pretopos, then $\mathcal{UF}_{\mathcal{C}}$
satisfies the right Ore condition: that is, each cospan in
$\mathcal{UF}_{\mathcal{C}}$ as in the solid part of the following diagram can
be completed to a commuting square as shown:

(6.5)
$\textstyle{(Z,{\mathcal{W}})\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{[g_{2}]}$$\scriptstyle{[g_{1}]}$$\textstyle{(X_{2},{\mathcal{U}}_{2})\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{[f_{2}]}$$\textstyle{(X_{1},{\mathcal{U}}_{1})\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{[f_{1}]}$$\textstyle{(Y,{\mathcal{V}})\hbox
to0.0pt{ .\hss}}$

###### Proof.

Since every map in $\mathcal{UF}_{\mathcal{C}}$ factors as an isomorphism
followed by the equivalence class of a _total_ map, we lose no generality in
assuming that the $f_{i}$’s in (6.5) are total. We can therefore form their
pullback $g_{1}\colon X_{1}\leftarrow Z\rightarrow X_{2}\colon g_{2}$ in
${\mathcal{C}}$, and consider the subset
${\mathcal{F}}\subseteq\mathrm{Sum}_{\mathcal{C}}(Z)$ given as the upward
closure of

(6.6) $\\{g_{1}^{-1}(U_{1})\cap
g_{2}^{-1}(U_{2}):U_{1}\in{\mathcal{U}}_{1},U_{2}\in{\mathcal{U}}_{2}\\}\hbox
to0.0pt{ .\hss}$

This subset is easily a filter on $\mathrm{Sum}_{\mathcal{C}}(Z)$, and we
claim it is a _proper_ filter; thus, for any $U_{1}\in{\mathcal{U}}_{1}$ and
$U_{2}\in{\mathcal{U}}_{2}$ we must show that $g_{1}^{-1}(U_{1})\cap
g_{2}^{-1}(U_{2})\neq\bot$. Now, by Frobenius, Beck–Chevalley, and Frobenius
we have

$\displaystyle\exists_{f_{1}g_{1}}(g_{1}^{-1}(U_{1})\cap g_{2}^{-1}(U_{2}))$
$\displaystyle=\exists_{f_{1}}(U_{1}\cap\exists_{g_{1}}(g_{2}^{-1}(U_{2})))$
$\displaystyle=\exists_{f_{1}}(U_{1}\cap f_{1}^{-1}(\exists_{f_{2}}(U_{2})))$
$\displaystyle=\exists_{f_{1}}(U_{1})\cap\exists_{f_{2}}(U_{2})\hbox to0.0pt{
,\hss}$

and so, since direct image preserves and reflects $\bot$, we must equally show
that $\exists_{f_{1}}(U_{1})\cap\exists_{f_{2}}(U_{2})\neq\bot$. If we set
$V_{i}=\neg\neg\exists_{f_{i}}(U_{i})$ then, by standard properties of
pseudocomplementation, this is in turn equivalent to showing that $V_{1}\cap
V_{2}\neq\bot$. Since ${\mathcal{C}}$ is De Morgan, we have
$V_{i}\in\mathrm{Sum}_{\mathcal{C}}(Y)$; moreover, $U_{i}\in{\mathcal{U}}_{i}$
and $U_{i}\subseteq f_{i}^{-1}(\exists_{f_{i}}(U_{i}))\subseteq
f_{i}^{-1}(V_{i})$ implies $f_{i}^{-1}(V_{i})\in{\mathcal{U}}_{i}$, and so
$V_{i}\in{\mathcal{V}}$ since $(f_{i})_{!}({\mathcal{U}}_{i})={\mathcal{V}}$.
Since ${\mathcal{V}}$ is an ultrafilter, we conclude that $V_{1}\cap
V_{2}\neq\bot$ as desired.

This proves that (6.6) generates a _proper_ filter ${\mathcal{F}}$. By the
Boolean prime ideal theorem, we can extend this to an ultrafilter
${\mathcal{W}}\in\beta Z$, which by construction satisfies
${\mathcal{U}}_{i}\subseteq(g_{i})_{!}({\mathcal{W}})$ for $i=1,2$, and so
${\mathcal{U}}_{i}=(g_{i})_{!}({\mathcal{W}})$ (since both sides are
ultrafilters). We have thus completed (6.6) to a commuting square as desired.∎

The key to constructing the locally connected classifying topos of a small De
Morgan pretopos is the following standard result on geometric morphisms into
sheaf toposes proved, for example, in [36, Lemma VII.7.3]. In the statement,
we write $\mathsf{CovFlat}({\mathcal{A}},{\mathcal{E}})$ for the category of
flat functors ${\mathcal{A}}\rightarrow{\mathcal{E}}$ which are also _cover-
preserving_ , in the sense of sending covers to jointly epimorphic families.

######  Proposition 40.

Let ${\mathcal{A}}$ be a small site and
$i\colon\mathrm{\mathcal{S}h}({\mathcal{A}})\rightarrow[{\mathcal{A}}^{\mathrm{op}},\mathrm{\mathcal{S}et}]$
the associated inclusion of toposes. Under the equivalence (6.2), a geometric
morphism
${\mathcal{E}}\rightarrow[{\mathcal{A}}^{\mathrm{op}},\mathrm{\mathcal{S}et}]$
factors through $i$ just when the corresponding flat functor
${\mathcal{A}}\rightarrow{\mathcal{E}}$ is cover-preserving. Consequently,
(6.2) restricts back to an equivalence

(6.7)
$\mathsf{GTop}({\mathcal{E}},\mathrm{\mathcal{S}h}({\mathcal{A}}))\simeq\mathsf{CovFlat}({\mathcal{A}},{\mathcal{E}})\hbox
to0.0pt{ .\hss}$

The locally connected classifying topos of the small De Morgan pretopos
${\mathcal{C}}$ will be obtained as a topos of sheaves on
$\mathcal{UF}_{\mathcal{C}}$ for a suitable Grothendieck topology, and its
universal property verified via a chain of pseudonatural equivalences
$\mathsf{LCGTop}({\mathcal{E}},\mathrm{\mathcal{S}h}({\mathcal{UF}_{\mathcal{C}}}))\simeq\mathsf{CovFlat}(\mathcal{UF}_{\mathcal{C}},{\mathcal{E}})\simeq\mathsf{Pretop}({\mathcal{C}},{\mathcal{E}})$,
each of whose terms is a restriction of the corresponding term in (6.3).

Since a pretopos morphism out of ${\mathcal{C}}$ is a lextensive functor which
also preserves regular epimorphisms, the topology on
$\mathcal{UF}_{\mathcal{C}}$ must be chosen so that, under the equivalence
$\mathsf{Flat}(\mathcal{UF}_{\mathcal{C}},{\mathcal{E}})\simeq\mathsf{Lext}({\mathcal{C}},{\mathcal{E}})$
of (6.3), the cover-preserving functors to the left correspond to the regular-
epimorphism-preserving ones to the right.

We now describe such a topology, specifying it in terms of a _coverage_ [26,
Definition C2.1.1]; this involves assigning to each object $X$ a set of
covering families $(f_{i}\colon X_{i}\rightarrow X\mid i\in I)$ satisfying the
stability property:

  * (C)

For any cover $(f_{i}\colon X_{i}\rightarrow X\mid i\in I)$ and any map
$g\colon Y\rightarrow X$ in ${\mathcal{A}}$, there is a cover $(h_{j}\colon
Y_{j}\rightarrow Y\mid j\in J)$ such that each $gh_{j}$ factors through some
$f_{i}$.

######  Proposition 41.

Let ${\mathcal{C}}$ be a pretopos. There is a coverage on
$\mathcal{UF}_{\mathcal{C}}$ for which a typical cover of the object
$(Y,{\mathcal{V}})\in\mathcal{UF}_{\mathcal{C}}$ is of the form

(6.8)
${\langle{f,{\mathcal{V}}}\rangle}\mathrel{\mathop{:}}=\big{(}\,[f]\colon(X,{\mathcal{U}})\rightarrow(Y,{\mathcal{V}})\,\mid\,{\mathcal{U}}\in\beta
X,f_{!}({\mathcal{U}})={\mathcal{V}}\,\big{)}$

for any $f\colon X\rightarrow Y$ whose image
$\operatorname{im}f\rightarrowtail Y$ is (a coproduct injection and) in
${\mathcal{V}}$.

###### Proof.

We must verify condition (C). So consider ${\langle{f,{\mathcal{V}}}\rangle}$
as above and a map
$[g]\colon(Y^{\prime},{\mathcal{V}}^{\prime})\rightarrow(Y,{\mathcal{V}})$ in
$\mathcal{UF}_{\mathcal{C}}$ defined on some $m\colon
V^{\prime}\rightarrowtail Y^{\prime}$ in ${\mathcal{V}}^{\prime}$. We first
pull back $f$ along $g$ in ${\mathcal{C}}$ as in the left-hand square below,
and now define $f^{\prime}=mq\colon X^{\prime}\rightarrow Y^{\prime}$. By
assumption, $\operatorname{im}f\in{\mathcal{V}}$; since $g$ is continuous and
image factorisations are pullback-stable, it follows that
$\operatorname{im}f^{\prime}\in{\mathcal{V}}^{\prime}$. Moreover, for each
$[f^{\prime}]\colon(X^{\prime},{\mathcal{U}}^{\prime})\rightarrow(Y^{\prime},{\mathcal{V}}^{\prime})$
in ${\langle{f^{\prime},{\mathcal{V}}^{\prime}}\rangle}$, the composite
$[gf^{\prime}]$ factorises through a map in
${\langle{f,{\mathcal{V}}}\rangle}$ as to the right in:

$\textstyle{{X^{\prime}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{p}$$\scriptstyle{q}$$\textstyle{{X}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{f}$$\textstyle{{(X^{\prime},{\mathcal{U}}^{\prime})}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{[p]}$$\scriptstyle{[f^{\prime}]}$$\textstyle{{(X,p_{!}{\mathcal{U}}^{\prime})}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{[f]}$$\textstyle{{V^{\prime}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{g}$$\textstyle{{Y}}$$\textstyle{{(Y^{\prime},{\mathcal{V}}^{\prime})}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{[g]}$$\textstyle{{(Y,{\mathcal{V}})}\hbox
to0.0pt{ .\hss}}$

This proves that the covers do indeed satisfy condition (C). ∎

We write $\mathrm{\mathcal{S}h}(\mathcal{UF}_{\mathcal{C}})$ for the topos of
sheaves on $\mathcal{UF}_{\mathcal{C}}$ for this coverage.

######  Theorem 42.

Let ${\mathcal{C}}$ be a small De Morgan pretopos. The topos
$\mathrm{\mathcal{S}h}({\mathcal{UF}_{\mathcal{C}}})$ is a locally connected
classifying topos for ${\mathcal{C}}$, and is itself De Morgan.

###### Proof.

We begin by showing that $\mathrm{\mathcal{S}h}(\mathcal{UF}_{\mathcal{C}})$
is locally connected and De Morgan. Since ${\mathcal{C}}$ is De Morgan, we
know by Proposition 39 that $\mathcal{UF}_{\mathcal{C}}$ satisfies the right
Ore condition, and so by [26, Examples C3.3.11(a)] and [11, Corollary 2.8],
the sheaf topos $\mathrm{\mathcal{S}h}(\mathcal{UF}_{\mathcal{C}})$ will be
both locally connected and De Morgan so long as every covering family
${\langle{f,{\mathcal{V}}}\rangle}$ as in (6.8) is non-empty. Thus, given
${\mathcal{V}}\in\beta Y$ and $f\colon X\rightarrow Y$ in ${\mathcal{C}}$ with
$\operatorname{im}f\in{\mathcal{V}}$, we must show that there exists an
ultrafilter ${\mathcal{U}}\in\beta X$ with
$f_{!}({\mathcal{U}})={\mathcal{V}}$. Much as in Proposition 39, we consider
the subset ${\mathcal{F}}\subseteq\mathrm{Sum}_{\mathcal{C}}(X)$ given as the
upwards-closure of

(6.9) $\\{f^{-1}(V):V\in{\mathcal{V}}\\}\hbox to0.0pt{ .\hss}$

Like there, ${\mathcal{F}}$ is a filter which we claim is moreover _proper_.
Indeed, if $\bot=f^{-1}(V)$ for some $V\in\mathrm{Sum}_{\mathcal{C}}(Y)$, then
also $\bot=\exists_{f}(f^{-1}(V)\cap\top)=V\cap\operatorname{im}f$ by
Frobenius; whence $V\notin{\mathcal{V}}$ since
$\operatorname{im}f\in{\mathcal{V}}$. Like before, we can now use the Boolean
prime ideal theorem to find an ultrafilter
${\mathcal{U}}\subseteq\mathrm{Sum}_{\mathcal{C}}(X)$ extending
${\mathcal{F}}$ which, by construction, will satisfy ${\mathcal{V}}\subseteq
f_{!}({\mathcal{U}})$ and hence (since both are ultrafilters)
${\mathcal{V}}=f_{!}({\mathcal{U}})$.

So $\mathrm{\mathcal{S}h}(\mathcal{UF}_{\mathcal{C}})$ is locally connected
and De Morgan; it remains to verify the classifying property, for which we
must exhibit equivalences
$\mathsf{LCGTop}({\mathcal{E}},\mathrm{\mathcal{S}h}({\mathcal{UF}_{\mathcal{C}}}),\mathrm{\mathcal{S}et}])\simeq\mathsf{Pretop}({\mathcal{C}},{\mathcal{E}})$,
pseudonaturally in ${\mathcal{E}}$. As discussed above, these will be obtained
by composing pseudonatural equivalences:

(6.10)
$\mathsf{LCGTop}({\mathcal{E}},\mathrm{\mathcal{S}h}({\mathcal{UF}_{\mathcal{C}}}))\ext@arrow
01{20}0\rightarrowfill@{}{\simeq}\mathsf{CovFlat}(\mathcal{UF}_{\mathcal{C}},{\mathcal{E}})\ext@arrow
01{20}0\rightarrowfill@{}{\simeq}\mathsf{Pretop}({\mathcal{C}},{\mathcal{E}})$

of which the first is (6.7), and the second is obtained by restricting the
right-hand equivalence
$\mathsf{Flat}(\mathcal{UF}_{\mathcal{C}},{\mathcal{E}})\simeq\mathsf{Lext}({\mathcal{C}},{\mathcal{E}})$
of (6.3). The only point to check is that the cover-preserving functors to the
left of this latter equivalence correspond to the regular-epimorphism-
preserving ones to the right.

So suppose given a covering family ${\langle{f,{\mathcal{V}}}\rangle}$ as in
(6.8). We may form the image factorisation $f=me\colon
X\twoheadrightarrow\operatorname{im}f\rightarrowtail Y$, and since by
assumption $\operatorname{im}f\in{\mathcal{V}}$, we conclude that

${\langle{f,{\mathcal{V}}}\rangle}=\big{(}\,(X,{\mathcal{U}})\ext@arrow
01{20}0\rightarrowfill@{}{[e]}(\operatorname{im}f,\left.{{\mathcal{V}}}\right|_{\operatorname{im}f})\ext@arrow
01{20}0\rightarrowfill@{}{[m]}(Y,{\mathcal{V}})\,\big{)}_{{\mathcal{U}}\in\beta
X,e_{!}({\mathcal{U}})=\left.{{\mathcal{V}}}\right|_{\operatorname{im}f}}\hbox
to0.0pt{ .\hss}$

Since $[m]$ is invertible in $\mathcal{UF}_{\mathcal{C}}$, this family will be
sent to a jointly epimorphic one just when
${\langle{e,\left.{{\mathcal{V}}}\right|_{\operatorname{im}f}}\rangle}$ is;
whence a functor $A\colon\mathcal{UF}_{\mathcal{C}}\rightarrow{\mathcal{E}}$
preserves all covers just when it preserves ones
${\langle{f,{\mathcal{V}}}\rangle}$ as in (6.8) with $f$ a _regular
epimorphism_. This is equally to say that, for each $f\colon
X\twoheadrightarrow Y$ and each ${\mathcal{V}}\in\beta Y$, the map to the left
in:

$\sum_{\begin{subarray}{c}{\mathcal{U}}\in\beta X\\\
f_{!}({\mathcal{U}})={\mathcal{V}}\end{subarray}}A(X,{\mathcal{U}})\rightarrow
A(Y,{\mathcal{V}})\qquad\qquad\sum_{{\mathcal{U}}\in\beta
X}A(X,{\mathcal{U}})\rightarrow\sum_{{\mathcal{V}}\in\beta
X}A(Y,{\mathcal{V}})$

obtained by copairing the maps $A([f])\colon A(X,{\mathcal{U}})\rightarrow
A(Y,{\mathcal{V}})$ is an epimorphism in ${\mathcal{E}}$. Summing these left-
hand maps over all ${\mathcal{V}}\in\beta Y$ and using infinite extensivity of
${\mathcal{E}}$, this is equally the condition that, for each $f\colon
X\twoheadrightarrow Y$ in ${\mathcal{C}}$, the map right above is an
epimorphism. Since this map is the value at $f$ of the functor
$\int\\!A\colon{\mathcal{C}}\rightarrow{\mathcal{E}}$ corresponding to $A$
under (3.7), this completes the proof. ∎

######  Remark 43.

As before, chasing the identity geometric morphism
$\mathrm{\mathcal{S}h}(\mathcal{UF}_{\mathcal{C}})\rightarrow\mathrm{\mathcal{S}h}(\mathcal{UF}_{\mathcal{C}})$
through this proof shows that the universal pretopos map
${\eta\colon{\mathcal{C}}\rightarrow\mathrm{\mathcal{S}h}({\mathcal{UF}_{\mathcal{C}}})}$
is the image under (3.7) of the composite
$ay\colon\mathcal{UF}_{\mathcal{C}}\rightarrow\mathrm{\mathcal{S}h}({\mathcal{UF}_{\mathcal{C}}})$
of the Yoneda embedding and the sheafification functor. As such it is given
by:

$\eta(X)=\textstyle\sum_{{\mathcal{U}}\in\beta X}ay_{(X,{\mathcal{U}})}\hbox
to0.0pt{ .\hss}$

Now, each object $ay_{(X,{\mathcal{U}})}$ is _connected_ in
$\mathrm{\mathcal{S}h}(\mathcal{UF}_{\mathcal{C}})$, in the sense of having no
non-trivial coproduct decomposition; and so it follows that
$\mathrm{\mathcal{S}um}_{\mathcal{UF}_{\mathcal{C}}}(\eta
X)={\mathcal{P}}(\beta X)$ is the canonical extension of the Boolean algebra
$\mathrm{\mathcal{S}um}_{\mathcal{C}}(X)$. This justifies the link drawn in
the introduction to this section between locally connected classifying
toposes, and canonical extension for Boolean algebras.

######  Remark 44.

We remarked above that the $2$-functor
$\mathsf{GTop}^{\mathrm{op}}\rightarrow\mathsf{Pretop}$ has a left biadjoint
at every small pretopos given by the topos
$\mathrm{\mathcal{S}h}({\mathcal{C}})$ of sheaves on ${\mathcal{C}}$ for the
topology of finite jointly epimorphic families. The toposes arising in this
way are commonly known as _coherent_ toposes; moreover, by [11, Theorem 3.11],
the coherent topos associated to a small De Morgan pretopos is itself De
Morgan. Given this, another way of seeing Theorem 42 is as giving an explicit
construction of the _locally connected coclosure_ [18] of any coherent De
Morgan topos.

One may reasonably ask if we have a similar explicit construction upon
dropping the qualifier “coherent”. The answer is yes, so long as we assume
that every cardinal is smaller than some strongly compact cardinal. In this
case, for any De Morgan Grothendieck topos ${\mathcal{E}}$, we can find a
strongly compact cardinal $\kappa$ such that ${\mathcal{E}}$ is the free
completion of a small De Morgan _$\kappa$ -ary pretopos_—that is, a pretopos
with pullback-stable $\kappa$-small coproducts. We can thus reduce the problem
to constructing the locally connected classifying topos of a small
$\kappa$-ary De Morgan pretopos; and we can do this by tracing through the
definitions and results of this paper replacing everywhere finite coproducts
by $\kappa$-small coproducts. The main change, as in [9], is that we must
replace ultrafilters by _$\kappa$ -complete ultrafilters_—ones closed under
$\kappa$-small intersections. The assumption of strong compactness of $\kappa$
is needed in the proofs of Proposition 39 and Theorem 42, where we are now
required to extend the $\kappa$-complete filters (6.6) and (6.9) to
$\kappa$-complete ultrafilters.

###  6.3. Relation to toposes of types

In the introduction to this section, we have already discussed the analogies
between our construction of a locally connected classifying topos, and
Makkai’s topos of types from [38]. We now provide a more detailed technical
comparison between these constructions and other similar constructions in the
literature.

The earliest “topos of types” in fact predates Makkai, appearing in Joyal and
Reyes’ [29]. Given a pretopos ${\mathcal{C}}$, a _prime filter_ on
$X\in{\mathcal{C}}$ is a prime filter in the distributive lattice
$\mathrm{Sub}_{\mathcal{C}}(X)$; these comprise the objects of a category
${\mathcal{P}}{\mathcal{F}}_{\mathcal{C}}$ of prime filters in ${\mathcal{C}}$
defined similarly to $\mathcal{UF}_{\mathcal{C}}$. Endowing
${\mathcal{P}}{\mathcal{F}}_{\mathcal{C}}$ with the obvious analogy of the
topology of Proposition 41 yields [29]’s _topos of existential types_. No
universal property is described, but the formula (3.6) appears on p.11 of
_ibid_.

Makkai’s topos of types from [38] is a topos of sheaves on the same category
${\mathcal{P}}{\mathcal{F}}_{\mathcal{C}}$, but for a different topology, and
he exhibits it as the “classifying prime-generated topos for
$\mathfrak{p}$-models of ${\mathcal{C}}$”. As we have already said, a
Grothendieck topos ${\mathcal{E}}$ is prime-generated if each subobject
lattice is completely distributive algebraic, while a pretopos morphism
$F\colon{\mathcal{C}}\rightarrow{\mathcal{E}}$ into a prime-generated topos is
said to be a _$\mathfrak{p}$ -model_ if for every prime filter $\mathfrak{p}$
on $\mathrm{\mathcal{S}ub}_{\mathcal{C}}(X)$ and every $f\colon X\rightarrow
Y$ we have
$\exists_{f}(\bigcap_{A\in\mathfrak{p}}FA)=\bigcap_{A\in\mathfrak{p}}F(\exists_{f}A)$
in $\mathrm{Sub}_{\mathcal{E}}(FY)$. The classifying property of the topos of
types $\tau({\mathcal{C}})$ is given by equivalences

(6.11)
$\mathsf{PGTop}({\mathcal{E}},\tau({\mathcal{C}}))\simeq\mathsf{pPretop}({\mathcal{C}},{\mathcal{E}})$

where to the left we have the category of geometric morphisms between prime-
generated toposes whose inverse image functors preserve all intersections, and
to the right we have the category of $\mathfrak{p}$-models. In establishing
this equivalence, the formula (3.6) again appears; see the bottom of p.164 of
_ibid_. In model-theoretic terms, the condition of being a
$\mathfrak{p}$-model is a _saturation_ condition; Makkai states this already
in [38], and the point is followed up in [10], and exploited in, among other
places, [43, 15].

The other main “topos of types” in the literature is Pitts’ _topos of filters_
$\Phi({\mathcal{C}})$ of a pretopos ${\mathcal{C}}$. Introduced in [44], this
is the topos of sheaves on the category ${\mathcal{F}}_{\mathcal{C}}$ of _all_