Polynomial functors III
What I call "distributive functors" are called "applicative" in the modern functional programming literature.

Despite what I thought previously:

Statement. All polynomial functors are distributive.
Proof.A polynomial functor can be rewritten (up to isomorphism) using a Horner-like formula,

F(t) = c⁰ + t*(c¹ + t*(c² + t*(... + t*cⁿ) ...)

Here the "coefficients" cⁱ are fixed types (independent of "t"): they could be 0, 1, or some nontrivial types.

Now, we will show by induction that F(t) is distributive, that is, there exists a natural transformation F(a)*F(b) ~> F(a*b) of functors C*C->C.

For the base of induction, we need to show that the constant functor F(t)=c (mapping everything to "c") is distributive. This is easy: F(a)*F(b) = c*c, F(a*b) = c. We need a natural transformation c*c ~> c. To produce such a natural transformation, we just ignore one of the factors of "c" (say, the second one).

For the step of induction, we need to show that, for a distributive functor F, the functor c+t*F is distributive. We first show that t*F is distributive:

a*F(a)*b*F(b) ~> a*b*F(a*b) can be constructed since we have already F(a)*F(b) ~> F(a*b).

Now we show that, for a distributive F, the functor c+F is also distributive.
We need to find a natural transformation (c+F(a))*(c+F(b)) ~> c+F(a*b).
The functor on the left is isomorphic to

c*c + c*F(b) + F(a)*c + F(a)*F(b).
To construct a natural transformation from this to c+F(a*b), we need to provide a natural transformation into either "c" or "F(a*b)", for each of the four terms separately.

For any functor G, we have a natural transformation c*G ~> c by simply ignoring the factor G.
So, we can provide natural transformations c*c ~> c, c*F(b) ~> c, and F(a)*c ~> c.
The last term, F(a)*F(b), has a natural transformation to F(a*b) by virtue of F being distributive. So, we can provide the required natural transformation, and c+F is distributive.

Q.E.D.

The dual property is that any polynomial functor F(t) is co-distributive: F(a+b) ~> F(a) + F(b). This can be proved in a different way.

Lemma: If a functor F(t) is co-distributive and either pointed or co-pointed, the functor t*F(t) is also co-distributive.
Proof: We need to construct a natural transformation (a+b)*F(a+b) ~> a*F(a) + b*F(b). First, we use the co-distributivity of F to construct a natural transformation (a+b)*F(a+b) ~> (a+b)*(F(a)+F(b)) = a*F(a) + a*F(b) + b*F(a) + b*F(b). For each of these four terms, we now need to construct a natural transformation to a*F(a) + b*F(b). This is easy for the first and the fourth terms.

For the second term, we need a*F(b) ~> a*F(a) + b*F(b). Consider two cases: either F is pointed, or F is co-pointed.

If F is pointed, we have a natural transformation a ~> F(a). Therefore, we can construct a natural transformation a ~> a*F(a) as well (just repeat the factor "a"). So we also have a*F(b) ~> a*F(a) by ignoring the factor F(b).

If F is co-pointed, we have a natural transformation F(b)~>b. Therefore, we can construct a natural transformation F(b) ~> b*F(b) by just repeating the factor F(b). So we also have a*F(b) ~> b*F(b) by ignoring the factor "a".

In both cases, we can construct the required natural transformation a*F(b) ~> a*F(a) + b*F(b).

Similarly, we show that we can construct the natural transformation b*F(a) ~> a*F(a) + b*F(b).

Q.E.D.

Statement: Any polynomial functor F(t) is co-distributive.
Proof: Any polynomial functor is a sum of "monomial" functors of the form c*t*t*...*t, for some constant type c. A sum of two co-distributive functors is again co-distributive. So it will be sufficient to prove that a monomial functor of the form c*t*t*...*t is co-distributive.

If a functor F is co-distributive, then so is c*F, where c is a constant type. This is so because the natural transformation F(a+b) ~> F(a)+F(b) leads directly to the natural transformation c*F(a+b) ~> c*(F(a)+F(b)) = c*F(a) + c*F(b).

So now it remains to show that "monic monomial" functors of the form t*t*...*t are co-distributive.

We first note that the functor F(t)=t (i.e. the identity functor) is co-pointed. It follows that all "monic monomial" functors of the form t*t*...*t are co-pointed.

Now we use the Lemma and show by induction that t*t*...*t is co-distributive.

Base of induction: the functor F(t)=t is co-distributive.
Step of induction: if F(t)=t*t*...*t is co-distributive, then so is t*F(t) because F is co-pointed and the Lemma holds.

Q.E.D.