Polynomial functors IV
Polynomial functors never cease to surprise. They always have all the nice properties.

Definition: A functor F(t) is pre-monadic if there exists a natural transformation F(F(t)) ~> F(t). A functor F(t) is pre-comonadic if there exists a natural transformation F(t) ~> F(F(t)). A functor F(t) is monadic if it is pointed and pre-monadic. A functor F(t) is co-monadic if it is co-pointed and pre-comonadic.

Recall that polynomial functors are pointed if t ~> F(t) exists. This is so iff F(t) contains at least one "monic monomial" in its distributive normal form. For example, F(t) = ... + t*t*t + ... is pointed because it contains a monic monomial t*t*t. A polynomial functor is co-pointed iff it is of the form F(t) = t*G(t) for some other polynomial functor G(t).

Obviously, not all polynomial functors are pointed or co-pointed. It is surprising that all of them are pre-monadic and pre-comonadic!

Lemma 1. For any functor F(t) in a Cartesian closed category, there exists a natural transformation F(t)*s ~> F(s), where both sides are understood as functors C*C -> C.
Proof: We have a morphism t*s->s (which ignores the factor "t"). Rewrite this as s -> (t->s) and lift the "t->s" into the functor F, to obtain a morphism s -> (F(t)->F(s)). Now, rewrite this as s*F(t) -> F(s).
Q.E.D.

There is an alternative formulation of Lemma 1, which would be also sufficient for our purposes, and which avoids the rewriting of morphisms as functions returning functions, which requires the assumption of Cartesian closed category.

Lemma 1'. For any polynomial functor F(t), there exists a natural transformation F(t)*s ~> F(s).
Proof: The distributive normal form of F(t) is F(t) = c₀ + c₁*t + c₂*t*t + ..., so we are required to construct a natural transformation

c₀*s + c₁*t*s + c₂*t*t*s + ... ~> c₀ + c₁*s + c₂*s*s + ...

We can construct this transformation simply by mapping each term on the left to the corresponding term on the right. This is so because we have natural transformations of the form
c₀*s ~> c₀ by ignoring the factor "s" and
c_n*t*t*...*t*s ~> c_n*s*s*...*s by ignoring the factors "t" and replicating the factor "s" as needed.

Q.E.D.

Lemma 2. For any polynomial functor F(t), there exists a natural transformation F(c) -> F(t)+c.

Proof. The distributive normal form of F allows us to write F(c) = b + c*G(c), where G is some functor and b is some constant type (independent of c). So, now we need to construct a natural transformation of the form b + c*G(c) ~> b + t*G(t) + c. We need to consider the terms "b" and "c*G(c)" separately. The term "b" is obviously mapped to "b". The functor c*G can be mapped to "c" by ignoring the factor "G".
Q.E.D.

Statement: For any polynomial functor F(t), there exist natural transformations F(F(t)) ~> F(t) and F(t) ~> F(F(t)).

Proof: By induction on the Horner-like form F(t) = c₀ + t*(c₁ + t*(...+t*c_n)...).

The base of induction is to show that the constant functor F(t)=c admits the required natural transformations: they can be taken as identical transformations.
The step of induction is to show that if F(t) admits the monadic transformation F(F(t))~>F(t) then both F(t)*t and F(t)+c also admit a monadic transformation; and similarly for the co-monadic transformation.

A calculation shows that there exists natural transformations in both directions between the following pairs of functors:

F(F(t)+c)+c and F(t)+c,
F(F(t)*t)*t and F(t)*t.

For example: To show that F(F(t)+c)+c ~> F(t)+c assuming that F(F(t))~>F(t).
We know that functor F is distributive (since it is polynomial; additionally, any pre-monadic functor is distributive in a CCC category). Therefore, we can transform F(F(t)+c)+c ~> F(F(t))+F(c)+c ~> F(t)+F(c)+c. By Lemma 2, we can further transform this to F(t)+(F(t)+c)+c. This can certainly be transformed into F(t)+c.

To show that F(t)+c ~> F(F(t)+c)+c assuming that F(t) ~> F(F(t)) is easier: it does not require Lemma 2. We just transform F(t)+c ~> F(F(t))+F(c)+c (by never generating the term F(c)). We know that we can transform F(x)+F(c)~>F(x+c) by functoriality of F. This gives us F(F(t)+c)+c as required.

Similarly, we can use Lemma 1 to prove that F(F(t)*t)*t ~> F(t)*t when F(F(t))~>F(t), etc.

Q.E.D.