I believe I found a simple sample for a ccc, based on the answers from Tom Leinster, Finn Lawler and John Bourke, and http://opus.bath.ac.uk/23104[1]
I also used the fact I found in Moggi's "Computational lambda-calculus and monads" - that a category should be well-pointed.
Take category 2 (two objects, three arrows), and a topos Set2. This topos is obviously not well-pointed, so we can proceed. Take a monad M that is similar to the one described in http://opus.bath.ac.uk/23104/[1]. Namely, (a: a0 → a1) maps to a + (0 → a0), with obvious unit and multiplication.
Now this monad is not strong. Suppose it were, then for a: a0 → a1 and b: b0 → b1, the strength a × M[b] → M[a × b] would involve specifying a morphism from a1 to a0 × b0 + a1 × b1. This morphism cannot be a × b1, because in this case it won't be preserving the tensor product's (which is Cartesian in our case) unit. And what if b0 is empty.
I believe this kind of topos would be a good testing area for the favorite Haskell constructs. Some of them won't hold, I believe.
Now I wonder... can we prove that if all monads over a topos are strong, then the topos is Boolean? Will post it in another question.
