Here's a write-up I did on deriving the Y combinator from Lawvere's fixed-point theorem: https://emarzion.github.io/Y-Comb/

Anyone interested in this might get a kick out of the book “To Mock A Mockingbird”.

The first half of the book is an almost exhaustive exploration of self-referential riddles. Like “if the barber shaves everyone who doesn’t shave themselves, who shaves the barber?” and “if one gremlin always tells the truth and the other always lies, how can you ask them for directions?”

The second half of the book is a rigorous examination of combinatorial logic through an analogy of birds who make calls depending on the calls of other birds they hear. It touches on function composition,recursion, fixed points, godels theorems, and the Y combinator (the mockingbird).

My only gripe with the book is that it stays completely within the bird metaphor, and doesn’t always explicitly state the underlying math concept.

Is there a technique to remember this? I will understand it today and forget after a few weeks.

If anyone wants this in a humorous 1 hour format, watch the legendary Jim Weirich (rip) explain it here: https://www.youtube.com/watch?v=FITJMJjASUs

Don't be discouraged that it is in Ruby as the concepts are completely general. Great watch even though I never coded a line of Ruby.

From scratch it's also easy dress up a quoted Y combinator as in Löb's theorem. Start with the usual Y combinator

  Y = \f. (\x.f(x x)) (\x.f(x x))
    : (p -> p) -> p

which can produce a thing of type p from a function f : p -> p.

Now Löb's theorem states that []([]p -> p) -> []p, which can be read, "if you have the source code to transform (the source code of a thing of type p) to a thing of type p, then you can produce the source code for a thing of type p". Let's embellish Y using {} to denote the quoting comonad.

  Y' = \{f}. (\{x}.{f{x{x}}}) {\{x}.{f{x{x}}}}
     : []([]p -> p) -> []p

To get there, just add quotes as needed: f must be quoted, f's result must be quoted, and f takes a quoted input.