# Contents

## Introduction

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.

## Free coproduct cocompletions

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

$\sum_{x : X} f(x)$

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

$\Sigma E = E \downarrow \Delta.$

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

$E \downarrow \Delta \simeq Set^{D_{+}^{op}}$

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

$\Delta: Set \to C$

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

$\Sigma(C) \simeq C \downarrow \Delta.$

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)$.

## Pullback-preserving comonads on $\Pi$-pretoposes

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.

###### Lemma

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.

###### Lemma

A cocomplete locally cartesian closed extensive category $C$ is complete.

###### Proof

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$:

$p: \sum_{i \in I} B_i \to \Delta I,$

where $\Delta I = \sum_{i \in I} 1$, sending the summand $B_i$ to $i$ (the $i^{th}$ copy of $1$). Then

$\prod_{i \in I} B_i = \Pi_! p$

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.

###### Theorem

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.

###### Proof

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

$\array{ & & Z \\ & & \downarrow \mathrlap{\eta_Z} \\ G X & \underset{G f}{\to} & G Z, }$

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

$\array{ 0 & \to & X \\ \downarrow & & \downarrow \\ Y & \to & X + Y }$

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.

###### Corollary

Let $C$ be a cocomplete $\Pi$-pretopos, and let $\Delta: Set \to C$ be the (essentially unique) left exact left adjoint. Then

$\Sigma(C) = C \downarrow \Delta$

is a cocomplete $\Pi$-pretopos.

###### Proof

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.

## Quotients and exact completions

For a finitely complete category $C$, let $C_{ex}$ denote its exact or ex/lex completion.

###### Lemma

(Carboni) If $C$ is a small lex category, then $(\Sigma C)_{ex} \simeq Set^{C^{op}}$.

###### Proof

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}}$.

###### Lemma

(Rosický) If $C$ is finitely complete, then $Colim(C) \simeq (\Sigma C)_{ex}$.

###### Proof

$C$ is a (large) union of small lex categories $C_i$, and we have a series of equivalences

$(\Sigma C)_{ex} \simeq \bigcup_i (\Sigma C_i)_{ex} \simeq \bigcup_i Set^{C_i^{op}} = Colim(C)$

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.)

###### Theorem

If $E$ is a cocomplete $\Pi$-pretopos, then so is $E_{ex}$.

###### Proof

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.

###### Corollary

If $E$ is a cocomplete $\Pi$-pretopos, then so is the free small-colimit cocompletion $Colim(E)$.

###### Proof

Combine Corollary 1, Lemma 4, and Theorem 2.

## Inductive types

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

$E \stackrel{Y^\ast}{\to} E/Y \stackrel{\Pi_f}{\to} E/X \stackrel{\Sigma_X}{\to} E$

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.

###### Proposition

Terminal $P_f$-coalgebras exist for any $f: Y \to X$ in any $\Pi$-pretopos.

###### Proof

Since cocomplete $\Pi$-pretoposes $E$ are complete, the limit of the following diagram exists in $E$:

$\ldots \to (P_f)^{n+1}(1) \stackrel{(P_f)^n !}{\to} (P_f)^n(1) \to \ldots \to P_f (1) \stackrel{!}{\to} 1.$

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.

###### Theorem

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.

###### Lemma

If $E$ is a $\Pi$-pretopos and

$\array{ P & \stackrel{k}{\to} & B \\ ^\mathllap{h} \downarrow & & \downarrow^\mathrlap{g} \\ A & \underset{f}{\to} & C }$

is a pullback diagram in $E$, then there is an isomorphism

$\array{ E/A & \stackrel{\Pi_f}{\to} & E/C \\ ^\mathllap{h^\ast} \downarrow & \cong & \downarrow^\mathrlap{g^\ast} \\ E/P & \underset{\Pi_k}{\to} & E/B }$

of Beck-Chevalley type.

###### Proof of Theorem

(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

$W_G(f) \stackrel{j}{\to} W(f) \stackrel{\overset{\alpha}{\to}}{\underset{\beta}{\to}} W(G f).$

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

$\array{ & & E/G B & \stackrel{\Pi_{G f}}{\to} & E/G A & \stackrel{\Sigma_{G A}}{\to} & E \\ & ^\mathllap{G B^\ast} \nearrow \cong & ^\mathllap{\eta_B^\ast} \downarrow & \cong & ^\mathllap{\eta_A^\ast} \downarrow & ^\Uparrow \nearrow^\mathrlap{\Sigma_A} & \\ E & \underset{B^\ast}{\to} & E/B & \underset{\Pi_f}{\to} & E/A & & }$

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

$P_f(W(G f)) \to P_{G f}(W(G f)) \cong W(G f)$

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

$\alpha: W(f) \to W(G f).$

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

$P_f(W(G f)^S) \times S \to P_{G f}(W(G f)) (\cong W(G f)).$

It is probably simplest to describe this map in the internal language of $\Pi$-pretoposes (or in dependent type theory); it is the mapping

$(a: A, S \times f^{-1}(a) \stackrel{t}{\to} X; \eta: S) \mapsto (\eta(a), \lambda u: (G f)^{-1}(\eta(a)). t(\eta, \varepsilon_B(u)): (G f)^{-1}(\eta(a)) \to X).$

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

$f(\varepsilon_B(u)) = (f \circ \varepsilon_B)(u) = (\varepsilon_A \circ G f)(u) = \varepsilon_A((G f)(u)) = \varepsilon_A (\eta (a)) = a$

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

$W(f) \to W(G f)^S \stackrel{eval_{\eta_A}}{\to} W(G f).$

(To be continued.)

## References

• 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)

Revised on October 9, 2016 at 14:19:10 by Todd Trimble