Contrafunctors cannot be distributive or traversable
In the previous two posts, I used contrafunctors that are either traversable or distributive; there I assumed, without checking, that some non-constant contrafunctors with these properties would exist. It appears, however, that they do not exist.

My proofs shown here are a bit shaky. I'm not certain that I have really proved these statements. But I have "convinced myself" that they are true "at the programmer's level of rigor". (As I noted in an earlier post, functional programming is somewhat analogous to physics; similarly to having theoretical physics that uses a "physicist's level of rigor" in proofs, there is also a functional type theory and a "programmer's level of rigor" in its derivations.)

Statement 1. If a contrafunctor S is distributive, it is a constant type S t = c for some fixed type c.

Comments: A contrafunctor S is distributive if there exists a natural transformation S(a × b) ~> S a × S b, which is equivalent to the existence of the transformation, say, S(a × b) ~> S b.
Note that all contrafunctors are co-distributive: S a ~> S(a × b) and S b ~> S(a × b) both exist due to the existence of canonical morphisms a × b -> a and a × b -> b.

Proof.
If S(a × b) ~> S b exists, set a = 0 and b = 1. We then get a canonical morphism S(0) ~> S(1). This is a peculiar morphism: since we have 0 -> 1, we also have S(1) -> S(0). Thus, the types S(0) and S(1) should be equivalent. This can work only when S is a constant contrafunctor.

Statement 2. If a contrafunctor is traversable, it is a constant unit type, S t = 1.

Comments: A contrafunctor S is traversable if, for any applicative functor A, there exists a natural transformation A (S t) ~> S(A t) that commutes with the two natural transformations ("point" and "apply") that define the applicative property of A.
Note that all contrafunctors are co-traversable, i.e. they admit a natural transformation S(A t) ~> A(S t). This exists due to the A-point transformations t ~> A t and S t ~> A(S t), which allow us to map S(A t) ~> S t ~> A(S t).

Proof: If S were traversable, we would have A(S t) ~> S(A t) -> S t. So, the type S t is such that we can extract a value of type S t from A(S t) for any applicative functor A. This is impossible, because some applicative functors are not co-pointed; the applicative property does not include any natural transformations that remove a layer of A from the type. So, the only way to extract x from A x for any A is to ignore the given value of A x and provide a fixed value of x. However, this will not commute with the point law unless x = 1.