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.