For $C$ a small category, it is well-known (and fundamental) that the presheaf category $Set^{C^{op}}$ is the free cocompletion of $C$ with respect to small colimits. Analogously, if $V$ is a complete and cocomplete symmetric monoidal closed category and $C$ is a small $V$-enriched category, the enriched presheaf category $V^{C^{op}}$ is the free (co)completion of $C$ with respect to $V$-colimits.
If $C$ is merely locally small (or merely takes homs in $V$ as above), the presheaf category may be too large to be a free small-colimit cocompletion. Nevertheless, the small-colimit cocompletion of $C$ exists, as the full subcategory of $Set^{C^{op}}$ consisting of functors $C^{op} \to Set$ that are small colimits of representables.
However, this cocompletion (which we denote by $Colim(C)$) typically does not have the properties one associates with presheaf toposes; for example, $Colim(C)$ might not even be complete, or might not even have a terminal object. But $Colim(C)$ may inherit some good properties from $C$ if $C$ has them. While it is rare for $Colim(C)$ to be a Grothendieck topos even if $C$ is, it is at least true in this case that $Colim(C)$ is a locally cartesian closed pretopos, thus satisfying many of the topos-like properties one needs to internalize large chunks of mathematics.
In these notes, we wish to prove that if $C$ is a complete and cocomplete locally cartesian closed pretopos (or a cocomplete $\Pi$-pretopos; see below), then so is $Colim(C)$. The expectation is that this result can be strengthened to incorporate $W$-types (i.e., $\Pi$-pretoposes which admit initial algebras for polynomial functors). Eventually, we hope to study the initial algebra or final coalgebra for the $Colim$ construction itself, which again should have all these properties.
As a stepping stone, consider the cocompletion of a category $C$ with respect to small coproducts (denoted $\Sigma C$). This may be constructed explicitly by a comma category construction: objects of $\Sigma C$ are pairs $(X, f: X_d \to C)$ where $X$ is a set and $f$ is a functor from the discrete category $X_d$ on $X$ to $C$. Morphisms $(X, f) \to (Y, g)$ are pairs $(h, \Phi)$ where $h: X \to Y$ is a function and $\Phi: f \to g \circ h_d$ is a natural transformation. The idea is that a pair $(X, f)$ is a formal coproduct
of objects of $C$.
If $E$ is a Grothendieck topos, and $\Delta: Set \to E$ is the essentially unique left exact left adjoint, a functor $X_d \to E$ may be identified with an object in the slice $E/\Delta(X)$, and the comma category construction for $\Sigma E$ may be written as
This is an example of Artin-Wraith gluing, and $E \downarrow \Delta$ is again a Grothendieck topos.
As a special case, when $E$ is a presheaf topos $Set^{D^{op}}$, we have
where $D_+$ is obtained by formally adjoining a (new) initial object to $D$.
Rather more generally, if $C$ is an $\infty$-lextensive category, then we have an essentially unique left exact coproduct-preserving functor
which takes a set $X$ to a coproduct of an $X$-indexed collection of copies of the terminal object $1$ of $C$, and the infinite extensivity means that we again have an equivalence
This applies in particular to the case where $C$ is a $\Pi$-pretopos. In the next section, we will prove a general result that has the following corollary: if $C$ is a complete and cocomplete $\Pi$-pretopos, then so is $\Sigma(C)$.
Analogously to the case for toposes, we will show that if $G$ is a left exact (or even just a pullback-preserving) comonad on a cocomplete $\Pi$-pretopos, then the category of $G$-coalgebras is also a cocomplete $\Pi$-pretopos.
A cocomplete locally cartesian closed extensive category is $\infty$-extensive.
This is essentially obvious: infinite coproducts are still disjoint, and stable under pullbacks by local cartesian closure.
A cocomplete locally cartesian closed extensive category $C$ is complete.
The condition of local cartesian closure includes the existence of finite limits, so it suffices to see that $C$ has arbitrary products. Let $B_i$ be a collection of objects of $C$ indexed over a set $I$. By cocompleteness, we have a map in $C$:
where $\Delta I = \sum_{i \in I} 1$, sending the summand $B_i$ to $i$ (the $i^{th}$ copy of $1$). Then
is the product, where $!$ is the unique map $\Delta I \to 1$. Indeed, maps $X \to \Pi_! p$ are in natural bijection with maps $!^\ast X \to p$ in $E/\Delta(I) \simeq E^I$ (this equivalence holds by infinite extensivity), i.e., with an $I$-indexed family of maps $X \to B_i$, as required.
In particular, cocomplete $\Pi$-pretoposes are also complete.
Let $G$ be a pullback-preserving comonad on a cocomplete $\Pi$-pretopos $E$. Then the category of $G$-coalgebras $Coalg_G$ is also a cocomplete $\Pi$-pretopos.
The underlying functor $U: Coalg_G \to E$ preserves and reflects colimits, so it is clear that $Coalg_G$ is cocomplete. It has a terminal object $G 1$ and has pullbacks since $G$ preserves pullbacks, so $Coalg_G$ is finitely complete. To show $Coalg_G$ is locally cartesian closed, we must check that for each $G$-coalgebra $Z$ the slice $Coalg_G/Z$ is cartesian closed. Now the forgetful functor $U_Z: Coalg_G/Z \to E/Z$ is left exact: it clearly preserves the terminal object $1_Z: Z \to Z$, and preserves pullbacks because $U: Coalg_G \to E$ does. It is also comonadic with respect to a comonad $G_Z$ whose functor part takes an object $f: X \to Z$ of $E/Z$ to the pullback of the diagram
as may be checked directly (or using a crude monadicity theorem). Then we use the familiar fact that if $C$ is cartesian closed and $H: C \to C$ is a lex comonad, then $Coalg_H$ is also cartesian closed; apply this to $H = G_Z: E/Z \to E/Z$ to conclude $Coalg_G/Z$ is cartesian closed.
It remains to see that $Coalg_G$ is a pretopos.
In brief, $Coalg_G$ is a pretopos because the pretopos axioms are expressed in terms of pullbacks and colimits. If $G: E \to E$ is preserves pullbacks, then the underlying functor $U: Coalg_G \to E$ preserves and reflects colimits and pullbacks, and this means that the pretopos axioms hold on $Coalg_G$ if they hold on $E$.
For example, $U$ preserves and reflects monos. Thus, a pushout diagram in $Coalg_G$ of the form
is also a pullback in which all arrows are monic, since this is true as a diagram in $E$ by extensivity. Also such coproducts are stable under pullback (say by local cartesian closure). Therefore $Coalg_G$ is extensive.
It is also regular: given $f: X \to Y$ in $Coalg_G$, the coequalizer of the kernel pair of $f$ can be computed at the level of $E$ (again by the preservation and reflection properties of $U$), and this gives the regular epi-mono factorization in $Coalg_G$. Of course, regular epis in $Coalg_G$, being coequalizers, are stable under pullback by local cartesian closure. Hence $Coalg_G$ is regular. And congruences in $Coalg_G$ are kernel pairs, again by the same reasoning about preservation and reflection of finite limits and colimits. Hence $Coalg_G$ is (Barr-)exact. This completes the proof.
Let $C$ be a cocomplete $\Pi$-pretopos, and let $\Delta: Set \to C$ be the (essentially unique) left exact left adjoint. Then
is a cocomplete $\Pi$-pretopos.
Let $G: C \times Set \to C \times Set$ be the functor defined by $G(c, X) = (c \times \Delta X, X)$. Then $G$ is left exact and carries an obvious comonad structure. The category of $G$-coalgebras is $C \downarrow \Delta$, and this is a cocomplete $\Pi$-pretopos by the theorem.
For a finitely complete category $C$, let $C_{ex}$ denote its exact or ex/lex completion.
(Carboni) If $C$ is a small lex category, then $(\Sigma C)_{ex} \simeq Set^{C^{op}}$.
The category $\Sigma C$ is $\infty$-lextensive if $C$ is lex, and the exact completion of an $\infty$-lextensive category is cocomplete, exact, and $\infty$-lextensive. The projective objects in $(\Sigma C)_{ex}$ are the objects in $\Sigma C$, and the connected projective objects in $(\Sigma C)_{ex}$ are the objects of $C$. Thus all the Giraud conditions are satisfied, making $(\Sigma C)_{ex}$ a Grothendieck topos with a generating set of objects given by objects of $C$, and since these generators are connected and projective, this topos is actually a presheaf topos $Set^{C^{op}}$.
(Rosický) If $C$ is finitely complete, then $Colim(C) \simeq (\Sigma C)_{ex}$.
$C$ is a (large) union of small lex categories $C_i$, and we have a series of equivalences
where the colimit given by the second expression is over the system of exact functors $(\Sigma C_i)_{ex} \to (\Sigma C_j)_{ex}$ that are identified with left Kan extensions along inclusions $C_i \to C_j$.
(Possible mention of work by Pitts et al. on reflexive coqualizer completions, etc.)
If $E$ is a cocomplete $\Pi$-pretopos, then so is $E_{ex}$.
First, if $E$ is cocomplete, so is $E_{ex}$ (reference needed). It is known that $E_{ex}$ is locally cartesian closed if $E$ has weak dependent products (and hence if $E$ has dependent products, i.e., if $E$ is locally cartesian closed), and that $E_{ex}$ is a pretopos if $E$ is extensive. This is all we need.
If $E$ is a cocomplete $\Pi$-pretopos, then so is the free small-colimit cocompletion $Colim(E)$.
Now we reprise some of the above development, but this time adding in $W$-types.
Suppose given a cocomplete $\Pi$-pretopos $E$, and let $f: Y \to X$ be a morphism in $E$. The polynomial endofunctor $P_f: E \to E$ is defined to be the composite
which, informally, takes an object $X$ to the “polynomial” $\sum_{a: A} X^{f^{-1}(a)}$.
The $W$-type $W(f)$, if it exists, is the initial $P_f$-algebra. A $\Pi W$-pretopos is a $\Pi$-pretopos $E$ which admits a $W$-type $W(f)$ for every morphism $f$ of $E$.
More generally, one speaks of inductive types. One thing we can point out immediately is that the construction of the corresponding coinductive types, i.e., terminal $P_f$-coalgebras, is completely unproblematic.
Terminal $P_f$-coalgebras exist for any $f: Y \to X$ in any $\Pi$-pretopos.
Since cocomplete $\Pi$-pretoposes $E$ are complete, the limit of the following diagram exists in $E$:
Moreover, $P_f$ preserves this limit because (a) this is a connected limit, and (b) the functors $Y^\ast$, $\Pi_f$, and $\Sigma_X$ all preserve connected limits. Then the result follows from Adámek’s theorem, which asserts that this limit $L$, with coalgebra structure $L \to P_f L$ the isomorphism that obtains by the limit preservation by $P_f$, is the terminal coalgebra.
Below, we hope to exploit this to give a relatively painless proof of the following theorem, by situating initial algebras inside terminal coalgebras. The proof we give now is somewhat technical; it is adapted from a result in a paper of Moerdijk and Palmgren, who cite Alex Simpson as the originator of the proof they give the slice topos case.
If $E$ is a $\Pi W$-pretopos and $G: E \to E$ is a pullback-preserving comonad on $E$, then $Coalg_G$ is also a $\Pi W$-pretopos.
If $E$ is a $\Pi$-pretopos and
is a pullback diagram in $E$, then there is an isomorphism
of Beck-Chevalley type.
(This “proof” isn’t correct, but I’m letting it sit as is while I ponder…) Let $f: B \to A$ be a map between $G$-coalgebras, and let $W(f)$ denote the $W$-type of $f$ seen as a morphism of $E$. We will denote the to-be-constructed $W$-type of $f$, regarded as a morphism of $Coalg_G$, by $W_G(f)$.
We construct $W_G(f)$ as an equalizer
To define $\alpha$, first observe that there is a natural transformation $P_f \to P_{G f}$, obtained by pasting together a 2-cell diagram
where the $\eta$‘s refer to the given coalgebra structures, the middle 2-cell is a Beck-Chevalley isomorphism, and the transformation $\Sigma_A \eta_A^\ast \to \Sigma_{G A}$ is mated to the canonical isomorphism $\Sigma_A \to \Sigma_{G A} \Sigma_{\eta_A}$. Then, we have a composite
where the isomorphism obtains by initiality of $W(G f)$. Thus $W(G f)$ carries a $P_f$-algebra structure, whence there is a unique $P_f$-algebra map
To define $\beta$, let $S = Struct_G(A) \hookrightarrow G A^A$ be the object of possible structures on $A$ as a coalgebra over the comonad $G$ (this is easily defined in a $\Pi$-pretopos $E$). There is of course a point $[\eta_A]: 1 \to Struct_G(A)$ where $\eta_A$ is the given coalgebra structure on $A$. We begin by exhibiting a canonical $P_f$-algebra structure on the exponential $W(G f)^S$, which is tantamount to giving a map
It is probably simplest to describe this map in the internal language of $\Pi$-pretoposes (or in dependent type theory); it is the mapping
Here $\varepsilon: G \to 1_E$ is the counit of the comonad, and the definition makes sense because the judgment $\varepsilon_B u: f^{-1}(a)$ is valid, given the judgment $(G f)(u) = \eta(a): G A$. Indeed, we have
where the last equation holds since $\varepsilon_A \circ \eta$ for any $G$-coalgebra structure $\eta$.
(It is straightforward – although somewhat tedious – to write out the definition in purely categorical language.)
Since we have a $P_f$-algebra structure on $W(G f)^S$, we obtain a unique $P_f$-algebra map $W(f) \to W(G f)^S$, and the map $\beta$ is the composite
(To be continued.)
A. Carboni and P. Johnstone, Connected limits, familial representability and Artin glueing, Math. Structures in Comp. Sci. 5 no. 4 (December 1995), 441-459. (web)
J. Rosický, Cartesian closed exact completions, JPAA 142 no. 3 (October 1999), 261-270. (web)
A. Carboni and E.M. Vitale, Regular and exact completions, JPAA 125 no. 1 (March 1998), 79-116. (web)
A. Carboni, Some free constructions in realizability and proof theory, JPAA 105 no. 2 (September 1993), 117-148. (web)
B. van den Berg, Inductive types and exact completion, Ann. Pure Appl. Logic, 134 (2005), 95–121. (online .pdf file)
I. Moerdijk and E. Palmgren, Well-founded trees in categories, Ann. Pure Appl. Logic 104 (2000), 189-218. (online .pdf file)