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

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.

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

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.

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.

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

Proof

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

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.

Proof

Combine Corollary 1, Lemma 4, and Theorem 2.

Proof

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.

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

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