Polynomial functors VIII. Pre-comonadic recursive functors
Polynomial functors I. Basic motivations. All polynomial type constructors are functors.
Polynomial functors II. Basic definitions: (co)pointed, (co)distributive, (co)monadic. Monadic functors are distributive.
Co-pointed functors are co-distributive
Polynomial functors III: all polynomial functors are (co)distributive
Polynomial functors IV: all polynomial functors are pre-(co)-monadic
Polynomial functors V: recursive functors are (co)distributive
Polynomial functors VI: how to characterize pairs of functors with natural transformations between them
Polynomial functors VII. Pointed and co-pointed recursive polynomial functors
Exponential-polynomial functors, contrafunctors, and profunctors
Exponential-polynomial profunctors II. Modularity with respect to a monoid
Functional programming is physics
Tutorial on the free monad
Functors of functors. Deriving the "free monad". All recursive polynomial functors are pre-monadic
Polynomial functors VIII. Some recursive polynomial functors are pre-comonadic

We have established that all recursive polynomial type constructors are pre-monadic functors. The key method we used for proof was to use the construction called "Fix" (which is a "functor of functors") on a bifunctor of the form F(t,x) = A(x) + t*B(t,x). Let us see if the dual construction yields pre-comonadic functors.

The formula dual to A(x) + t*B(t,x) is A(x)*(t+B(t,x)). It turns out that this formula does not work (does not produce pre-comonadic functors as its x-fixpoints)! However, a weaker formula will work.

Theorem 1. If a bifunctor F(t,x) has the form F(t,x) = A(x)*B(t), where A and B are any functors, then G(t) = Fix_xF(t,x) is a pre-comonadic functor, which means that there exists a natural transformation G(t) ~> G(G(t)).

Proof. We need to produce a natural transformation G(t) = F(t,G(t)) ~> G(G(t)) = F(G(t),G(G(t))). As before, we use the boldface G to denote the functor for which the statement of the theorem already holds by the inductive assumption.
Substituting the formula for F(t,x), we see that we need to produce a natural transformation
G(t) = A(G(t))*B(t) ~> A(G(G(t)))*B(G(t)).
We will be able to produce it if we produce natural transformations
A(G(t))*B(t) ~> A(G(G(t))) -- (1)
and
G(t) = A(G(t))*B(t) ~> B(G(t)) -- (2).
We can produce (1) by taking the natural morphism G(t) ~> G(G(t)), which exists by the inductive assumption, and lifting it into the functor A.
The transformation (2) takes a bit more work. We need to produce B(G(t)) from G(t), or equivalently from A(G(t))*B(t). We may assume that we have both G(t) and A(G(t))*B(t) = G(t). Thus it will suffice if we produce a morphism
G(t) * A(G(t))*B(t) ~> B(G(t)). (We dropped the boldface notation since we will not need it for now.)

We can show that, for any functor B, the following natural morphism can be constructed:
x*B(y) ~> B(x). -- (3)
This morphism, or its equivalent x -> B(y) -> B(x), is obtained by taking the constant function x -> y -> x and lifting its value y -> x into the functor B.

Now we use (3) with x = G(t) and y = t, and obtain the required morphism.
Q.E.D.

Now, it is not true that all polynomial bifunctors F(t,x) can be written as A(x)*B(t). (In any case, there is no "conjunctive normal form" for polynomial functors, because polynomial functors cannot be decomposed into factors.) So, for instance, the bifunctor F(t,x) = x*x+t*t cannot be written as A(x)*B(t). So we cannot conclude that all recursive polynomial functors are pre-comonadic.

Is it possible to give a counterexample: to produce a polynomial bifunctor F(t,x) such that G(t) = Fix_xF(t,x) is definitely not pre-comonadic?

Or else, is it possible to relax the conditions of Theorem 1 so that more bifunctors can be used?