[maxiepoo]

I have to plug my favorite "explanation" of the Y combinator, which is called "Lawvere's fixed point theorem".

In a cartesian closed category, if there is a function p : A -> (A -> B) that has a left-inverse, i.e., e : (A -> B) -> A with p o e = id_(A -> B) then B has a fixed point combinator Y : (B -> B) -> B, i.e., every function from B to itself has a fixed point: Y(f) = f(Y(f)).

The proof is like the Y combinator in untyped lambda calculus, but with extra ps and es. This is because one way to understand untyped lambda calculus is that you are working with a single type D that satisfies D = (D -> D) (so p,e are identities).

I like this because it makes the connection between the Y combinator and diagonalization arguments like Cantor's theorem explicit.

For instance, Cantor's theorem says that the powerset of a set always has higher cardinality. We can reformulate this as saying that there is no onto function p : X -> (X -> 2) because a subset of X is the same as a function from X to booleans (2 = {true, false}). An onto function has a left inverse (using axiom of choice) and so if we have an onto function X -> (X -> 2) then every function (2 -> 2) has a fixed point, but this isn't true! If we took Y(not) we would construct a boolean b : 2 such that b = not(b), which is impossible so we have a contradiction. I found this helpful in understanding why the "not" appears in just the right place in the classical proof.

[3PS]

> if there is a function p : A -> (A -> B) that has a left-inverse, i.e., e : (A -> B) -> A with p o e = id_(A -> B) then B has a fixed point combinator

I think you meant to write "right inverse" here.

Agreed that Lawvere's theorem is very cool. It helps that Cartesian closed categories are basically just categories where you can do typed lambda calculus, so the underlying link is already very close.