Hi, John, In your Week 240 post to categories, you said
The moral of this game is that all systematic methods for picking an element of (X^X)^(X^X) for an unknown set X can be written using the lambda calculus.
What is unsystematic about the contagious-fixpoint functional? This is the functional that maps those functions that have any fixpoints to the identity function (the function that makes every element a fixpoint) and functions without fixpoints to themselves (thus preserving the absence of fixpoints). It's a perfectly good functional that is equally well defined for all sets X, its statement in no way depends on X, and conceptually the concept of contagious fixpoints is even intuitively natural, but how do you write it using the lambda calculus? Many more examples in this vein at JPAA 128, 33-92 (Pare and Roman, Dinatural numbers, 1998). The above is the case K = {0} of Freyd's (proper) class of examples. Vaughan