Baking the Y Combinator from Scratch

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.