Is this monad equation true?

Stream: general

[François G. Dorais]

Is this true?

[Monad m] [LawfulMonad m] (f : m α → m β) (x : m α) : x >>= f ∘ pure = f x

I would love a proof if it is true.

[François G. Dorais]

Never mind. I found a counterexample right after pressing enter...

[Mario Carneiro]

this depends on some property of f, it's related to monotonicity in the domain theory sense

[Mario Carneiro]

or maybe lower semicontinuity, since it's saying that f x is the supremum of f (pure a) over all a <= x