What sort of W-types follow from existence of an NNO?

Question

A W-type is an initial algebra for a polynomial endofunctor $P$ on a category $C$. A well-known example is that of a natural numbers object (NNO). Usually it is assumed that $C$ is locally cartesian closed (lcc), but this only ensures that all polynomial endofunctors exist so as to ask whether the corresponding W-type exists, and it also simplifies the definition of W-type (one needs to use parameters if not in the lcc case, see for example the definition of an NNO in a merely finite-product category). One can always, in a lextensive category, talk about finitary polynomial endofunctors: these are 'really' polynomials, namely endofunctors of the form $$ X \mapsto \coprod_{i \leq n} A_i \times X^{\times i}, $$ for some collection of objects $\lbrace A_i\rbrace_{i \leq n}$, or, if countably extensive, with a coproduct over $\mathbb{N}$ (the external natural numbers), and this is the case in the example I'm particularly interested in (and I know it is not lcc, just a cocomplete pretopos with NNO, in the appropriate sense).

My question is this:

If I have an infinitary lextensive category (so all coproducts, compatible with pullbacks) that is locally cartesian closed, with an NNO, what W-types do I get for free? What if the category is not lcc?

The first question at least puts an upper bound on what I can expect, the second one is closer to what I expect to see.

Answer 1

If CC is infinitary lextensive and in addition locally small, then the global sections functor $\Gamma$ : CC --> Set has a lex left adjoint $\Delta$ : Set --> CC, and CC automatically has a natural numbers object since NNOs are preserved by inverse image functors. Moreover, the reason that this is the case can be formulated in a way that also works for initial algebras of more general polynomial functors.

If I haven't made a mistake, it should work at least for polynomial functors of the form $G(X)=\sum_n \Delta(A_n)\times X^n$, i.e. polynomial functors whose coefficients are in the image of $\Delta$. With each such polynomial functor on CC there comes an obvious polynomial functor $F(S)=\sum_n A_n\times S^n$ on Set, and if $T$ is an initial algebra for $F$, then I think that $\Delta T$ is an initial algebra for $G$.

The proof goes roughly as follows: Since $\Delta$ commutes with finite products and all coproducts we have $\Delta\circ F = G\circ \Delta$, whence applying $\Delta$ to the algebra structure $t: FT\to T$ on $T$ gives a $G$-algebra structure on $\Delta T$. Now given another $G$-algebra $x:GX\to X$ all we have to do is to find an $F$-algebra structure on $\Gamma X$ such that a morphism $f:\Delta T\to X$ is a $G$-algebra morphism iff its adjoint transpose is a $F$-algebra morphism. Initiality of $\Delta T$ among $G$-algebras then follows from initiality of $T$ among $F$-algebras.

The components of the algebra structure on $\Gamma X$ are given by $$ A_n\times (\Gamma X)^n\to\Gamma\Delta A_n\times (\Gamma X)^n\cong\Gamma(\Delta(A_n)\times X^n)\xrightarrow{\Gamma(x_n)}\Gamma X, $$ where $x_n:\Delta A_n\times X^n\to X$ is a component of $x:GX\to X$.

I also think that it is possible to construct free monoids in CC by the "tensor algebra formula" $A^*=\sum_n A^n$. However, this is not an instance of the previous construction since $A^*$ is the initial algebra for $H(X) = 1 + A\times X$ where $A$ appears as a coefficient and is not assumed in the image of $\Delta$. I wonder if there is a more general construction that comprises both as instances? Or did I get something totally wrong?

Anyway, all this supposes that CC is locally small, I don't know if this is the case in what you have in mind.