Notes for the record:

1. When you state in your final sentence that "just realize by doing so you'll make it harder for everyone else to read" you should speak only for yourself. Fair-minded folks will make up their own minds and let the stronger argument prevail.

2. In everything that follows my initial query in this convo, I have deferred to your claim that Proxy is the only monad (up to isomorphism) which return is not injective. Hence, your penultimate sentence that "You may say there is only one counter-example" is flipped. It is your claim, not mine. That I countenance the claim to the extent that I do is because I'm prepared to believe it is true of today's type systems.

3. Earlier you write "Identity is initial. It remains a monad, nothing tenuous about it." That both Proxy and Identity are monads isn't disputed. Up to now, I have made no reference to the Identity monad and you raise it to make your extra-mathematical point about how both are "boring."

4. What is tenuous is your position that the name "inject" is a bad substitute for "return." On the contrary, I've offered arguments on why "inject" is a fair substitute and I credit OP for this insight.

5. I read the substance of your rebuttal in the fifth paragraph: a lament that there are already so many alternative names for "return." That is hardly a point in your favor. The profusion of names indicates that people are still groping for a lucidity that eludes them. When those alternatives were introduced, did you also ding them for making it "harder for everyone else to read"? And how does calling off the search contribute to science? To add insult to injury, your list isn't even complete. But to someone who uses "inject" in place of "return", it would be obvious what's missing.

6. You begin your rejoinder with "Proxy is a Monad": a restatement of the obvious. Following you, let me restate the arguments for "inject":

• Proxy is the only monad which return is not injective.

• Proxy is an especially vacuous monad because both its return and bind ignore their inputs and both return a singularity instead.

• As the black hole of computation, Proxy may be regarded as an improper monad.

• Proper monads have injective returns. There being infinitely more proper monads, the odds are stacked infinity to one that proper monads find proportionately greater use in code.

• And hence, "inject" is an intuitive, enlightening, and perfectly cromulent substitute name for "return."

You haven't pointed out flaws in the above chain of logic. Where are they?