Skip to main content
1 of 4

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 similar to the one described in http://opus.bath.ac.uk/23104/[1]. Namely, (a: a0 → a1) maps to a + (0 → a1), with obvious unit and multiplication. Now this monad is obviously not strong.

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.