Co-pointed functors are co-distributive
There was a bit of commotion about the concept of "co-applicative functors" (which I call co-distributive).
http://cstheory.stackexchange.com/questions/16241/is-there-a-concept-of-something-like-co-applicative-functors-sitting-between-com
https://www.reddit.com/r/haskell/comments/qsrmq/coapplicative_functor/
http://fplab.bitbucket.org/posts/2007-07-08-decisive-functors.html
Apparently it's not clear how exactly to define the categorical dual of "applicative" (= distributive) functor that would be useful in functional programming.

It turns out that co-monadic functors are co-distributive, but this is so for a different reason that the reason for monadic functors to be distributive.

Namely, monadic functors F are distributive by virtue of the monadic natural transformation F.F~>F, while co-monadic functors F are co-distributive by virtue of the "co-pointed" property, which is a natural transformation F ~> Id. The "co-monadic" property, F ~> F.F, is not used in the proof.

We need to work in a Cartesian closed category: all sums and products exist, and all morphisms are equivalent to some objects.

Definition: A functor F is co-pointed if there exists a natural transformation F ~> Id. In other words, there must be a function F(t) -> t that commutes with functor applications.

Statement: A co-pointed functor F is co-distributive: there exists a natural transformation F(a+b) ~> F(a)+F(b).

Proof: First apply the co-pointed property and get a+b out of F(a+b). It remains to construct F(a)+F(b) out of a+b and F(a+b).
For a fixed "a", consider the morphism a+b -> a defined in a special way: If a+b consists of an "a", return that "a" which is inside "a+b". If a+b consists of a "b", return the first "a".

chooseL :: a -> a+b -> a
chooseL x (0+y) = x
chooseL _ (x+0) = x

If "a" is given, this returns a morphism a+b -> a. We can lift this function into the image of the functor F and obtain a morphism F(a+b) -> F(a).

Similarly, if "b" is given, we can get a morphism F(a+b) -> F(a).

Now, returning to our task, we look at a+b and F(a+b). We make a choice based on a+b. If this contains an "a", we use the first morphism F(a+b)->F(a) to get F(a). Otherwise we use the second morphism F(a+b)->F(b) to get F(b). The result will be in F(a)+F(b), as required.

I'm starting to have doubts that I'm using a good approach. The proof is long-winded, and it would be faster just to write code (as people do in the articles linked above) than to explain all this in words.

Also, it is not obvious how to derive this proof automatically, starting from the required diagrams.

For instance, there is a trivial way of constructing a morphism a-> a+b -> a, by just ignoring a+b altogether and using the identity morphism a->a. But this would be incorrect (it fails to provide a natural transformation after the computation is over).