A valuable insight, but doesn't that come with a caveat. Def 3 is only def 1 when the 'x' in def 1 is a function or an operator or some kind. If it's "truly a v

A valuable insight, but doesn't that come with a caveat. Def 3 is only def 1 when the 'x' in def 1 is a function or an operator or some kind. If it's "truly a value" then x is instead an identity value and not idempotent isn't it? And for #1, what if "f" is a function that selects the first of the two arguments? Then the relation in #1 holds true for all values of 'x', but that doesn't feel like idempotency to me. And we definitely can't say that 'x' is idempotent. As 'x' defined to be "add1" wouldn't be idempotent according to the definition, but would pass the relation if "f" is fst(). I think #1 only holds under compose or 'f's that are similar to compose when 'x' is a function. And at that point you've added so many restrictions you've made definition 3. So I think I disagree with definition #1 as being a def of idempotency.